Difference between revisions of "Publications/duret.14.ijccbs"
From LRDE
(Created page with "{{Publication | published = true | date = 2014-03-06 | authors = Alexandre Duret-Lutz | title = LTL Translation Improvements in Spot 1.0 | journal = International Journal on C...") |
|||
| Line 12: | Line 12: | ||
| lrdenewsdate = 2014-03-06 |
| lrdenewsdate = 2014-03-06 |
||
| urllrde = 201403-IJCCBS |
| 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. 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 |
+ | | 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 benchmarkswe show how Spot competes with other LTL translators, and how it has improved over the years. |
| type = article |
| type = article |
||
| id = duret.14.ijccbs |
| id = duret.14.ijccbs |
||
| Line 20: | Line 20: | ||
title = <nowiki>{</nowiki><nowiki>{</nowiki>LTL<nowiki>}</nowiki> Translation Improvements in <nowiki>{</nowiki>S<nowiki>}</nowiki>pot 1.0<nowiki>}</nowiki>, |
title = <nowiki>{</nowiki><nowiki>{</nowiki>LTL<nowiki>}</nowiki> Translation Improvements in <nowiki>{</nowiki>S<nowiki>}</nowiki>pot 1.0<nowiki>}</nowiki>, |
||
journal = <nowiki>{</nowiki>International Journal on Critical Computer-Based Systems<nowiki>}</nowiki>, |
journal = <nowiki>{</nowiki>International Journal on Critical Computer-Based Systems<nowiki>}</nowiki>, |
||
| − | year = |
+ | year = 2014, |
| − | volume = |
+ | volume = 5, |
number = <nowiki>{</nowiki>1/2<nowiki>}</nowiki>, |
number = <nowiki>{</nowiki>1/2<nowiki>}</nowiki>, |
||
pages = <nowiki>{</nowiki>31--54<nowiki>}</nowiki>, |
pages = <nowiki>{</nowiki>31--54<nowiki>}</nowiki>, |
||
| Line 29: | Line 29: | ||
linear-time temporal logic (LTL) formulas into B<nowiki>{</nowiki>\"u<nowiki>}</nowiki>chi |
linear-time temporal logic (LTL) formulas into B<nowiki>{</nowiki>\"u<nowiki>}</nowiki>chi |
||
automata: one of the steps required in the |
automata: one of the steps required in the |
||
| − | automata-theoretic approach to LTL model-checking. |
+ | automata-theoretic approach to LTL model-checking. We |
| ⚫ | |||
| − | |||
| ⚫ | |||
translation: the core translation itself, which performs |
translation: the core translation itself, which performs |
||
many simplifications thanks to its use of binary decision |
many simplifications thanks to its use of binary decision |
||
| Line 38: | Line 37: | ||
various post-processing algorithms whose use depends on the |
various post-processing algorithms whose use depends on the |
||
intent of the translation: do we favor deterministic |
intent of the translation: do we favor deterministic |
||
| − | automata, or small automata? |
+ | automata, or small automata? Using different benchmarks, we |
| + | show how Spot competes with other LTL translators, and how |
||
| − | |||
| ⚫ | |||
| − | Using different benchmarks, we show how Spot competes with |
||
| − | other LTL translators, and how it has improved over the |
||
| ⚫ | |||
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
||
Revision as of 09:01, 25 June 2014
- 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 benchmarkswe 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.}
}