D 2012

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

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

Basic information

Original name

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

Name in Czech

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

Authors

BABIAK, Tomáš (203 Czech Republic, guarantor, belonging to the institution), Mojmír KŘETÍNSKÝ (203 Czech Republic, belonging to the institution), Vojtěch ŘEHÁK (203 Czech Republic, belonging to the institution) and Jan STREJČEK (203 Czech Republic, belonging to the institution)

Edition

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

Publisher

Springer-Verlag

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

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

Publication form

storage medium (CD, DVD, flash disk)

References:

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/12:00057222

Organization unit

Faculty of Informatics

ISBN

978-3-642-28755-8

ISSN

DOI

Keywords (in Czech)

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

Keywords in English

Linear Temporal Logic; Büchi Automata

Tags

International impact, Reviewed
Změněno: 9/4/2013 18:14, doc. RNDr. Vojtěch Řehák, Ph.D.

Abstract

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.

In Czech

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čí.

Links

GAP202/10/1469, research and development project
Name: Formální metody pro analýzu a verifikaci komplexních systémů
Investor: Czech Science Foundation
GA201/09/1389, research and development project
Name: Verifikace a analýza velmi velkých počítačových systémů
Investor: Czech Science Foundation, Verification and Analysis of Large-Scale Computer Systems
GBP202/12/G061, research and development project
Name: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Acronym: CE-ITI)
Investor: Czech Science Foundation
GD102/09/H042, research and development project
Name: 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: Czech Science Foundation
GPP202/12/P612, research and development project
Name: Formální verifikace stochastických systémů s reálným časem (Acronym: Formální verifikace stochastických systémů s reáln)
Investor: Czech Science Foundation
MSM0021622419, plan (intention)
Name: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems
MUNI/A/0758/2011, interní kód MU
Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)
Investor: Masaryk University, Category A
MUNI/A/0914/2009, interní kód MU
Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Acronym: SV-FI MAV)
Investor: Masaryk University, Category A