We are happy to announce that the following paper has been accepted
for publication at the 2nd International Workshop on Scalable and
Usable Model Checking for Petri Nets and other models of Concurrency
(SUMo'11) that will take place in Newcastle, UK, on June 21, 2011.
Generalized Büchi Automata versus Testing Automata
for Model Checking
A.-E. Ben Salem (1&2)
A. Duret-Lutz (1)
F. Kordon (2)
(1) Laboratoire de Recherche et Développement de l'Epita (LRDE)
(2) Laboratoire d'Informatique de Paris 6 (LIP6)
http://publis.lrde.epita.fr/201106-SUMO
Geldenhuys and Hansen have shown that a kind of omega-automaton
known as testing automata can outperform the Büchi automata
traditionally used in the automata-theoretic approach to model
checking. This work completes their experiments by including a
comparison with generalized Büchi automata; by using larger state
spaces derived from Petri nets; and by distinguishing violated
formulae (for which testing automata fare better) from verified
formulae (where testing automata are hindered by their two-pass
emptiness check).
--
Alexandre Duret-Lutz