Linear Encodings of Bounded LTL Model Checking

Details Linear Encodings of Bounded LTL Model Checking Linear Encodings of Bounded LTL Model Checking

2006-11-07

arxiv.org/abs/cs/0611029v3

LMCS 2 (5:5) 2006

Computer Science

Logic in Computer Science

Final version for Logical Methods in Computer Science CAV 2005 special issue

Scientific paper

10.2168/LMCS-2(5:5)2006

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.

Affiliated with

Also associated with

No associations

Rating

Linear Encodings of Bounded LTL Model Checking does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Linear Encodings of Bounded LTL Model Checking, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Linear Encodings of Bounded LTL Model Checking will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-617635