---
_id: '13160'
abstract:
- lang: eng
  text: "Transforming deterministic ω\r\n-automata into deterministic parity automata
    is traditionally done using variants of appearance records. We present a more
    efficient variant of this approach, tailored to Rabin automata, and several optimizations
    applicable to all appearance records. We compare the methods experimentally and
    find out that our method produces smaller automata than previous approaches. Moreover,
    the experiments demonstrate the potential of our method for LTL synthesis, using
    LTL-to-Rabin translators. It leads to significantly smaller parity automata when
    compared to state-of-the-art approaches on complex formulae."
acknowledgement: This work is partially funded by the DFG project “Verified Model
  Checkers” and by the Czech Science Foundation, grant No. P202/12/G061.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Jan
  full_name: Kretinsky, Jan
  id: 44CEF464-F248-11E8-B48F-1D18A9856A87
  last_name: Kretinsky
  orcid: 0000-0002-8122-2881
- first_name: Tobias
  full_name: Meggendorfer, Tobias
  id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
  last_name: Meggendorfer
  orcid: 0000-0002-1712-2165
- first_name: Clara
  full_name: Waldmann, Clara
  last_name: Waldmann
- first_name: Maximilian
  full_name: Weininger, Maximilian
  last_name: Weininger
citation:
  ama: 'Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record
    for transforming Rabin automata into parity automata. In: <i>Tools and Algorithms
    for the Construction and Analysis of Systems</i>. Vol 10205. Springer; 2017:443-460.
    doi:<a href="https://doi.org/10.1007/978-3-662-54577-5_26">10.1007/978-3-662-54577-5_26</a>'
  apa: 'Kretinsky, J., Meggendorfer, T., Waldmann, C., &#38; Weininger, M. (2017).
    Index appearance record for transforming Rabin automata into parity automata.
    In <i>Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol.
    10205, pp. 443–460). Uppsala, Sweden: Springer. <a href="https://doi.org/10.1007/978-3-662-54577-5_26">https://doi.org/10.1007/978-3-662-54577-5_26</a>'
  chicago: Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger.
    “Index Appearance Record for Transforming Rabin Automata into Parity Automata.”
    In <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, 10205:443–60.
    Springer, 2017. <a href="https://doi.org/10.1007/978-3-662-54577-5_26">https://doi.org/10.1007/978-3-662-54577-5_26</a>.
  ieee: J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance
    record for transforming Rabin automata into parity automata,” in <i>Tools and
    Algorithms for the Construction and Analysis of Systems</i>, Uppsala, Sweden,
    2017, vol. 10205, pp. 443–460.
  ista: 'Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2017. Index appearance
    record for transforming Rabin automata into parity automata. Tools and Algorithms
    for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for
    the Construction and Analysis of Systems, LNCS, vol. 10205, 443–460.'
  mla: Kretinsky, Jan, et al. “Index Appearance Record for Transforming Rabin Automata
    into Parity Automata.” <i>Tools and Algorithms for the Construction and Analysis
    of Systems</i>, vol. 10205, Springer, 2017, pp. 443–60, doi:<a href="https://doi.org/10.1007/978-3-662-54577-5_26">10.1007/978-3-662-54577-5_26</a>.
  short: J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, in:, Tools and
    Algorithms for the Construction and Analysis of Systems, Springer, 2017, pp. 443–460.
conference:
  end_date: 2017-04-29
  location: Uppsala, Sweden
  name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
  start_date: 2017-04-22
date_created: 2023-06-21T13:21:14Z
date_published: 2017-03-31T00:00:00Z
date_updated: 2023-06-21T13:29:46Z
day: '31'
department:
- _id: KrCh
doi: 10.1007/978-3-662-54577-5_26
external_id:
  arxiv:
  - '1701.05738'
intvolume: '     10205'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.48550/arXiv.1701.05738
month: '03'
oa: 1
oa_version: Preprint
page: 443-460
publication: Tools and Algorithms for the Construction and Analysis of Systems
publication_identifier:
  eisbn:
  - '9783662545775'
  eissn:
  - 1611-3349
  isbn:
  - '9783662545768'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
status: public
title: Index appearance record for transforming Rabin automata into parity automata
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10205
year: '2017'
...