Compositional Approach to Suspension and Other Improvements to LTL Translation

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F13%3A00066141" target="_blank" >RIV/00216224:14330/13:00066141 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-642-39176-7_6" target="_blank" >http://dx.doi.org/10.1007/978-3-642-39176-7_6</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-642-39176-7_6" target="_blank" >10.1007/978-3-642-39176-7_6</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Compositional Approach to Suspension and Other Improvements to LTL Translation

Popis výsledku v původní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.

Název v anglickém jazyce

Compositional Approach to Suspension and Other Improvements to LTL Translation

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Centrum excelence - Institut teoretické informatiky (CE-ITI)</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2013

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Model Checking Software - 20th International Symposium, SPIN 2013

ISBN

9783642391750

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

18

Strana od-do

81-98

Název nakladatele

Springer

Místo vydání

Berlin Heidelberg

Místo konání akce

Stony Brook, NY, USA

Datum konání akce

1. 1. 2013

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—