[Lrde Annonce] Publication: SUMo'11: Generalized Büchi Automata versus Testing Automata for Model Checking

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