Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F14%3A00073720" target="_blank" >RIV/00216224:14330/14:00073720 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-319-11936-6_17" target="_blank" >http://dx.doi.org/10.1007/978-3-319-11936-6_17</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-11936-6_17" target="_blank" >10.1007/978-3-319-11936-6_17</a>
Alternative languages
Result language
angličtina
Original language name
Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata
Original language description
We present a tool for translating LTL formulae into deterministic automata. It is the first tool that covers the whole LTL, while not using Safra's determinization or any of its variants, which leads to smaller automata. There are several outputs of thetool: firstly, deterministic Rabin automata, which are the standard input for probabilistic model checking, e.g. for the probabilistic model-checker PRISM; secondly, deterministic generalized Rabin automata, which can also be used for probabilistic modelchecking and are sometimes by orders of magnitude smaller. We also link our tool to PRISM and show that this leads to a significant speed-up of probabilistic LTL model checking, especially with the generalized Rabin automata.
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
Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014
ISBN
9783319119359
ISSN
0302-9743
e-ISSN
—
Number of pages
7
Pages from-to
235-241
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
—