Difference between revisions of "Publications/duret.09.atva"

From LRDE
Line 9: Line 9:
 
| pages = 213 to 227
  
| pages = 213 to 227
 
| volume = 5799
  
| volume = 5799
−
| abstract = In the automata theoretic approach to model checkingchecking a state-space S against a linear-time property φ can be done in RO(|S|times 2^RO(|φ|)) time. When model checking under n strong fairness hypotheses expressed as a Generalized Büchi automaton, this complexity becomes RO(|S|times 2^RO(|φ|+n)).par Here we describe an algorithm to check the emptiness of Streett automata, which allows model checking under n strong fairness hypotheses in RO(|S|times 2^RO(|φ|)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.
 +
| abstract = In the automata theoretic approach to model checkingchecking a state-space S against a linear-time property φ can be done in O(|S|times 2^O(|φ|)) time. When model checking under n strong fairness hypotheses expressed as a Generalized Büchi automaton, this complexity becomes O(|S|times 2^O(|φ|+n)).par Here we describe an algorithm to check the emptiness of Streett automata, which allows model checking under n strong fairness hypotheses in O(|S|times 2^mathrmO(|φ|)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.
 
| urllrde = 200910-ATVA
  
| urllrde = 200910-ATVA
 
| lrdepaper = http://www.lrde.epita.fr/dload/papers/duret.09.atva.pdf
  
| lrdepaper = http://www.lrde.epita.fr/dload/papers/duret.09.atva.pdf
Line 31: Line 31:
 
abstract = <nowiki>{</nowiki>In the automata theoretic approach to model checking,
  
abstract = <nowiki>{</nowiki>In the automata theoretic approach to model checking,
 
checking a state-space $S$ against a linear-time property
  
checking a state-space $S$ against a linear-time property
−
$\varphi$ can be done in $\RO(|S|\times
 +
$\varphi$ can be done in $\mathrm<nowiki>{</nowiki>O<nowiki>}</nowiki>(|S|\times
−
2^<nowiki>{</nowiki>\RO(|\varphi|)<nowiki>}</nowiki>)$ time. When model checking under $n$
 +
2^<nowiki>{</nowiki>\mathrm<nowiki>{</nowiki>O<nowiki>}</nowiki>(|\varphi|)<nowiki>}</nowiki>)$ time. When model checking under
−
strong fairness hypotheses expressed as a Generalized
 +
$n$ strong fairness hypotheses expressed as a Generalized
−
B\"uchi automaton, this complexity becomes $\RO(|S|\times
 +
B\"uchi automaton, this complexity becomes
−
2^<nowiki>{</nowiki>\RO(|\varphi|+n)<nowiki>}</nowiki>)$.\par Here we describe an algorithm
 +
$\mathrm<nowiki>{</nowiki>O<nowiki>}</nowiki>(|S|\times 2^<nowiki>{</nowiki>\mathrm<nowiki>{</nowiki>O<nowiki>}</nowiki>(|\varphi|+n)<nowiki>}</nowiki>)$.\par
−
to check the emptiness of Streett automata, which allows
 +
Here we describe an algorithm to check the emptiness of
−
model checking under $n$ strong fairness hypotheses in
 +
Streett automata, which allows model checking under $n$
−
$\RO(|S|\times 2^<nowiki>{</nowiki>\RO(|\varphi|)<nowiki>}</nowiki>\times n)$. We focus on
 +
strong fairness hypotheses in $\mathrm<nowiki>{</nowiki>O<nowiki>}</nowiki>(|S|\times
  +
2^<nowiki>{</nowiki>\mathrm<nowiki>{</nowiki>O<nowiki>}</nowiki>(|\varphi|)<nowiki>}</nowiki>\times n)$. We focus on
 
transition-based Streett automata, because it allows us to
  
transition-based Streett automata, because it allows us to
 
express strong fairness hypotheses by injecting Streett
  
express strong fairness hypotheses by injecting Streett

Revision as of 15:30, 25 October 2013

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
Date
2009-01-01

Abstract

In the automata theoretic approach to model checkingchecking a state-space S against a linear-time property φ can be done in O(

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






Retrieved from "https://www.lrde.epita.fr/index.php?title=Publications/duret.09.atva&oldid=5188"