Rabinizer 2: Small Deterministic Automata for LTLGU

Kód výsledku v 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>
Výsledek na webu
<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>

Jazyk výsledku
angličtina
Název v původním jazyce
Rabinizer 2: Small Deterministic Automata for LTLGU
Popis výsledku v původním jazyce
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.
Název v anglickém jazyce
Rabinizer 2: Small Deterministic Automata for LTLGU
Popis výsledku anglicky
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.

Projekt
<a href="/cs/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Centrum excelence - Institut teoretické informatiky (CE-ITI)</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění
2013
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku
Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013
ISBN
9783319024431
ISSN
0302-9743
e-ISSN
—
Počet stran výsledku
5
Strana od-do
446-450
Název nakladatele
Springer
Místo vydání
Heidelberg Dordrecht London New York
Místo konání akce
Heidelberg Dordrecht London New York
Datum konání akce
1. 1. 2013
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—

Podobné výsledky(10)