From LTL to Deterministic Automata: A Safraless Compositional Approach
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F14%3A00073709" target="_blank" >RIV/00216224:14330/14:00073709 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-319-08867-9_13" target="_blank" >http://dx.doi.org/10.1007/978-3-319-08867-9_13</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-08867-9_13" target="_blank" >10.1007/978-3-319-08867-9_13</a>
Alternative languages
Result language
angličtina
Original language name
From LTL to Deterministic Automata: A Safraless Compositional Approach
Original language description
We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula phi. The automaton is the product of a master automaton and an array of slave automata, one for each G-subformula of phi. The slave automaton for G(psi) is in charge of recognizing whether FG(psi) holds. As opposed to standard determinization procedures, the states of all our automata have a clear logical structure, which allows for various optimizations. Our construction subsumes former algorithms for fragments of LTL. Experimental results show improvement in the sizes of the resulting automata compared to existing methods.
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
2014
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
Computer Aided Verification - 26th International Conference, CAV 2014
ISBN
9783319088662
ISSN
0302-9743
e-ISSN
—
Number of pages
17
Pages from-to
192-208
Publisher name
Springer
Place of publication
Heidelberg Dordrecht London New York
Event location
Heidelberg Dordrecht London New York
Event date
Jan 1, 2014
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—