Difference between revisions of "Publications/duret.09.atva"
From LRDE
(7 intermediate revisions by 2 users not shown) | |||
Line 8: | Line 8: | ||
| series = Lecture Notes in Computer Science |
| series = Lecture Notes in Computer Science |
||
| publisher = Springer-Verlag |
| publisher = Springer-Verlag |
||
− | | pages = |
+ | | 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 |
+ | | abstract = In the automata theoretic approach to model checkingchecking a state-space <math>S</math> against a linear-time property <math>\varphi</math> can be done in <math>\mathrm{O}(|S|\times 2^{\mathrm{O}(|\varphi|)})</math> time. When model checking under <math>n</math> strong fairness hypotheses expressed as a Generalized Büchi automaton, this complexity becomes <math>\mathrm{O}(|S|\times 2^{\mathrm{O}(|\varphi|+n)})</math>.par Here we describe an algorithm to check the emptiness of Streett automata, which allows model checking under <math>n</math> strong fairness hypotheses in <math>\mathrm{O}(|S|\times 2^{\mathrm{O}(|\varphi|)}\times n)</math>. 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. |
| lrdepaper = http://www.lrde.epita.fr/dload/papers/duret.09.atva.pdf |
| lrdepaper = http://www.lrde.epita.fr/dload/papers/duret.09.atva.pdf |
||
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
| type = inproceedings |
| type = inproceedings |
||
| id = duret.09.atva |
| id = duret.09.atva |
||
+ | | identifier = doi:10.1007/978-3-642-04761-9_17 |
||
| bibtex = |
| bibtex = |
||
@InProceedings<nowiki>{</nowiki> duret.09.atva, |
@InProceedings<nowiki>{</nowiki> duret.09.atva, |
||
Line 32: | Line 33: | ||
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 $\mathrm<nowiki>{</nowiki>O<nowiki>}</nowiki>( |
+ | $\varphi$ can be done in $\mathrm<nowiki>{</nowiki>O<nowiki>}</nowiki>(|S|\times |
− | 2^<nowiki>{</nowiki>\mathrm<nowiki>{</nowiki>O<nowiki>}</nowiki>( |
+ | 2^<nowiki>{</nowiki>\mathrm<nowiki>{</nowiki>O<nowiki>}</nowiki>(|\varphi|)<nowiki>}</nowiki>)$ time. When model checking under |
$n$ strong fairness hypotheses expressed as a Generalized |
$n$ strong fairness hypotheses expressed as a Generalized |
||
B\"uchi automaton, this complexity becomes |
B\"uchi automaton, this complexity becomes |
||
− | $\mathrm<nowiki>{</nowiki>O<nowiki>}</nowiki>( |
+ | $\mathrm<nowiki>{</nowiki>O<nowiki>}</nowiki>(|S|\times 2^<nowiki>{</nowiki>\mathrm<nowiki>{</nowiki>O<nowiki>}</nowiki>(|\varphi|+n)<nowiki>}</nowiki>)$.\par |
Here we describe an algorithm to check the emptiness of |
Here we describe an algorithm to check the emptiness of |
||
Streett automata, which allows model checking under $n$ |
Streett automata, which allows model checking under $n$ |
||
− | strong fairness hypotheses in $\mathrm<nowiki>{</nowiki>O<nowiki>}</nowiki>( |
+ | strong fairness hypotheses in $\mathrm<nowiki>{</nowiki>O<nowiki>}</nowiki>(|S|\times |
− | 2^<nowiki>{</nowiki>\mathrm<nowiki>{</nowiki>O<nowiki>}</nowiki>( |
+ | 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 |
||
− | acceptance conditions into the state-space without any blowup.<nowiki>}</nowiki> |
+ | acceptance conditions into the state-space without any blowup.<nowiki>}</nowiki>, |
+ | doi = <nowiki>{</nowiki>10.1007/978-3-642-04761-9_17<nowiki>}</nowiki> |
||
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
||
Latest revision as of 11:30, 1 April 2019
- 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} }