The Hanoi Omega-Automata format

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

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

65 Scopus citations

Abstract

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.

Original languageEnglish
Title of host publicationComputer Aided Verification - 27th International Conference, CAV 2015, Proceedings
EditorsCorina S. Pasareanu, Daniel Kroening, Corina S. Pasareanu, Daniel Kroening
PublisherSpringer Verlag
Pages479-486
Number of pages8
ISBN (Print)9783319216898, 9783319216898
DOIs
StatePublished - 2015
Externally publishedYes
Event27th International Conference on Computer Aided Verification, CAV 2015 - San Francisco, United States
Duration: 18 Jul 201524 Jul 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9206
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference27th International Conference on Computer Aided Verification, CAV 2015
Country/TerritoryUnited States
CitySan Francisco
Period18/07/1524/07/15

Fingerprint

Dive into the research topics of 'The Hanoi Omega-Automata format'. Together they form a unique fingerprint.

Cite this