Liveness checking as safety checking to find shortest counterexamples to linear time properties

Temporal logic is widely used for specifying hardware and software systems.Typically two types of properties are distinguished, safety and liveness properties.While safety can easily be checked by reachability analysis, and many efficient checkers for safety properties exist, more sophisticated algorithms have always been considered to be necessary for checking liveness.In this dissertation we describe an efficient translation of liveness checking problems into safety checking problems for finite state systems.More precisely, fair repeated reachability in a fair Kripke structure K is formulated as reachability in a transformed Kripke structure K S .A fair loop in K is detected in K S by saving a previously visited state in an additional state-recording component, waiting until a fair state has been seen, and checking a loop closing condition.The approach extends to all ω-regular properties.We show that the size of the state space, the reachable state space, the transition relation, and its transitive closure grow by a factor of |S| in the transformed model, where |S| is the size of the state space in the original model.Radius and diameter increase by a small, constant factor.We discuss optimizations that limit the overhead of our translation.We have implemented the approach for BDD-based model checkers of the SMV family.Experimental results show not only that the approach is feasible for complex examples, but that it may lead to faster verification if the property turns out to be false.For one example even an exponential speed-up can be observed.We finally show that a similar reduction can be applied to a number of infinite state systems, namely, (ω-) regular model checking, pushdown systems, and timed automata.Counterexamples as produced by a model checker for a failing property help developers to understand the problem in a faulty design.The shorter a counterexample, the easier it is typically to understand.The length of a counterexample, as reported by a model checker, depends on both the algorithm used for state space exploration and the way the property is encoded.We provide necessary and sufficient criteria for a Büchi automaton to accept shortest counterexamples.Extending a notion introduced by Kupferman and Vardi we call a Büchi automaton that accepts shortest counterexamples tight.We prove that Büchi automata constructed using the approach of Kesten et al. (KPR), which is essentially the same as the construction by Lichtenstein and Pnueli, are tight for future time LTL formulae, while an automaton generated with the algorithm of Gerth et al. (GPVW) may lead to unnecessary long counterexamples.Optimality is lost in the first case as soon as past time operators are included.We show that potential excess length is in both cases at most linear in the length of the specification.Using a recently proposed encoding for bounded model checking of LTL with past by Latvala et al., we construct a Büchi automaton that accepts shortest counterexamples for full LTL.The construction adapts the idea of virtual unrolling by Benedetti and Cimatti to Büchi automata.Its generalization gives a method to make an arbitrary Büchi automaton accept shortest counterexamples.We use our method of translating liveness into safety to find shortest counterexamples with a BDD-based symbolic model checker without modifying the model checker itself.Though v vi our method involves a quadratic blowup of the state space, it proves to be competitive with SAT-based bounded model checking.Experimental results show that using a model checking algorithm that finds shortest cycles contributes much more to a reduction in counterexample length than using an automaton that accepts shortest counterexamples when compared with the automaton by Kesten et al.