LTL'S INTUITIVE REPRESENTATIONS AND ITS AUTOMATON TRANSLATION

摘要

Compared with other verification methods, to some sense, model checking can be thought of as more attractive method to test hardware and software systems due to its automatic features. However, a stumbling problem is how to supply correct formal properties in logic to do model checking by system designers without specific mathematical background. This paper first presents two intuit-tive representations for the LTL formulas: one is graphical automaton-like; the other is textual regular-expression-like and then shows how these representations can be used to construct Buechi automata for LTL model checking.