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

From LRDE

Abstract

In the automata theoretic approach to model checkingchecking a state-space Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle S} against a linear-time property Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \varphi} can be done in Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathrm{O}(|S|\times 2^{\mathrm{O}(|\varphi|)})} time. When model checking under Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle n} strong fairness hypotheses expressed as a Generalized Büchi automaton, this complexity becomes Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\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 Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle n} strong fairness hypotheses in Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\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.

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