Difference between revisions of "Publications/renault.13.tacas"
From LRDE
| (13 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
{{Publication |
{{Publication |
||
| − | | |
+ | | published = true |
| + | | date = 2013-01-08 |
||
| authors = Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud |
| authors = Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud |
||
| title = Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking |
| title = Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking |
||
| Line 10: | Line 11: | ||
| volume = 7795 |
| volume = 7795 |
||
| abstract = The automata-theoretic approach for model checking of linear-time temporal properties involves the emptiness check of a large Büchi automaton. Specialized emptiness-check algorithms have been proposed for the cases where the property is represented by a weak or terminal automaton. When the property automaton does not fall into these categories, a general emptiness check is required. This paper focuses on this class of properties. We refine previous approaches by classifying strongly-connected components rather than automata, and suggest a decomposition of the property automaton into three smaller automata capturing the terminal, weak, and the remaining strong behaviors of the property. The three corresponding emptiness checks can be performed independently, using the most appropriate algorithm. Such a decomposition approach can be used with any automata-based model checker. We illustrate the interest of this new approach using explicit and symbolic LTL model checkers. |
| abstract = The automata-theoretic approach for model checking of linear-time temporal properties involves the emptiness check of a large Büchi automaton. Specialized emptiness-check algorithms have been proposed for the cases where the property is represented by a weak or terminal automaton. When the property automaton does not fall into these categories, a general emptiness check is required. This paper focuses on this class of properties. We refine previous approaches by classifying strongly-connected components rather than automata, and suggest a decomposition of the property automaton into three smaller automata capturing the terminal, weak, and the remaining strong behaviors of the property. The three corresponding emptiness checks can be performed independently, using the most appropriate algorithm. Such a decomposition approach can be used with any automata-based model checker. We illustrate the interest of this new approach using explicit and symbolic LTL model checkers. |
||
| + | | lrdepaper = http://www.lrde.epita.fr/dload/papers/renault.13.tacas.pdf |
||
| − | | urllrde = 201303-TACAS |
||
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
| + | | lrdenewsdate = 2013-01-08 |
||
| type = inproceedings |
| type = inproceedings |
||
| id = renault.13.tacas |
| id = renault.13.tacas |
||
| + | | identifier = doi:10.1007/978-3-642-36742-7_42 |
||
| bibtex = |
| bibtex = |
||
@InProceedings<nowiki>{</nowiki> renault.13.tacas, |
@InProceedings<nowiki>{</nowiki> renault.13.tacas, |
||
author = <nowiki>{</nowiki>Etienne Renault and Alexandre Duret-Lutz and Fabrice |
author = <nowiki>{</nowiki>Etienne Renault and Alexandre Duret-Lutz and Fabrice |
||
Kordon and Denis Poitrenaud<nowiki>}</nowiki>, |
Kordon and Denis Poitrenaud<nowiki>}</nowiki>, |
||
| − | title = <nowiki>{</nowiki>Strength-Based Decomposition of the Property |
+ | title = <nowiki>{</nowiki>Strength-Based Decomposition of the Property <nowiki>{</nowiki>B\"u<nowiki>}</nowiki>chi |
Automaton for Faster Model Checking<nowiki>}</nowiki>, |
Automaton for Faster Model Checking<nowiki>}</nowiki>, |
||
booktitle = <nowiki>{</nowiki>Proceedings of the 19th International Conference on Tools |
booktitle = <nowiki>{</nowiki>Proceedings of the 19th International Conference on Tools |
||
| Line 24: | Line 27: | ||
(TACAS'13)<nowiki>}</nowiki>, |
(TACAS'13)<nowiki>}</nowiki>, |
||
editor = <nowiki>{</nowiki>Nir Piterman and Scott A. Smolka<nowiki>}</nowiki>, |
editor = <nowiki>{</nowiki>Nir Piterman and Scott A. Smolka<nowiki>}</nowiki>, |
||
| − | year = |
+ | year = 2013, |
month = mar, |
month = mar, |
||
pages = <nowiki>{</nowiki>580--593<nowiki>}</nowiki>, |
pages = <nowiki>{</nowiki>580--593<nowiki>}</nowiki>, |
||
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
||
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>, |
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>, |
||
| − | volume = |
+ | volume = 7795, |
abstract = <nowiki>{</nowiki>The automata-theoretic approach for model checking of |
abstract = <nowiki>{</nowiki>The automata-theoretic approach for model checking of |
||
linear-time temporal properties involves the emptiness |
linear-time temporal properties involves the emptiness |
||
| Line 35: | Line 38: | ||
emptiness-check algorithms have been proposed for the cases |
emptiness-check algorithms have been proposed for the cases |
||
where the property is represented by a weak or terminal |
where the property is represented by a weak or terminal |
||
| − | automaton. |
+ | automaton. When the property automaton does not fall into |
| ⚫ | |||
| − | |||
| ⚫ | |||
| − | When the property automaton does not fall into these |
||
| ⚫ | |||
| ⚫ | |||
previous approaches by classifying strongly-connected |
previous approaches by classifying strongly-connected |
||
components rather than automata, and suggest a |
components rather than automata, and suggest a |
||
| Line 46: | Line 47: | ||
strong behaviors of the property. The three corresponding |
strong behaviors of the property. The three corresponding |
||
emptiness checks can be performed independently, using the |
emptiness checks can be performed independently, using the |
||
| − | most appropriate algorithm. |
+ | most appropriate algorithm. Such a decomposition approach |
| ⚫ | |||
| − | |||
| ⚫ | |||
| − | Such a decomposition approach can be used with any |
||
| ⚫ | |||
| ⚫ | |||
| ⚫ | |||
| ⚫ | |||
| ⚫ | |||
| ⚫ | |||
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
||
Latest revision as of 11:30, 1 April 2019
- Authors
- Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud
- Where
- Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13)
- Type
- inproceedings
- Publisher
- Springer
- Projects
- Spot
- Date
- 2013-01-08
Abstract
The automata-theoretic approach for model checking of linear-time temporal properties involves the emptiness check of a large Büchi automaton. Specialized emptiness-check algorithms have been proposed for the cases where the property is represented by a weak or terminal automaton. When the property automaton does not fall into these categories, a general emptiness check is required. This paper focuses on this class of properties. We refine previous approaches by classifying strongly-connected components rather than automata, and suggest a decomposition of the property automaton into three smaller automata capturing the terminal, weak, and the remaining strong behaviors of the property. The three corresponding emptiness checks can be performed independently, using the most appropriate algorithm. Such a decomposition approach can be used with any automata-based model checker. We illustrate the interest of this new approach using explicit and symbolic LTL model checkers.
Documents
Bibtex (lrde.bib)
@InProceedings{ renault.13.tacas,
author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice
Kordon and Denis Poitrenaud},
title = {Strength-Based Decomposition of the Property {B\"u}chi
Automaton for Faster Model Checking},
booktitle = {Proceedings of the 19th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems
(TACAS'13)},
editor = {Nir Piterman and Scott A. Smolka},
year = 2013,
month = mar,
pages = {580--593},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 7795,
abstract = {The automata-theoretic approach for model checking of
linear-time temporal properties involves the emptiness
check of a large B{\"u}chi automaton. Specialized
emptiness-check algorithms have been proposed for the cases
where the property is represented by a weak or terminal
automaton. When the property automaton does not fall into
these categories, a general emptiness check is required.
This paper focuses on this class of properties. We refine
previous approaches by classifying strongly-connected
components rather than automata, and suggest a
decomposition of the property automaton into three smaller
automata capturing the terminal, weak, and the remaining
strong behaviors of the property. The three corresponding
emptiness checks can be performed independently, using the
most appropriate algorithm. Such a decomposition approach
can be used with any automata-based model checker. We
illustrate the interest of this new approach using explicit
and symbolic LTL model checkers.},
doi = {10.1007/978-3-642-36742-7_42}
}