Document Open Access Logo

State Space Reduction For Parity Automata

Authors Christof Löding, Andreas Tollkötter

PDF
Thumbnail PDF

File

LIPIcs.CSL.2020.27.pdf
  • Filesize: 0.52 MB
  • 16 pages

Document Identifiers

Author Details

Christof Löding
  • RWTH Aachen University, Germany
Andreas Tollkötter
  • RWTH Aachen University, Germany

Cite As Get BibTex

Christof Löding and Andreas Tollkötter. State Space Reduction For Parity Automata. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 27:1-27:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CSL.2020.27

Abstract

Exact minimization of ω-automata is a difficult problem and heuristic algorithms are a subject of current research. We propose several new approaches to reduce the state space of deterministic parity automata. These are based on extracting information from structures within the automaton, such as strongly connected components, coloring of the states, and equivalence classes of given relations, to determine states that can safely be merged. We also establish a framework to generalize the notion of quotient automata and uniformly describe such algorithms. The description of these procedures consists of a theoretical analysis as well as data collected from experiments.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Regular languages
Keywords
  • automata
  • ω-automata
  • parity
  • minimization
  • state space reduction
  • deterministic
  • simulation relations

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  2. J. Richard Büchi. On a decision method in restricted second order arithmetic. In International Congress on Logic, Methodology and Philosophy of Science, pages 1-11. Stanford University Press, 1962. Google Scholar
  3. Olivier Carton and Ramón Maceiras. Computing the Rabin index of a parity automaton. RAIRO-Theoretical Informatics and Applications, 33(6):495-505, 1999. Google Scholar
  4. Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Laurent Xu. Spot 2.0 - a framework for LTL and ω-automata manipulation. In Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA'16), volume 9938 of Lecture Notes in Computer Science, pages 122-129. Springer, October 2016. URL: https://doi.org/10.1007/978-3-319-46520-3_8.
  5. E. Allen Emerson and Chin-Laung Lei. Modalities for Model Checking: Branching Time Logic Strikes Back. Sci. Comput. Program., 8(3):275-306, 1987. URL: https://doi.org/10.1016/0167-6423(87)90036-0.
  6. Kousha Etessami, Thomas Wilke, and Rebecca A. Schuller. Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata. In Automata, Languages and Programming, pages 694-707, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg. Google Scholar
  7. Carsten Fritz and Thomas Wilke. Simulation Relations for Alternating Büchi Automata. Theor. Comput. Sci., 338(1-3):275-314, June 2005. URL: https://doi.org/10.1016/j.tcs.2005.01.016.
  8. Carsten Fritz and Thomas Wilke. Simulation Relations for Alternating Parity Automata and Parity Games. In Developments in Language Theory, 10th International Conference, DLT 2006, Santa Barbara, CA, USA, June 26-29, 2006, Proceedings, pages 59-70, 2006. URL: https://doi.org/10.1007/11779148_7.
  9. John E. Hopcroft. An N Log N Algorithm for Minimizing States in a Finite Automaton. Technical report, Stanford University, Stanford, CA, USA, 1971. Google Scholar
  10. Swen Jacobs, Guillermo A. Pérez, and Roderick Bloem. The Reactive Synthesis Competition. URL: http://www.syntcomp.org.
  11. Richard Mayr and Lorenzo Clemente. Advanced Automata Minimization. In POPL 2013, October 2012. URL: http://arxiv.org/abs/1210.6624.
  12. Philipp J. Meyer, Salomon Sickert, and Michael Luttenberger. Strix: Explicit Reactive Synthesis Strikes Back! In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, pages 578-586, 2018. URL: https://doi.org/10.1007/978-3-319-96145-3_31.
  13. A.W. Mostowski. Hierarchies of weak automata and weak monadic formulas. Theoretical Computer Science, 83(2):323-335, 1991. URL: https://doi.org/10.1016/0304-3975(91)90283-8.
  14. Anton Pirogov. nbautils. https://github.com/apirogov/nbautils, 2018.
  15. Nir Piterman. From nondeterministic Büchi and Streett automata to deterministic parity automata. In Logic in Computer Science, 2006 21st Annual IEEE Symposium on, pages 255-264. IEEE, 2006. Google Scholar
  16. Shmuel Safra. On the complexity of omega-automata. In Foundations of Computer Science, 1988., 29th Annual Symposium on, pages 319-327, 1988. Google Scholar
  17. Sven Schewe. Beyond Hyper-Minimisation - Minimising DBAs and DPAs is NP-Complete. In Kamal Lodaya and Meena Mahajan, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), volume 8 of Leibniz International Proceedings in Informatics (LIPIcs), pages 400-411, Dagstuhl, Germany, 2010. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2010.400.
  18. Fabio Somenzi and Roderick Bloem. Efficient Büchi Automata from LTL Formulae. In Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings, pages 248-263, 2000. URL: https://doi.org/10.1007/10722167_21.
  19. Wolfgang Thomas. Handbook of Formal Languages, Vol. 3. In Grzegorz Rozenberg and Arto Salomaa, editors, Handbook of Formal Languages, Vol. 3, chapter Languages, Automata, and Logic, pages 389-455. Springer-Verlag New York, Inc., New York, NY, USA, 1997. URL: http://dl.acm.org/citation.cfm?id=267871.267878.
  20. Wolfgang Thomas. Church’s Problem and a Tour through Automata Theory. In Pillars of Computer Science, Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, pages 635-655. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78127-1.
  21. Moshe Y. Vardi and Thomas Wilke. Automata: from logics to algorithms. In Logic and automata - history and perspectives, volume 2 of Texts in Logic and Games, pages 629-724. Amsterdam University Press, 2007. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact