TY - GEN
T1 - The Hanoi Omega-Automata format
AU - Babiak, Tomáš
AU - Blahoudek, František
AU - Duret-Lutz, Alexandre
AU - Klein, Joachim
AU - Křetínský, Jan
AU - Müller, David
AU - Parker, David
AU - Strejček, Jan
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2015.
PY - 2015
Y1 - 2015
N2 - We propose a flexible exchange format for ω-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 Büchi, 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.
AB - We propose a flexible exchange format for ω-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 Büchi, 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.
UR - http://www.scopus.com/inward/record.url?scp=84951002356&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-21690-4_31
DO - 10.1007/978-3-319-21690-4_31
M3 - Conference contribution
AN - SCOPUS:84951002356
SN - 9783319216898
SN - 9783319216898
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 479
EP - 486
BT - Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings
A2 - Pasareanu, Corina S.
A2 - Kroening, Daniel
A2 - Pasareanu, Corina S.
A2 - Kroening, Daniel
PB - Springer Verlag
T2 - 27th International Conference on Computer Aided Verification, CAV 2015
Y2 - 18 July 2015 through 24 July 2015
ER -