Causality-based LTL Model Checking without Automata

The classical LTL model checking algorithm starts by transforming the negated LTL property into the Büchi automaton. Unfortunately, already that step often takes exponential time and space. For concurrent programs the size of the formula that describes, e. g. , fairness assumptions, grows with the size of the program to be verified. Therefore, the exponential translation cost often does not allow the verification process even to start. In the present work we propose an alternative to the automata-based model checking, which is lazy and compositional with respect both to the system and to the LTL property. In our procedure, we characterize the existence of erroneous executions as Mazurkiewicz-style concurrent traces and apply causality-based transformation rules to refine them until a contradiction can be shown. The algorithm operates directly on the level of an LTL formula and a concurrent program description, and lazily pulls from both of them only the parts that are necessary in the current analysis context. We report on experimental results for previously intractable multi-threaded benchmarks.

Authors

• Andrey Kupriyanov

Keywords

No keywords are indexed for this paper.