Difference between revisions of "Publications/duret.14.ijccbs"
From LRDE
| (6 intermediate revisions by the same user not shown) | |||
| Line 11: | Line 11: | ||
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
| lrdenewsdate = 2014-03-06 |
| lrdenewsdate = 2014-03-06 |
||
| ⚫ | | abstract = Spot is a library of model-checking algorithms started in 2003. This paper focuses on its module for translating linear-time temporal logic (LTL) formulas into Büchi automata: one of the steps required in the automata-theoretic approach to LTL model-checking. We detail the different algorithms involved in this translation: the core translation itself, which performs many simplifications thanks to its use of binary decision diagrams; the pre-processing of the LTL formulas with rewriting rules chosen to help their translation; and various post-processing algorithms whose use depends on the intent of the translation: do we favor deterministic automata, or small automata? Using different benchmarks, we show how Spot competes with other LTL translators, and how it has improved over the years. |
||
| − | | urllrde = 201403-IJCCBS |
||
| ⚫ | | abstract = Spot is a library of model-checking algorithms started in 2003. This paper focuses on its module for translating linear-time temporal logic (LTL) formulas into Büchi automata: one of the steps required in the automata-theoretic approach to LTL model-checking. |
||
| type = article |
| type = article |
||
| id = duret.14.ijccbs |
| id = duret.14.ijccbs |
||
| + | | identifier = doi:10.1504/IJCCBS.2014.059594 |
||
| bibtex = |
| bibtex = |
||
@Article<nowiki>{</nowiki> duret.14.ijccbs, |
@Article<nowiki>{</nowiki> duret.14.ijccbs, |
||
| Line 39: | Line 39: | ||
automata, or small automata? Using different benchmarks, we |
automata, or small automata? Using different benchmarks, we |
||
show how Spot competes with other LTL translators, and how |
show how Spot competes with other LTL translators, and how |
||
| − | it has improved over the years.<nowiki>}</nowiki> |
+ | it has improved over the years.<nowiki>}</nowiki>, |
| + | doi = <nowiki>{</nowiki>10.1504/IJCCBS.2014.059594<nowiki>}</nowiki> |
||
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
||
Latest revision as of 11:30, 1 April 2019
- Authors
- Alexandre Duret-Lutz
- Journal
- International Journal on Critical Computer-Based Systems
- Type
- article
- Projects
- Spot
- Date
- 2014-03-06
Abstract
Spot is a library of model-checking algorithms started in 2003. This paper focuses on its module for translating linear-time temporal logic (LTL) formulas into Büchi automata: one of the steps required in the automata-theoretic approach to LTL model-checking. We detail the different algorithms involved in this translation: the core translation itself, which performs many simplifications thanks to its use of binary decision diagrams; the pre-processing of the LTL formulas with rewriting rules chosen to help their translation; and various post-processing algorithms whose use depends on the intent of the translation: do we favor deterministic automata, or small automata? Using different benchmarks, we show how Spot competes with other LTL translators, and how it has improved over the years.
Documents
Bibtex (lrde.bib)
@Article{ duret.14.ijccbs,
author = {Alexandre Duret-Lutz},
title = {{LTL} Translation Improvements in {S}pot 1.0},
journal = {International Journal on Critical Computer-Based Systems},
year = 2014,
volume = 5,
number = {1/2},
pages = {31--54},
month = mar,
abstract = { Spot is a library of model-checking algorithms started in
2003. This paper focuses on its module for translating
linear-time temporal logic (LTL) formulas into B{\"u}chi
automata: one of the steps required in the
automata-theoretic approach to LTL model-checking. We
detail the different algorithms involved in this
translation: the core translation itself, which performs
many simplifications thanks to its use of binary decision
diagrams; the pre-processing of the LTL formulas with
rewriting rules chosen to help their translation; and
various post-processing algorithms whose use depends on the
intent of the translation: do we favor deterministic
automata, or small automata? Using different benchmarks, we
show how Spot competes with other LTL translators, and how
it has improved over the years.},
doi = {10.1504/IJCCBS.2014.059594}
}