On-the-fly emptiness check of transition-based Streett automata
In Proceedings of the 7th international symposium on automated technology for verification and analysis (ATVA’09)
Abstract
In the automata theoretic approach to model checking, checking a state-space $S$ against a linear-time property $\varphi$ can be done in $\mathrm{O}(|S|\times 2^{\mathrm{O}(|\varphi|)})$ time. When model checking under $n$ strong fairness hypotheses expressed as a Generalized Büchi automaton, this complexity becomes $\mathrm{O}(|S|\times 2^{\mathrm{O}(|\varphi|+n)})$.Here we describe an algorithm to check the emptiness of Streett automata, which allows model checking under $n$ strong fairness hypotheses in $\mathrm{O}(|S|\times 2^{\mathrm{O}(|\varphi|)}\times 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.