Difference between revisions of "Publications/duret.09.atva"
From LRDE
(Created page with "{{Publication | date = 2009-01-01 | authors = Alexandre Duret-Lutz, Denis Poitrenaud, Jean-Michel Couvreur | title = On-the-fly Emptiness Check of Transition-based Streett Aut...") |
|||
| Line 11: | Line 11: | ||
| 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 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. |
||
| urllrde = 200910-ATVA |
| urllrde = 200910-ATVA |
||
| + | | lrdepaper = http://www.lrde.epita.fr/dload/papers/duret.09.atva.pdf |
||
| type = inproceedings |
| type = inproceedings |
||
| id = duret.09.atva |
| id = duret.09.atva |
||
Revision as of 16:42, 22 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 RO(
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 $\RO(