Improved automata generation for linear temporal logic. (English) Zbl 1046.68588

Daniele, Marco; Giunchiglia, Fausto; Vardi, Moshe Y.

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