publication . Article . Other literature type . Preprint . 2006

Linear Encodings of Bounded LTL Model Checking

Biere, Armin; Heljanko, Keijo; Junttila, Tommi; Latvala, Timo; Schuppan, Viktor;
Open Access
  • Published: 15 Nov 2006 Journal: Logical Methods in Computer Science, volume 2 (eissn: 1860-5974, Copyright policy)
  • Publisher: Logical Methods in Computer Science e.V.
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...
free text keywords: Theoretical Computer Science, General Computer Science, Invariant (mathematics), Counterexample, Encoding (memory), Büchi automaton, Discrete mathematics, Bounded function, Algorithm, Incremental encoding, Cycle detection, Model checking, Mathematics, Computer Science - Logic in Computer Science, F.3.1, B.6.3, D.2.4, F.4.1
93 references, page 1 of 7

[Acc04] Accellera. Property specification language: Reference manual - version 1.1, 2004. 60

[AEF+05] R. Armoni, S. Egorov, R. Fraer, D. Korchemny, and M. Y. Vardi. Efficient LTL compilation for SAT-based model checking. In ICCAD'05, pages 877-884. IEEE, 2005. 44 [OpenAIRE]

[AFF+05] R. Armoni, L. Fix, R. Fraer, S. Huddleston, N. Piterman, and M. Y. Vardi. SAT-based induction for temporal safety properties. ENTCS, 119(2):3-16, 2005. 24, 44, 55

[AS04] M. Awedh and F. Somenzi. Proving more properties with bounded model checking. In CAV'04, volume 3114 of LNCS, pages 96-108, 2004. 19, 44 [OpenAIRE]

[AS06] M. Awedh and F. Somenzi. Termination criteria for bounded model checking: Extensions and comparison. ENTCS, 144(1):51-66, 2006. 18, 19, 44, 52 [OpenAIRE]

[BAS02] A. Biere, C. Artho, and V. Schuppan. Liveness checking as safety checking. In FMICS'02, ENTCS, 66(2). Elsevier, 2002. 21 [OpenAIRE]

[BB04] M. Benedetti and S. Bernardini. Incremental compilation-to-SAT procedures. In SAT [SAT04]. 40

[BC03] M. Benedetti and A. Cimatti. Bounded model checking for past LTL. In TACAS'03, volume 2619 of LNCS, pages 18-33. Springer, 2003. 3, 4, 6, 7, 15, 25, 26, 27, 28, 40, 51, 53 [OpenAIRE]

[BCC+03] A. Biere, A. Cimatti, E. Clarke, O. Strichman, and Y. Zhu. Bounded model checking. In Advances in Computers, volume 58. Academic Press, 2003. 8

[BCCZ99] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In TACAS'99, volume 1579 of LNCS, pages 193-207. Springer, 1999. 2, 4, 7, 8, 13, 21, 26 [OpenAIRE]

[BCM+92] J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98:142-170, 1992. 18, 19, 49

[BCP+06] R. Bloem, A. Cimatti, I. Pill, M. Roveri, and S. Semprini. Symbolic implementation of alternating automata. In CIAA'06, volume 4094 of LNCS, pages 208-218, August 2006. 60 [OpenAIRE]

[BCRZ99] A. Biere, E. Clarke, R. Raimi, and Y. Zhu. Verifying safety properties of a Power PC microprocessor using symbolic model checking without BDDs. In CAV'99, volume 1633 of LNCS, pages 60-71. Springer, 1999. 3, 15 [OpenAIRE]

[BHV04] A. Bouajjani, P. Habermehl, and T. Vojnar. Abstract regular model checking. In CAV'04, volume 3114 of LNCS, pages 372-386. Springer, 2004. 21 [OpenAIRE]

[Bry86] R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 38(8):677-691, 1986. 3

93 references, page 1 of 7
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue