zbMATH — the first resource for mathematics

Alternating the temporal picture for safety. (English) Zbl 0973.68141
Montanari, Ugo (ed.) et al., Automata, languages and programming. 27th international colloquium, ICALP 2000, Geneva, Switzerland, July 9-15, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1853, 429-450 (2000).
Summary: We use alternating automata on infinite words to reduce the verification of linear temporal logic safety properties over infinite-state systems to the proof of first-order verification conditions. This method generalizes the traditional deductive verification approach of providing verification rules for particular classes of formulas, such as invariances, nested precedence formulas, etc. It facilitates the deductive verification of arbitrary safety properties without the need for explicit temporal reasoning.
For the entire collection see [Zbl 0941.00034].

68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
68Q45 Formal languages and automata