---
_id: '1601'
abstract:
- lang: eng
  text: 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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Tomáš
  full_name: Babiak, Tomáš
  last_name: Babiak
- first_name: František
  full_name: Blahoudek, František
  last_name: Blahoudek
- first_name: Alexandre
  full_name: Duret Lutz, Alexandre
  last_name: Duret Lutz
- first_name: Joachim
  full_name: Klein, Joachim
  last_name: Klein
- first_name: Jan
  full_name: Kretinsky, Jan
  id: 44CEF464-F248-11E8-B48F-1D18A9856A87
  last_name: Kretinsky
  orcid: 0000-0002-8122-2881
- first_name: Daniel
  full_name: Mueller, Daniel
  last_name: Mueller
- first_name: David
  full_name: Parker, David
  last_name: Parker
- first_name: Jan
  full_name: Strejček, Jan
  last_name: Strejček
citation:
  ama: 'Babiak T, Blahoudek F, Duret Lutz A, et al. The Hanoi omega-automata format.
    In: Vol 9206. Springer; 2015:479-486. doi:<a href="https://doi.org/10.1007/978-3-319-21690-4_31">10.1007/978-3-319-21690-4_31</a>'
  apa: 'Babiak, T., Blahoudek, F., Duret Lutz, A., Klein, J., Kretinsky, J., Mueller,
    D., … Strejček, J. (2015). The Hanoi omega-automata format (Vol. 9206, pp. 479–486).
    Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States:
    Springer. <a href="https://doi.org/10.1007/978-3-319-21690-4_31">https://doi.org/10.1007/978-3-319-21690-4_31</a>'
  chicago: Babiak, Tomáš, František Blahoudek, Alexandre Duret Lutz, Joachim Klein,
    Jan Kretinsky, Daniel Mueller, David Parker, and Jan Strejček. “The Hanoi Omega-Automata
    Format,” 9206:479–86. Springer, 2015. <a href="https://doi.org/10.1007/978-3-319-21690-4_31">https://doi.org/10.1007/978-3-319-21690-4_31</a>.
  ieee: 'T. Babiak <i>et al.</i>, “The Hanoi omega-automata format,” presented at
    the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015,
    vol. 9206, pp. 479–486.'
  ista: 'Babiak T, Blahoudek F, Duret Lutz A, Klein J, Kretinsky J, Mueller D, Parker
    D, Strejček J. 2015. The Hanoi omega-automata format. CAV: Computer Aided Verification,
    LNCS, vol. 9206, 479–486.'
  mla: Babiak, Tomáš, et al. <i>The Hanoi Omega-Automata Format</i>. Vol. 9206, Springer,
    2015, pp. 479–86, doi:<a href="https://doi.org/10.1007/978-3-319-21690-4_31">10.1007/978-3-319-21690-4_31</a>.
  short: T. Babiak, F. Blahoudek, A. Duret Lutz, J. Klein, J. Kretinsky, D. Mueller,
    D. Parker, J. Strejček, in:, Springer, 2015, pp. 479–486.
conference:
  end_date: 2015-07-24
  location: San Francisco, CA, United States
  name: 'CAV: Computer Aided Verification'
  start_date: 2015-07-18
date_created: 2018-12-11T11:52:57Z
date_published: 2015-07-16T00:00:00Z
date_updated: 2025-09-23T13:50:55Z
day: '16'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-319-21690-4_31
ec_funded: 1
external_id:
  isi:
  - '000364182900031'
file:
- access_level: open_access
  checksum: 5885236fa88a439baba9ac6f3e801e93
  content_type: application/pdf
  creator: dernst
  date_created: 2020-05-15T08:38:12Z
  date_updated: 2020-07-14T12:45:04Z
  file_id: '7850'
  file_name: 2015_CAV_Babiak.pdf
  file_size: 1651779
  relation: main_file
file_date_updated: 2020-07-14T12:45:04Z
has_accepted_license: '1'
intvolume: '      9206'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 479 - 486
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: Formal methods for the design and analysis of complex systems
- _id: 25681D80-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '291734'
  name: International IST Postdoc Fellowship Programme
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
publication_status: published
publisher: Springer
publist_id: '5566'
quality_controlled: '1'
scopus_import: '1'
status: public
title: The Hanoi omega-automata format
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9206
year: '2015'
...