Constructing automata from temporal logic formulas: A tutorial. (English) Zbl 0990.68088
Brinksma, Ed (ed.) et al., Lectures on Formal methods and performance analysis. 1st EEF/Euro summer school on trends in computer science, Berg en Dal, the Netherlands, July 3-7, 2000. Revised lectures. Berlin: Springer. Lect. Notes Comput. Sci. 2090, 261-277 (2001).
Summary: This paper presents a tutorial introduction to the construction of finite automata on infinite words from linear-time temporal logic formulas. After defining the source and target formalisms, it describes a first construction whose correctness is quite direct to establish, but whose behavior is always equal to the worst-case upper bound. It then turns to the techniques that can be used to improve this algorithm in order to obtain the quite effective algorithms that are now in use.
For the entire collection see [Zbl 0969.00082].
For the entire collection see [Zbl 0969.00082].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q45 | Formal languages and automata |
| 03B44 | Temporal logic |
| 03D05 | Automata and formal grammars in connection with logical questions |
