| Identifikační kód | RIV/00216224:14330/13:00066141 |
|---|
| Název v anglickém jazyce | Compositional Approach to Suspension and Other Improvements to LTL Translation |
|---|
| Druh | D - Článek ve sborníku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2013 |
|---|
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
|---|
| Počet výskytů výsledku | 2 |
|---|
| Počet tvůrců celkem | 5 |
|---|
| Počet domácích tvůrců | 3 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | Tomáš Babiak (státní příslušnost: SK - Slovenská republika, domácí tvůrce: A, vedidk: 9653023)
Thomas Badie (státní příslušnost: FR - Francouzská republika)
Alexandre Duret-Lutz (státní příslušnost: FR - Francouzská republika)
Mojmír Křetínský (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 5598095)
Jan Strejček (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 3978915) |
|---|
| Popis výsledku v anglickém jazyce | Recently, there was defined a fragment of LTL (containing fairness properties among other interesting formulae) whose validity over a given infinite word depends only on an arbitrary suffix of the word. Building upon an existing translation from LTL to Büchi automata, we introduce a compositional approach where subformulae of this fragment are translated separately from the rest of an input formula and the produced automata are composed in a way that the subformulae are checked only in relevant accepting strongly connected components of the final automaton. Further, we suggest improvements over some procedures commonly applied to generalized Büchi automata, namely over generalized acceptance simplification and over degeneralization. Finally we show howexisting simulation-based reductions can be implemented in a signature-based framework in a way that improves the determinism of the automaton. |
|---|
| Klíčová slova oddělená středníkem | linear time logic; model-checking; translation LTL to Buchi automata |
|---|
| Stránka www, na které se nachází výsledek | - |
|---|
| DOI výsledku | 10.1007/978-3-642-39176-7_6 |
|---|