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

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 $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)})$.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.

Documents

• Paper

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