From LTL to Deterministic Automata: A Safraless Compositional Approach

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F14%3A00073709" target="_blank" >RIV/00216224:14330/14:00073709 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-319-08867-9_13" target="_blank" >http://dx.doi.org/10.1007/978-3-319-08867-9_13</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-08867-9_13" target="_blank" >10.1007/978-3-319-08867-9_13</a>

Jazyk výsledku

angličtina

Název v původním jazyce

From LTL to Deterministic Automata: A Safraless Compositional Approach

Popis výsledku v původním jazyce

We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula phi. The automaton is the product of a master automaton and an array of slave automata, one for each G-subformula of phi. The slave automaton for G(psi) is in charge of recognizing whether FG(psi) holds. As opposed to standard determinization procedures, the states of all our automata have a clear logical structure, which allows for various optimizations. Our construction subsumes former algorithms for fragments of LTL. Experimental results show improvement in the sizes of the resulting automata compared to existing methods.

Název v anglickém jazyce

From LTL to Deterministic Automata: A Safraless Compositional Approach

Popis výsledku anglicky

We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula phi. The automaton is the product of a master automaton and an array of slave automata, one for each G-subformula of phi. The slave automaton for G(psi) is in charge of recognizing whether FG(psi) holds. As opposed to standard determinization procedures, the states of all our automata have a clear logical structure, which allows for various optimizations. Our construction subsumes former algorithms for fragments of LTL. Experimental results show improvement in the sizes of the resulting automata compared to existing methods.

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

Computer Aided Verification - 26th International Conference, CAV 2014

ISBN

9783319088662

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

17

Strana od-do

192-208

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

—