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.

Abstract:
Satisfiability checking for Linear Temporal Logic (LTL) is a fundamental step in checking for possible errors in LTL assertions. Extant LTL satisfiability checkers use a variety of different search procedures. With the sole exception of LTL satisfiability checking based on bounded model checking, which does not provide a complete decision procedure, LTL satisfiability checkers have not taken advantage of the remarkable progress over the past 20 years in Boolean satisfiability solving. In this paper, we propose a new LTL satisfiability-checking framework that is accelerated using a Boolean SAT solver. Our approach is based on the variant of the \emph{obligation-set method}, which we proposed in earlier work. We describe here heuristics that allow the use of a Boolean SAT solver to analyze the obligations for a given LTL formula. The experimental evaluation indicates that the new approach provides a a significant performance advantage.

Abstract:
The parameter synthesis problem for timed automata is undecidable in general even for very simple reachability properties. In this paper we introduce restrictions on parameter valuations under which the parameter synthesis problem is decidable for LTL properties. The proposed problem could be solved using an explicit enumeration of all possible parameter valuations. However, we introduce a symbolic zone-based method for synthesising bounded integer parameters of parametric timed automata with an LTL specification. Our method extends the ideas of the standard automata-based approach to LTL model checking of timed automata. Our solution employs constrained parametric difference bound matrices and a suitable notion of extrapolation.

Abstract:
This paper introduces a novel technique to decide the satisfiability of formulae written in the language of Linear Temporal Logic with Both future and past operators and atomic formulae belonging to constraint system D (CLTLB(D) for short). The technique is based on the concept of bounded satisfiability, and hinges on an encoding of CLTLB(D) formulae into QF-EUD, the theory of quantifier-free equality and uninterpreted functions combined with D. Similarly to standard LTL, where bounded model-checking and SAT-solvers can be used as an alternative to automata-theoretic approaches to model-checking, our approach allows users to solve the satisfiability problem for CLTLB(D) formulae through SMT-solving techniques, rather than by checking the emptiness of the language of a suitable automaton A_{\phi}. The technique is effective, and it has been implemented in our Zot formal verification tool.

Abstract:
By algorithmic metatheorems for a model checking problem P over infinite-state systems we mean generic results that can be used to infer decidability (possibly complexity) of P not only over a specific class of infinite systems, but over a large family of classes of infinite systems. Such results normally start with a powerful formalism of infinite-state systems, over which P is undecidable, and assert decidability when is restricted by means of an extra "semantic condition" C. We prove various algorithmic metatheorems for the problems of model checking LTL and its two common fragments LTL(Fs,Gs) and LTLdet over the expressive class of word/tree automatic transition systems, which are generated by synchronized finite-state transducers operating on finite words and trees. We present numerous applications, where we derive (in a unified manner) many known and previously unknown decidability and complexity results of model checking LTL and its fragments over specific classes of infinite-state systems including pushdown systems; prefix-recognizable systems; reversal-bounded counter systems with discrete clocks and a free counter; concurrent pushdown systems with a bounded number of context-switches; various subclasses of Petri nets; weakly extended PA-processes; and weakly extended ground-tree rewrite systems. In all cases,we are able to derive optimal (or near optimal) complexity. Finally, we pinpoint the exact locations in the arithmetic and analytic hierarchies of the problem of checking a relevant semantic condition and the LTL model checking problems over all word/tree automatic systems.

Abstract:
We propose a novel algorithm for automata-based LTL model checking that interleaves the construction of the generalized B\"{u}chi automaton for the negation of the formula and the emptiness check. Our algorithm first converts the LTL formula into a linear weak alternating automaton; configurations of the alternating automaton correspond to the locations of a generalized B\"{u}chi automaton, and a variant of Tarjan's algorithm is used to decide the existence of an accepting run of the product of the transition system and the automaton. Because we avoid an explicit construction of the B\"{u}chi automaton, our approach can yield significant improvements in runtime and memory, for large LTL formulas. The algorithm has been implemented within the SPIN model checker, and we present experimental results for some benchmark examples.

Abstract:
Constraint automata are an adaptation of B\"uchi-automata that process data words where the data comes from some relational structure S. Every transition of such an automaton comes with constraints in terms of the relations of S. A transition can only be fired if the current and the next data values satisfy all constraints of this transition. These automata have been used in the setting where S is a linear order for deciding constraint LTL with constraints over S. In this paper, S is the infinitely branching infinite order tree T. We provide a PSPACE algorithm for emptiness of T-constraint automata. This result implies PSPACE-completeness of the satisfiability and the model checking problem for constraint LTL with constraints over T.

Abstract:
Timed automata (TAs) are a common formalism for modeling timed systems. Bounded model checking (BMC) is a verification method that searches for runs violating a property using a SAT or SMT solver. MITL is a real-time extension of the linear time logic LTL. Originally, MITL was defined for traces of non-overlapping time intervals rather than the "super-dense" time traces allowing for intervals overlapping in single points that are employed by the nowadays common semantics of timed automata. In this paper we extend the semantics of a fragment of MITL to super-dense time traces and devise a bounded model checking encoding for the fragment. We prove correctness and completeness in the sense that using a sufficiently large bound a counter-example to any given non-holding property can be found. We have implemented the proposed bounded model checking approach and experimentally studied the efficiency and scalability of the implementation.

Abstract:
We study complexity of the model-checking problems for LTL with registers (also known as freeze LTL) and for first-order logic with data equality tests over one-counter automata. We consider several classes of one-counter automata (mainly deterministic vs. nondeterministic) and several logical fragments (restriction on the number of registers or variables and on the use of propositional variables for control locations). The logics have the ability to store a counter value and to test it later against the current counter value. We show that model checking over deterministic one-counter automata is PSPACE-complete with infinite and finite accepting runs. By constrast, we prove that model checking freeze LTL in which the until operator is restricted to the eventually operator over nondeterministic one-counter automata is undecidable even if only one register is used and with no propositional variable. As a corollary of our proof, this also holds for first-order logic with data equality tests restricted to two variables. This makes a difference with the facts that several verification problems for one-counter automata are known to be decidable with relatively low complexity, and that finitary satisfiability for the two logics are decidable. Our results pave the way for model-checking memoryful (linear-time) logics over other classes of operational models, such as reversal-bounded counter machines.

Abstract:
In this paper we present a tool that performs CUDA accelerated LTL Model Checking. The tool exploits parallel algorithm MAP adjusted to the NVIDIA CUDA architecture in order to efficiently detect the presence of accepting cycles in a directed graph. Accepting cycle detection is the core algorithmic procedure in automata-based LTL Model Checking. We demonstrate that the tool outperforms non-accelerated version of the algorithm and we discuss where the limits of the tool are and what we intend to do in the future to avoid them.