Linear Encodings of Bounded LTL Model Checking

Abstract

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.

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

Cited by in corpus (22)

• Industrial-Strength Model-Based Testing - State of the Art and Current Challenges
• A Metric Encoding for Bounded Model Checking (extended version)
• Tarmo: A Framework for Parallelized Bounded Model Checking
• From Uncertainty Data to Robust Policies for Temporal Logic Planning
• Extracting Unsatisfiable Cores for LTL via Temporal Resolution
• Model Predictive Control for Signal Temporal Logic Specification
• Extending a system in the calculus of structures with a self-dual quantifier
• An Abstraction-Free Method for Multi-Robot Temporal Logic Optimal Control Synthesis
• Active Perception and Control from PrSTL Specifications
• Computing unsatisfiable cores for LTLf specifications
• Robust Control Policies given Formal Specifications in Uncertain Environments
• Constraint LTL Satisfiability Checking without Automata
• Explaining Multi-stage Tasks by Learning Temporal Logic Formulas from Suboptimal Demonstrations
• A User's Guide to Zot
• Bounded Reachability for Temporal Logic over Constraint Systems
• SMT-based Verification of LTL Specifications with Integer Constraints and its Application to Runtime Checking of Service Substitutability
• Monte Carlo Tree Search guided by Symbolic Advice for MDPs
• Control of Timed Discrete Event Systems with Ticked Linear Temporal Logic Constraints
• Bounded Model Checking of an MITL Fragment for Timed Automata
• idSTLPy: A Python Toolbox for Active Perception and Control
• Footstep Planning with Encoded Linear Temporal Logic Specifications
• Automatic Trajectory Synthesis for Real-Time Temporal Logic