Rabinizer 2: Small Deterministic Automata for LTLGU
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F13%3A00066204" target="_blank" >RIV/00216224:14330/13:00066204 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-319-02444-8_32" target="_blank" >http://dx.doi.org/10.1007/978-3-319-02444-8_32</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-02444-8_32" target="_blank" >10.1007/978-3-319-02444-8_32</a>
Alternative languages
Result language
angličtina
Original language name
Rabinizer 2: Small Deterministic Automata for LTLGU
Original language description
We present a tool that generates automata for LTL(X,F,G,U) where U does not occur in any G-formula (but F still can). The tool generates deterministic generalized Rabin automata (DGRA) significantly smaller than deterministic Rabin automata (DRA) generated by state-of-the-art tools. For complex properties such as fairness constraints, the difference is in orders of magnitude. DGRA have been recently shown to be as useful in probabilistic model checking as DRA, hence the difference in size directly translates to a speed up of the model checking procedures.
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
Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013
ISBN
9783319024431
ISSN
0302-9743
e-ISSN
—
Number of pages
5
Pages from-to
446-450
Publisher name
Springer
Place of publication
Heidelberg Dordrecht London New York
Event location
Heidelberg Dordrecht London New York
Event date
Jan 1, 2013
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—