Armin Biere ; Keijo Heljanko ; Tommi Junttila ; Timo Latvala ; Viktor Schuppan - Linear Encodings of Bounded LTL Model Checking

lmcs:2236 - Logical Methods in Computer Science, November 15, 2006, Volume 2, Issue 5 -
Linear Encodings of Bounded LTL Model CheckingArticle

Authors: Armin Biere ORCID1; Keijo Heljanko ORCID2; Tommi Junttila 2; Timo Latvala 3; Viktor Schuppan 4

  • 1 Institute for Formal Models and Verification, Johannes Kepler University
  • 2 Laboratory for Theoretical Computer Science, Helsinki University of Technology
  • 3 Department of Computer Science, University of Illinois at Urbana-Champaign
  • 4 Computer Systems Institute, ETH Zentrum

We consider the problem of bounded model checking (BMC) for linear temporal logic (LTL). We present several efficient encodings that have size linear in the bound. Furthermore, we show how the encodings can be extended to LTL with past operators (PLTL). The generalised encoding is still of linear size, but cannot detect minimal length counterexamples. By using the virtual unrolling technique minimal length counterexamples can be captured, however, the size of the encoding is quadratic in the specification. We also extend virtual unrolling to Buchi automata, enabling them to accept minimal length counterexamples. Our BMC encodings can be made incremental in order to benefit from incremental SAT technology. With fairly small modifications the incremental encoding can be further enhanced with a termination check, allowing us to prove properties with BMC. Experiments clearly show that our new encodings improve performance of BMC considerably, particularly in the case of the incremental encoding, and that they are very competitive for finding bugs. An analysis of the liveness-to-safety transformation reveals many similarities to the BMC encodings in this paper. Using the liveness-to-safety translation with BDD-based invariant checking results in an efficient method to find shortest counterexamples that complements the BMC-based approach.

Volume: Volume 2, Issue 5
Published on: November 15, 2006
Submitted on: February 16, 2006
Keywords: Computer Science - Logic in Computer Science,F.3.1,B.6.3,D.2.4,F.4.1
    Source : OpenAIRE Graph
  • Rajoiteohjelmointimenetelmät laajoille rakenteisille ongelmille; Funder: Academy of Finland; Code: 211025
  • Testing, verification and synthesis of distributed systems; Funder: Academy of Finland; Code: 213113
  • Scalable Model Checking Techniques; Funder: Academy of Finland; Code: 109539

107 Documents citing this article

Consultation statistics

This page has been seen 1878 times.
This article's PDF has been downloaded 876 times.