Document Open Access Logo

Minimizing GFG Transition-Based Automata (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors Bader Abu Radi, Orna Kupferman

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2019.100.pdf
  • Filesize: 0.51 MB
  • 16 pages

Document Identifiers

Author Details

Bader Abu Radi
  • School of Computer Science and Engineering, The Hebrew University, Jerusalem, Israel
Orna Kupferman
  • School of Computer Science and Engineering, The Hebrew University, Jerusalem, Israel

Cite As Get BibTex

Bader Abu Radi and Orna Kupferman. Minimizing GFG Transition-Based Automata (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 100:1-100:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ICALP.2019.100

Abstract

While many applications of automata in formal methods can use nondeterministic automata, some applications, most notably synthesis, need deterministic or good-for-games automata. The latter are nondeterministic automata that can resolve their nondeterministic choices in a way that only depends on the past. The minimization problem for nondeterministic and deterministic Büchi and co-Büchi word automata are PSPACE-complete and NP-complete, respectively. We describe a polynomial minimization algorithm for good-for-games co-Büchi word automata with transition-based acceptance. Thus, a run is accepting if it traverses a set of designated transitions only finitely often. Our algorithm is based on a sequence of transformations we apply to the automaton, on top of which a minimal quotient automaton is defined.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Automata over infinite objects
Keywords
  • Minimization
  • Deterministic co-Büchi Automata

Metrics

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

References

  1. A. Badr, V. Geffert, and I. Shipman. Hyper-minimizing minimized deterministic finite state automata. ITA, 43(1):69-94, 2009. Google Scholar
  2. M. Bagnol and D. Kuperberg. Büchi Good-for-Games Automata Are Efficiently Recognizable. In Proc. 38th Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 122 of LIPIcs, pages 16:1-16:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. Google Scholar
  3. U. Boker, D. Kuperberg, O. Kupferman, and M. Skrzypczak. Nondeterminism in the Presence of a Diverse or Unknown Future. In Proc. 40th Int. Colloq. on Automata, Languages, and Programming, volume 7966 of Lecture Notes in Computer Science, pages 89-100, 2013. Google Scholar
  4. U. Boker, O. Kupferman, and M. Skrzypczak. How Deterministic are Good-For-Games Automata? In Proc. 37th Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 93 of Leibniz International Proceedings in Informatics (LIPIcs), pages 18:1-18:14, 2017. Google Scholar
  5. J.R. Büchi. On a Decision Method in Restricted Second Order Arithmetic. In Proc. Int. Congress on Logic, Method, and Philosophy of Science. 1960, pages 1-12. Stanford University Press, 1962. Google Scholar
  6. Th. Colcombet. The theory of stabilisation monoids and regular cost functions. In Proc. 36th Int. Colloq. on Automata, Languages, and Programming, volume 5556 of Lecture Notes in Computer Science, pages 139-150. Springer, 2009. Google Scholar
  7. A. Duret-Lutz, A. Lewkowicz, A. Fauchille, Th. Michaud, E. Renault, and L. Xu. Spot 2.0 - a framework for LTL and ω-automata manipulation. In 14th Int. Symp. on Automated Technology for Verification and Analysis, volume 9938 of Lecture Notes in Computer Science, pages 122-129. Springer, 2016. Google Scholar
  8. J. Esparza, O. Kupferman, and M.Y. Vardi. Verification. In Handbook AutoMathA, pages 549-588. European Mathematical Society, 2018. Google Scholar
  9. D. Giannakopoulou and F. Lerda. From States to Transitions: Improving Translation of LTL Formulae to Büchi Automata. In Proc. 22nd International Conference on Formal Techniques for Networked and Distributed Systems, volume 2529 of Lecture Notes in Computer Science, pages 308-326. Springer, 2002. Google Scholar
  10. S. Gurumurthy, R. Bloem, and F. Somenzi. Fair simulation minimization. In Proc. 14th Int. Conf. on Computer Aided Verification, volume 2404 of Lecture Notes in Computer Science, pages 610-623. Springer, 2002. Google Scholar
  11. S. Halamish and O. Kupferman. Minimizing Deterministic Lattice Automata. ACM Transactions on Computational Logic, 16(1):1-21, 2015. Google Scholar
  12. T.A. Henzinger, O. Kupferman, and S. Rajamani. Fair simulation. Information and Computation, 173(1):64-81, 2002. Google Scholar
  13. T.A. Henzinger and N. Piterman. Solving Games without Determinization. In Proc. 15th Annual Conf. of the European Association for Computer Science Logic, volume 4207 of Lecture Notes in Computer Science, pages 394-410. Springer, 2006. Google Scholar
  14. J.E. Hopcroft. An n log n algorithm for minimizing the states in a finite automaton. In Z. Kohavi, editor, The Theory of Machines and Computations, pages 189-196. Academic Press, 1971. Google Scholar
  15. A. Jez and A. Maletti. Hyper-Minimization for Deterministic Tree Automata. Int. J. Found. Comput. Sci., 24(6):815-830, 2013. Google Scholar
  16. T. Jiang and B. Ravikumar. Minimal NFA problems are hard. SIAM Journal on Computing, 22(6):1117-1141, 1993. Google Scholar
  17. D. Kuperberg and M. Skrzypczak. On Determinisation of Good-for-Games Automata. In Proc. 42nd Int. Colloq. on Automata, Languages, and Programming, pages 299-310, 2015. Google Scholar
  18. O. Kupferman and Y. Lustig. Lattice Automata. In Proc. 8th Int. Conf. on Verification, Model Checking, and Abstract Interpretation, volume 4349 of Lecture Notes in Computer Science, pages 199-213. Springer, 2007. Google Scholar
  19. O. Kupferman, S. Safra, and M.Y. Vardi. Relating word and tree automata. Ann. Pure Appl. Logic, 138(1-3):126-146, 2006. Google Scholar
  20. O. Kupferman and M.Y. Vardi. Safraless Decision Procedures. In Proc. 46th IEEE Symp. on Foundations of Computer Science, pages 531-540, 2005. Google Scholar
  21. L.H. Landweber. Decision Problems for ω-Automata. Mathematical Systems Theory, 3:376-384, 1969. Google Scholar
  22. W. Li, Sh. Kan, and Z. Huang. A Better Translation From LTL to Transition-Based Generalized Büchi Automata. IEEE Access, 5:27081-27090, 2017. Google Scholar
  23. C. Löding. Efficient Minimization of Deterministic Weak Omega-Automata. Information Processing Letters, 79(3):105-109, 2001. Google Scholar
  24. A. Malcher. Minimizing finite automata is computationally hard. Theoretical Computer Science, 327(3):375-390, 2004. Google Scholar
  25. M. Mohri. Finite-State Transducers in Language and Speech Processing. Computational Linguistics, 23(2):269-311, 1997. Google Scholar
  26. G. Morgenstern. Expressiveness results at the bottom of the ω-regular hierarchy. M.Sc. Thesis, The Hebrew University, 2003. Google Scholar
  27. D.E. Muller, A. Saoudi, and P. E. Schupp. Weak Alternating Automata Give a Simple Explanation of Why Most Temporal and Dynamic Logics are Decidable in Exponential Time. In Proc. 3rd IEEE Symp. on Logic in Computer Science, pages 422-427, 1988. Google Scholar
  28. J. Myhill. Finite automata and the representation of events. Technical Report WADD TR-57-624, pages 112-137, Wright Patterson AFB, Ohio, 1957. Google Scholar
  29. A. Nerode. Linear Automaton Transformations. Proceedings of the American Mathematical Society, 9(4):541-544, 1958. Google Scholar
  30. D. Niwinski and I. Walukiewicz. Relating hierarchies of word and tree automata. In Proc. 15th Symp. on Theoretical Aspects of Computer Science, volume 1373 of Lecture Notes in Computer Science. Springer, 1998. Google Scholar
  31. M.O. Rabin and D. Scott. Finite automata and their decision problems. IBM Journal of Research and Development, 3:115-125, 1959. Google Scholar
  32. S. Safra. On the Complexity of ω-Automata. In Proc. 29th IEEE Symp. on Foundations of Computer Science, pages 319-327, 1988. Google Scholar
  33. S. Schewe. Beyond Hyper-Minimisation - Minimising DBAs and DPAs is NP-Complete. In Proc. 30th Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 8 of Leibniz International Proceedings in Informatics (LIPIcs), pages 400-411, 2010. Google Scholar
  34. S. Sickert, J. Esparza, S. Jaax, and J. Křetínský. Limit-Deterministic Büchi Automata for Linear Temporal Logic. In Proc. 28th Int. Conf. on Computer Aided Verification, volume 9780 of Lecture Notes in Computer Science, pages 312-332. Springer, 2016. Google Scholar
  35. R.E. Tarjan. Depth first search and linear graph algorithms. SIAM Journal of Computing, 1(2):146-160, 1972. Google Scholar
  36. M.Y. Vardi and P. Wolper. Reasoning about Infinite Computations. Information and Computation, 115(1):1-37, 1994. 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