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 …