We are happy to announce that the following paper has been accepted for publication at the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09) that will take place at Macao on 14-16 October 2009.

Alexandre Duret-Lutz (1) Denis Poitrenaud (2) Jean-Michel Couvreur (3)

On-the-fly Emptiness Check of Transition-based Streett Automata

http://publis.lrde.epita.fr/200910-ATVA

(1) EPITA Research and Development Laboratory (LRDE) (2) Laboratoire d'Informatique de Paris 6 (LIP6) (3) Laboratoire d'Informatique Fondamentale d'Orléans (LIFO)

In the automata theoretic approach to model checking, checking a state-space S against a linear-time property F can be done in O(|S|\times 2^O(|F|)) time. When model checking under n strong fairness hypotheses expressed as a Generalized Büchi automaton, this complexity becomes O(|S|*2^O(|F|+n)).

Here we describe an algorithm to check the emptiness of Streett automata, which allows model checking under n strong fairness hypotheses in O(|S|*2^O(|F|)*n). We focus on transition-based Streett automata, because it allows us to express strong fairness hypotheses by injecting Streett acceptance conditions into the state-space without any blowup.