| 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. |
|
Other formats:
BibTeX
LaTeX
RIS
|
| 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 | |
|---|---|
| Original language | English |
| Type of outcome | Proceedings paper |
| Field of Study | 10201 Computer sciences, information science, bioinformatics |
| Country of publisher | Italy |
| Confidentiality degree | is not subject to a state or trade secret |
| WWW | DOI |
| RIV identification code | RIV/00216224:14330/09:00029631 |
| Organization unit | Faculty of Informatics |
| ISSN | 2075-2180 |
| 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 |
| Changed by | Changed by: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Changed: 23/11/2009 16:12. |
| Abstract |
|---|
| 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. |
| Abstract (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 | |
PrintDisplayed: 25/4/2024 17:16