In the automata theoretic approach to model checking, checking a state-space S against a linear-time property φ can be done in O(|S|×2 O(|φ|)) time. When model checking under n strong fairness hypotheses expressed as a Generalized Büchi automaton, this complexity becomes O(|S|×2 O(|φ|∈+∈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(|φ|)×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. © 2009 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Duret-Lutz, A., Poitrenaud, D., & Couvreur, J. M. (2009). On-the-fly emptiness check of transition-based Streett automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5799 LNCS, pp. 213–227). https://doi.org/10.1007/978-3-642-04761-9_17
Mendeley helps you to discover research relevant for your work.