Almost linear Büchi automata

BABIAK, Tomáš; Jan STREJČEK and Vojtěch ŘEHÁK. Almost linear Büchi automata. Mathematical Structures in Computer Science. Cambridge: Cambridge University Press, 2012, vol. 22, No 2, p. 203-235. ISSN 0960-1295. Available from: https://dx.doi.org/10.1017/S0960129511000399.

Basic information

Original name

Almost linear Büchi automata

Name in Czech

Skoro lineární Büchiho automaty

Authors

BABIAK, Tomáš (703 Slovakia, belonging to the institution); Jan STREJČEK (203 Czech Republic, belonging to the institution) and Vojtěch ŘEHÁK (203 Czech Republic, guarantor, belonging to the institution)

Edition

Mathematical Structures in Computer Science, Cambridge, Cambridge University Press, 2012, 0960-1295

---

Other information

Language

English

Type of outcome

Article in a journal

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Czech Republic

Confidentiality degree

is not subject to a state or trade secret

References:

URL

Impact factor

Impact factor: 0.722

RIV identification code

RIV/00216224:14330/12:00057181

Organization unit

Faculty of Informatics

DOI

http://dx.doi.org/10.1017/S0960129511000399

UT WoS

000300844900004

Keywords (in Czech)

LTL; logiky lineárního času; ověřování modelu

Keywords in English

LTL; linear time logic; model checking

Tags

to appear

Tags

International impact, Reviewed

---

Abstract

In the original language

We introduce a new fragment of Linear temporal logic (LTL) called LIO and a new class of Büchi automata (BA) called Almost linear Büchi automata (ALBA). We provide effective translations between LIO and ALBA showing that the two formalisms are expressively equivalent. As we expect applications of our results in model checking, we use two standard sources of specification formulae, namely Spec Patterns and BEEM, to study practical relevance of LIO fragment, and to compare our translation of LIO to ALBA with two standard translations of LTL to BA via alternating automata. Finally, we demonstrate that the LIO to ALBA translation can be much faster than the standard translation and the produced automata can be substantially smaller.

In Czech

V článku zavádíme nový fragment logiky lineárního času (LTL) nazvaný LIO a dále také novou třídu Büchiho automatů (BA) nazývanou Almost linear Büchi automata (ALBA). Prezentujeme efektivní transformace mezi LIO a ALBA a ukazujeme tak, že tyto formalizmy mají stejnou vyjadřovací sílu. Protože očekáváme aplikace našich výsledků v oblasti model checkingu, používamé dva standardní zdroje specifikačních formulí (Spec Patterns a BEEM) k posouzení praktické relevance LIO fragmentu a k porovnání našeho překladu LIO na ALBA s dvojicí standardních překladů LTL na BA pomocí alternujících automatů. Na závěr ukazujeme, že překlad LIO na ALBA může být mnohem rychlejší než standardní překlad a může také produkovat podstatně menší automaty.

---

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
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
GP201/08/P375, research and development project	Name: Formální verifikace: algoritmy, vlastnosti modelovacích formalismů a temporálních logik Investor: Czech Science Foundation, Formal verification: algorithms, properties of modelling formalisms amd temporal logics
GP201/08/P459, research and development project	Name: Nové možnosti automatické verifikace síťových protokolů Investor: Czech Science Foundation, New possibilities in automatic verification of network protocols
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/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
1M0545, research and development project	Name: Institut Teoretické Informatiky Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science