The Hanoi Omega-Automata Format

D 2015

The Hanoi Omega-Automata Format

BABIAK, Tomáš, František BLAHOUDEK, Alexandre DURET-LUTZ, Joachim KLEIN, Jan KŘETÍNSKÝ et. al.

Basic information

Original name

The Hanoi Omega-Automata Format

Authors

BABIAK, Tomáš (703 Slovakia, belonging to the institution), František BLAHOUDEK (203 Czech Republic, belonging to the institution), Alexandre DURET-LUTZ (250 France), Joachim KLEIN (276 Germany), Jan KŘETÍNSKÝ (203 Czech Republic, guarantor, belonging to the institution), David MÜLLER (276 Germany), David PARKER (826 United Kingdom of Great Britain and Northern Ireland) and Jan STREJČEK (203 Czech Republic, belonging to the institution)

Edition

Cham, Computer Aided Verification: 27th International Conference, CAV 2015, p. 479-486, 8 pp. 2015

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Switzerland

Confidentiality degree

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

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/15:00080919

Organization unit

Faculty of Informatics

ISBN

978-3-319-21689-8

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-21690-4_31

UT WoS

000364182900031

Keywords in English

automata; infinite words; verification

Abstract

V originále

We propose a flexible exchange format for omega-automata, as typically used in formal verification, and implement support for it in a range of established tools. Our aim is to simplify the interaction of tools, helping the research community to build upon other people's work. A key feature of the format is the use of very generic acceptance conditions, specified by Boolean combinations of acceptance primitives, rather than being limited to common cases such as Buchi, Streett, or Rabin. Such flexibility in the choice of acceptance conditions can be exploited in applications, for example in probabilistic model checking, and furthermore encourages the development of acceptance-agnostic tools for automata manipulations. The format allows acceptance conditions that are either state-based or transition-based, and also supports alternating automata.

Links

GBP202/12/G061, research and development project

Name: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Acronym: CE-ITI)

Investor: Czech Science Foundation

MUNI/A/1159/2014, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV.

Investor: Masaryk University, Category A

MUNI/A/1206/2014, interní kód MU

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)

Investor: Masaryk University, Category A

Citovat

BABIAK, Tomáš, František BLAHOUDEK, Alexandre DURET-LUTZ, Joachim KLEIN, Jan KŘETÍNSKÝ, David MÜLLER, David PARKER and Jan STREJČEK. The Hanoi Omega-Automata Format. In Daniel Kroening, Corina Pasareanu. Computer Aided Verification: 27th International Conference, CAV 2015. Cham: Springer, 2015, p. 479-486. ISBN 978-3-319-21689-8. Available from: https://dx.doi.org/10.1007/978-3-319-21690-4_31.

@inproceedings{1306808,
   author = {Babiak, Tomáš and Blahoudek, František and DuretandLutz, Alexandre and Klein, Joachim and Křetínský, Jan and Müller, David and Parker, David and Strejček, Jan},
   address = {Cham},
   booktitle = {Computer Aided Verification: 27th International Conference, CAV 2015},
   doi = {http://dx.doi.org/10.1007/978-3-319-21690-4_31},
   editor = {Daniel Kroening, Corina Pasareanu},
   keywords = {automata; infinite words; verification},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-319-21689-8},
   pages = {479-486},
   publisher = {Springer},
   title = {The Hanoi Omega-Automata Format},
   year = {2015}
}

TY  - JOUR
ID  - 1306808
AU  - Babiak, Tomáš - Blahoudek, František - Duret-Lutz, Alexandre - Klein, Joachim - Křetínský, Jan - Müller, David - Parker, David - Strejček, Jan
PY  - 2015
TI  - The Hanoi Omega-Automata Format
PB  - Springer
CY  - Cham
SN  - 9783319216898
KW  - automata
KW  - infinite words
KW  - verification
N2  - We propose a flexible exchange format for omega-automata, as typically used in formal verification, and implement support for it in a range of established tools. Our aim is to simplify the interaction of tools, helping the research community to build upon other people's work. A key feature of the format is the use of very generic acceptance conditions, specified by Boolean combinations of acceptance primitives, rather than being limited to common cases such as Buchi, Streett, or Rabin. Such flexibility in the choice of acceptance conditions can be exploited in applications, for example in probabilistic model checking, and furthermore encourages the development of acceptance-agnostic tools for automata manipulations. The format allows acceptance conditions that are either state-based or transition-based, and also supports alternating automata.
ER  -

BABIAK, Tomáš, František BLAHOUDEK, Alexandre DURET-LUTZ, Joachim KLEIN, Jan KŘETÍNSKÝ, David MÜLLER, David PARKER and Jan STREJČEK. The Hanoi Omega-Automata Format. In Daniel Kroening, Corina Pasareanu. \textit{Computer Aided Verification: 27th International Conference, CAV 2015}. Cham: Springer, 2015, p.~479-486. ISBN~978-3-319-21689-8. Available from: https://dx.doi.org/10.1007/978-3-319-21690-4\_{}31.

Detailed Information on Publication Record