The Hanoi Omega-Automata Format

Tomáš BabiakTomáš Babiak, František BlahoudekFrantišek Blahoudek, Alexandre Duret-LutzAlexandre Duret-Lutz, Joachim KleinJoachim Klein, Jan KřetínskýJan Křetínský, David MüllerDavid Müller, David ParkerDavid Parker, Jan StrejčekJan Strejček

DOI Link

Tomáš Babiak, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Křetínský, David Müller, David Parker, Jan Strejček
The Hanoi Omega-Automata Format
Proc. of the 27th Conference on Computer Aided Verification, Part I (CAV), volume 9206 of Lecture Notes in Computer Science, 479--486, 2015. Springer

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-21690-4_31.

@inproceedings{BBDKKMPS2015,
  author    = {Tom{\'{a}}{\v{s}} Babiak and Franti{\v{s}}ek Blahoudek and
               Alexandre Duret-Lutz and Joachim Klein and Jan
               K{\v{r}}et{\'{\i}}nsk{\'{y}} and David M{\"{u}}ller and David
               Parker and Jan Strej{\v{c}}ek},
  title     = {The Hanoi Omega-Automata Format},
  booktitle = {Proc. of the 27th Conference on Computer Aided Verification, Part
               I (CAV)},
  series    = {Lecture Notes in Computer Science},
  volume    = {9206},
  publisher = {Springer},
  year      = {2015},
  pages     = {479--486},
  doi       = {10.1007/978-3-319-21690-4_31}
}