Deterministic Compilation of Temporal Safety Properties in Explicit State Model Checking

The translation of temporal logic specifications constitutes an essen- tial step in model checking and a major influence on the efficiency of formal verification via model checking. We devise a new explicit-state translation of Lin- ear Temporal Logic to automata for the class of LTL specifications that describe safety properties, arguably the most used formal specifications in real-world sys- tems. By exploiting the inherent determinism in safety specifications, we can build deterministic Promela never claims that accept only the bad prefixes of the safety specification. In contrast to previous works, we focus on compilation to never claims rather than simply automata and measure Spin model-checking time separately from compilation time and automata size. An extensive experi- mental evaluation over a space of configurations demonstrates that our new trans- lation consistently results in better model-checking performance, for a large array of benchmarks, over the best current translation.