Compositional Approach to Suspension and Other Improvements to LTL Translation
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Compositional Approach to Suspension and Other Improvements to LTL Translation
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Center of excellence - Institute for theoretical computer science (CE-ITI)</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach
Others
Publication year
2013
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Model Checking Software - 20th International Symposium, SPIN 2013
ISBN
9783642391750
ISSN
0302-9743
e-ISSN
—
Number of pages
18
Pages from-to
81-98
Publisher name
Springer
Place of publication
Berlin Heidelberg
Event location
Stony Brook, NY, USA
Event date
Jan 1, 2013
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—