LTL’s Intuitive Representations and Its Automaton Translation
Yuhong Zhao · Kluwer Academic Publishers eBooks · 2006
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 intuittive 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 Büchi automata for LTL model checking.