Almost Linear Büchi Automata

BABIAK, Tomáš, Vojtěch ŘEHÁK and Jan STREJČEK. Almost Linear Büchi Automata. In Proceedings 16th International Workshop on Expressiveness in Concurrency 2009 (EXPRESS'09). 1st ed. internet: EPTCS, 2009, p. 16-25. ISSN 2075-2180.

Basic information

Original name

Almost Linear Büchi Automata

Name in Czech

Skoro lineární Büchiho automaty

Authors

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

Edition

1st ed. internet, Proceedings 16th International Workshop on Expressiveness in Concurrency 2009 (EXPRESS'09), p. 16-25, 10 pp. 2009

Publisher

EPTCS

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Italy

Confidentiality degree

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

References:

DOI

RIV identification code

RIV/00216224:14330/09:00029631

Organization unit

Faculty of Informatics

ISSN

Keywords (in Czech)

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

Keywords in English

LTL; linear time logic; model checking

Tags

linear time logic, Model checking

Tags

International impact, Reviewed

---

Abstract

V originále

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. While standard translations of LTL into BA use some intermediate formalisms, the presented translation of LIO into ALBA is direct. As we expect applications of ALBA in model checking, we compare the expressiveness of ALBA with other classes of Büchi automata studied in this context and we indicate possible applications.

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 Skoro lineární automaty (ALBA). Předvádíme efektivní transformaci mezi LIO a ALBA a ukazujeme tak, že tyto formalizmy mají stejnou vyjadřovací sílu. Naproti tomu, že standardní transformace LTL do BA používá pomocného meziformalizmu, naše transformace LIO na ALBA je přímá. Protože očekáváme praktické uplatnění ALBA v ověřování modelů, srovnáváme též vyjadřovací sílu ALBA s dalšími třídami BA.

---

Links

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
1M0545, research and development project	Name: Institut Teoretické Informatiky Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science