D 2012

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

BABIAK, Tomáš, Mojmír KŘETÍNSKÝ, Vojtěch ŘEHÁK a Jan STREJČEK

Základní údaje

Originální název

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

Název česky

Překlad LTL na Büchiho automaty: rychle a determinističtěji

Autoři

BABIAK, Tomáš (203 Česká republika, garant, domácí), Mojmír KŘETÍNSKÝ (203 Česká republika, domácí), Vojtěch ŘEHÁK (203 Česká republika, domácí) a Jan STREJČEK (203 Česká republika, domácí)

Vydání

Berlin, Heidelberg, TACAS 2012: 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, od s. 95-109, 15 s. 2012

Nakladatel

Springer-Verlag

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

paměťový nosič (CD, DVD, flash disk)

Odkazy

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/12:00057222

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-28755-8

ISSN

DOI

Klíčová slova česky

Lineární temporální logika; Büchiho automaty

Klíčová slova anglicky

Linear Temporal Logic; Büchi Automata

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 9. 4. 2013 18:14, doc. RNDr. Vojtěch Řehák, Ph.D.

Anotace

ORIG CZ

V originále

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 formula where 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 competitive with the current version of SPOT, sometimes outperforming it substantially.

Česky

Představujeme vylepšení algoritmu Gastina a Oddouxe pro překlad LTL formulí na Büchiho automaty pomocí velmi slabých alternujících co-Büchiho automatů a zobecněných Büchiho automatů. Několik vylepšení je založeno na specifických vlastnostech formulí, kde každá cesta syntaktickým stromem obsahuje alespoň jeden operátor "eventually" a alespoň jeden operátor "always". Tato vylepšení vedou k rychlejšímu překladu a menším automatům. Další vylepšení redukují nedeterminismus produkovaných automatů. Ve skutečnosti modifikujeme všechno kroky původního algoritmu a jeho implementace známé pod názvem LTL2BA. Experimentální výsledky ukazují, že naše modifikace jsou vskutku vylepšeními. Díky nim se LTL2BA stává opět srovnatelným se současnou verzí překladače SPOT, někdy ho dokonce výrazně předčí.

Návaznosti

GAP202/10/1469, projekt VaV
Název: Formální metody pro analýzu a verifikaci komplexních systémů
Investor: Grantová agentura ČR, Formální metody pro analýzu a verifikaci komplexních systémů
GA201/09/1389, projekt VaV
Název: Verifikace a analýza velmi velkých počítačových systémů
Investor: Grantová agentura ČR, Verifikace a analýza velmi velkých počítačových systémů
GBP202/12/G061, projekt VaV
Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)
Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky
GD102/09/H042, projekt VaV
Název: Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů
Investor: Grantová agentura ČR, Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů
GPP202/12/P612, projekt VaV
Název: Formální verifikace stochastických systémů s reálným časem (Akronym: Formální verifikace stochastických systémů s reáln)
Investor: Grantová agentura ČR, Formální verifikace stochastických systémů s reálným časem
MSM0021622419, záměr
Název: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
MUNI/A/0758/2011, interní kód MU
Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)
Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0914/2009, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty