LTL to Büchi Automata Translation: Fast and More Deterministic

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F12%3A00057222" target="_blank" >RIV/00216224:14330/12:00057222 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-642-28756-5_8" target="_blank" >http://dx.doi.org/10.1007/978-3-642-28756-5_8</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-642-28756-5_8" target="_blank" >10.1007/978-3-642-28756-5_8</a>

Jazyk výsledku

angličtina

Název v původním jazyce

LTL to Büchi Automata Translation: Fast and More Deterministic

Popis výsledku v původním jazyce

We introduce improvements in the algorithm by Gastin and Oddoux translating LTL formulae into Büchi automata via very weak alternating co-Büchi automata and generalized Büchi automata. Several improvements are based on specific properties of any formulawhere each branch of its syntax tree contains at least one eventually operator and at least one always operator. These changes usually result in faster translations and smaller automata. Other improvements reduce non-determinism in the produced automata.In fact, we modified all the steps of the original algorithm and its implementation known as LTL2BA. Experimental results show that our modifications are real improvements. Their implementations within an LTL2BA translation made LTL2BA very competitivewith the current version of SPOT, sometimes outperforming it substantially.

Název v anglickém jazyce

LTL to Büchi Automata Translation: Fast and More Deterministic

Popis výsledku anglicky

We introduce improvements in the algorithm by Gastin and Oddoux translating LTL formulae into Büchi automata via very weak alternating co-Büchi automata and generalized Büchi automata. Several improvements are based on specific properties of any formulawhere each branch of its syntax tree contains at least one eventually operator and at least one always operator. These changes usually result in faster translations and smaller automata. Other improvements reduce non-determinism in the produced automata.In fact, we modified all the steps of the original algorithm and its implementation known as LTL2BA. Experimental results show that our modifications are real improvements. Their implementations within an LTL2BA translation made LTL2BA very competitivewith the current version of SPOT, sometimes outperforming it substantially.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2012

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

TACAS 2012: 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems

ISBN

9783642287558

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

15

Strana od-do

95-109

Název nakladatele

Springer-Verlag

Místo vydání

Berlin, Heidelberg

Místo konání akce

Tallinn, Estonia

Datum konání akce

1. 1. 2012

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

WRD - Celosvětová akce

Kód UT WoS článku

—