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

## Abstract

In the automata theoretic approach to model checkingchecking a state-space ${\displaystyle S}$ against a linear-time property ${\displaystyle \varphi }$ can be done in ${\displaystyle \mathrm {O} (|S|\times 2^{\mathrm {O} (|\varphi |)})}$ time. When model checking under ${\displaystyle n}$ strong fairness hypotheses expressed as a Generalized Büchi automaton, this complexity becomes ${\displaystyle \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 ${\displaystyle n}$ strong fairness hypotheses in ${\displaystyle \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.

## 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}
}