Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F13%3A00066175" target="_blank" >RIV/00216224:14330/13:00066175 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-319-02444-8_4" target="_blank" >http://dx.doi.org/10.1007/978-3-319-02444-8_4</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-02444-8_4" target="_blank" >10.1007/978-3-319-02444-8_4</a>
Alternative languages
Result language
angličtina
Original language name
Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment
Original language description
Some applications of linear temporal logic (LTL) require to translate formulae of the logic to deterministic omega-automata. There are currently two translators producing deterministic automata: ltl2dstar working for the whole LTL and Rabinizer applicable to the fragment LTL(F,G). We present a new translation to deterministic Rabin automata via alternating automata and deterministic transition-based generalized Rabin automata. Our translation applies to a fragment that is strictly larger than LTL(F,G).Experimental results show that our algorithm can produce significantly smaller automata compared to Rabinizer and ltl2dstar, especially for more complex LTL formulae.
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<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
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
11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013
ISBN
9783319024431
ISSN
0302-9743
e-ISSN
—
Number of pages
15
Pages from-to
24-38
Publisher name
Springer
Place of publication
Berlin Heidelberg
Event location
Hanoi, Vietnam
Event date
Jan 1, 2013
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—