The Hanoi Omega-Automata Format

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BABIAK Tomáš BLAHOUDEK František DURET-LUTZ Alexandre KLEIN Joachim KŘETÍNSKÝ Jan MÜLLER David PARKER David STREJČEK Jan

Year of publication 2015
Type Article in Proceedings
Conference Computer Aided Verification: 27th International Conference, CAV 2015
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-319-21690-4_31
Field Informatics
Keywords automata; infinite words; verification
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.