Difference between revisions of "Publications/xu.18.seminar"
From LRDE
(Created page with "{{CSIReport | authors = Laurent XU | title = Efficient Translation of Fairness LTL Formulae into Deterministic Automata | year = 2018 | number = 1802 | abstract = In the autom...") |
|||
| Line 4: | Line 4: | ||
| year = 2018 |
| year = 2018 |
||
| number = 1802 |
| number = 1802 |
||
| − | | abstract = In the automata-theoretic approach to Linear Temporal Logic (LTL) model checking, the negation of an LTL formula is translated into an <math>\omega</math>-automaton. The construction of a smaller automaton reduces a lot the runtime and the memory consumption of the subsequent operations in the model checking pipeline. Müller and Sickert presented an efficient method to translate any LTL formula into a small deterministic automaton. |
+ | | abstract = In the automata-theoretic approach to Linear Temporal Logic (LTL) model checking, the negation of an LTL formula is translated into an <math>\omega</math>-automaton. The construction of a smaller automaton reduces a lot the runtime and the memory consumption of the subsequent operations in the model checking pipeline. Müller and Sickert presented an efficient method to translate any LTL formula into a small deterministic automaton. This method consists in splitting the formula into three sets of subformulae which are respectively taken from the (co-)safety fragment, the fairness fragment and the rest. Then they translate all sets of subformulae apart from each other into deterministic automata and they combine these resulting automata. Spot can already translate obligation formulae into minimal deterministic automata. Since obligation formulae are a superset of (co-)safety formulae, we replace the (co-)safety fragment by the obligation fragment to generalize the translation of Müller and Sickert. Concerning the fairness fragment, they showed an efficient translation algorithm that produces small deterministic automata. They also showed a method to compute an efficient product of these automata with other automata. We present how these two methods are implemented in Spot. |
| type = techreport |
| type = techreport |
||
| id = xu.18.seminar |
| id = xu.18.seminar |
||
Latest revision as of 12:44, 27 February 2018
- Authors
- Laurent XU
- Type
- techreport
- Year
- 2018
- Number
- 1802
Abstract
In the automata-theoretic approach to Linear Temporal Logic (LTL) model checking, the negation of an LTL formula is translated into an -automaton. The construction of a smaller automaton reduces a lot the runtime and the memory consumption of the subsequent operations in the model checking pipeline. Müller and Sickert presented an efficient method to translate any LTL formula into a small deterministic automaton. This method consists in splitting the formula into three sets of subformulae which are respectively taken from the (co-)safety fragment, the fairness fragment and the rest. Then they translate all sets of subformulae apart from each other into deterministic automata and they combine these resulting automata. Spot can already translate obligation formulae into minimal deterministic automata. Since obligation formulae are a superset of (co-)safety formulae, we replace the (co-)safety fragment by the obligation fragment to generalize the translation of Müller and Sickert. Concerning the fairness fragment, they showed an efficient translation algorithm that produces small deterministic automata. They also showed a method to compute an efficient product of these automata with other automata. We present how these two methods are implemented in Spot.
