×

zbMATH — the first resource for mathematics

Improved automata generation for linear temporal logic. (English) Zbl 1046.68588
Halbwachs, Nicolas (ed.) et al., Computer aided verification. 11th international conference, CAV ’99. Trento, Italy, July 6–10, 1999. Proceedings. Berlin: Springer (ISBN 3-540-66202-2). Lect. Notes Comput. Sci. 1633, 249-260 (1999).
Summary: We improve the state-of-the-art algorithm for obtaining an automaton from a linear temporal logic formula. The automaton is intended to be used for model checking, as well as for satisfiability checking. Therefore, the algorithm is mainly concerned with keeping the automaton as small as possible. The experimental results show that our algorithm outperforms the previous one, with respect to both the size of the generated automata and computation time. The testing is performed following a newly developed methodology based on the use of randomly generated formulas.
For the entire collection see [Zbl 0925.68015].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
68Q45 Formal languages and automata
Software:
CESAR; SPIN
PDF BibTeX XML Cite