Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

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í

2014

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 - 12th International Symposium, ATVA 2014

ISBN

9783319119359

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

7

Strana od-do

235-241

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. 2014

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—