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

### From LRDE

- Authors
- Alexandre Duret-Lutz, Denis Poitrenaud, Jean-Michel Couvreur
- Where
- Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09)
- Type
- inproceedings
- Publisher
- Springer-Verlag
- Projects
- Spot
- Date
- 2009-01-01

## Abstract

In the automata theoretic approach to model checkingchecking a state-space against a linear-time property can be done in time. When model checking under strong fairness hypotheses expressed as a Generalized Büchi automaton, this complexity becomes .par Here we describe an algorithm to check the emptiness of Streett automata, which allows model checking under strong fairness hypotheses in . 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.

## Documents

## Bibtex (lrde.bib)

@InProceedings{ duret.09.atva, author = {Alexandre Duret-Lutz and Denis Poitrenaud and Jean-Michel Couvreur}, title = {On-the-fly Emptiness Check of Transition-based {S}treett Automata}, booktitle = {Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09)}, year = 2009, editor = {Zhiming Liu and Anders P. Ravn}, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, pages = {213--227}, volume = 5799, 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\"uchi automaton, this complexity becomes $\mathrm{O}(|S|\times 2^{\mathrm{O}(|\varphi|+n)})$.\par 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.}, doi = {10.1007/978-3-642-04761-9_17} }