Skip to main content
SpringerLink
Log in

State Space Reductions for Alternating Büchi Automata Quotienting by Simulation Equivalences

  • Conference paper
  • First Online:
FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2556))

Abstract

Quotienting by simulation equivalences is a well-established technique for reducing the size of nondeterministic Büchi automata.We adapt this technique to alternating Büchi automata. To this end we suggest two new quotients, namely minimax and semi-elective quotients, prove that they preserve the recognized languages, and show that computing them is not more difficult than computing quotients for nondeterministic Büchi automata. We explain the merits of of our quotienting procedures with respect to converting alternating Büchi automata into nondeterministic ones.

This also implies that approximation of a minimum-size ω-automaton within a constant factor is impossible in polynomial time unless P=PSPACE.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Rajeev Alur, ThomasA. Henzinger, Orna Kupferman, and MosheY. Vardi. Alternating refinement relations. In D. Sangiorgi and R. de Simone, editors, CONCUR 1998, vol. 1466 of LNCS, pp. 163–178, 1998.

    Google Scholar 

  2. Doran Bustan and Orna Grumberg. Checking for fair simulation in models with Büchi fairness constraints, Dec. 2000. Tech. Rep. TR-CS-2000-13, Technion.

    Google Scholar 

  3. Marco Daniele, Fausto Giunchiglia, and MosheY. Vardi. Improved automata generation for linear time temporal logic. In N. Halbwachs and D. Peled, editors, CAV 1999, vol. 1633 of LNCS, pp. 249–260, 1999.

    Google Scholar 

  4. David L. Dill, Alan J. Hu, and Howard Wong-Toi. Checking for language inclusion using simulation preorders. In Kim G. Larsen and Arne Skou, editors, CAV 1991, vol. 575 of LNCS, pp. 255–265, 1991.

    Google Scholar 

  5. Kousha Etessami and Gerard Holzmann. Optimizing Büchi automata. In Catuscia Palamidessi, editor, CONCUR 2000, vol. 1877 of LNCS, pp. 153–167, 2000.

    Chapter  Google Scholar 

  6. E. Allen Emerson and Charanjit S. Jutla. The complexity of tree automata and logics of programs (extended abstract). In FoCS 1988, pp. 328–337. 1988. IEEE.

    Google Scholar 

  7. E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy. In FoCS 1991, pp. 368–377, San Juan, Puerto Rico, Oct. 1991. IEEE.

    Google Scholar 

  8. Kousha Etessami, Rebecca Schuller, and Thomas Wilke. Fair simulation relations, parity games, and state space reduction forBüchi automata. In F. Orejas, P.G. Spirakis, and J. van Leeuwen, editors, ICALP 2001, vol. 2076 of LNCS, pp. 694–707, 2001.

    Google Scholar 

  9. Kousha Etessami. A Hierarchy of Polynomial-Time Computable Simulations for Automata. CONCUR 2002, to appear.

    Google Scholar 

  10. Carsten Fritz and Thomas Wilke. Simulation relations for alternating Büchi automata. Extended version of tech. rep. 2019, Institut für Informatik, CAU Kiel, July 2002. URL: http://www.informatik.uni-kiel.de/∽fritz/ TechRep2019 ext.ps.

  11. Yuri Gurevich and Leo Harrington. Trees, automata, and games. In 14th ACM Symp. on the Theory of Computing, pp. 60–65, 1982.

    Google Scholar 

  12. M. R. Garey and D. S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman and Co., San Francisco, 1979.

    MATH  Google Scholar 

  13. Paul Gastin and Denis Oddoux. Fast LTL to Büchi automata translation. In G. Berry, H. Comon, and A. Finkel, editors, CAV 2001, vol. 2102 of LNCS, pp. 53–65, 2001.

    Google Scholar 

  14. Rob Gerth, Doron Peled, Moshe Y. Vardi, and Pierre Wolper. Simple on-the-.y automatic verification of linear temporal logic. In PSTV 1995, pp. 3–18, Warsaw, Poland, June 1995. Chapman Hall.

    Google Scholar 

  15. Sankar Gurumurthy, Roderick Bloem, and Fabio Somenzi. Fair simulation minimization. CAV 2002, to appear.

    Google Scholar 

  16. Monika Henzinger Rauch, Thomas A. Henzinger, and Peter W. Kopke. Computing simulations on finite and infinite graphs. In FoCS 1995, pp. 453–462, 1995.

    Google Scholar 

  17. Thomas A. Henzinger, Orna Kupferman, and Sriram K. Rajamani. Fair simulation. In CONCUR 1997, vol. 1243 of LNCS, pp. 273–287, 1997.

    Google Scholar 

  18. Thomas A. Henzinger and Sriram K. Rajamani. Fair bisimulation.In S. Graf and M. Schwartzbach, editors, TACAS 2000, vol. 1785 of LNCS, pp. 299–314, 2000.

    Google Scholar 

  19. Marcin Jurdziński. Small progress measures for solving parity games. In H. Reichel and S. Tison, editors, STACS 2000, vol. 1770 of LNCS, pp. 290–301, 2000.

    Chapter  Google Scholar 

  20. OrnaKupferman, MosheY. Vardi, and Pierre Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312–360, 2000.

    Article  MATH  MathSciNet  Google Scholar 

  21. Martin Leucker and Thomas Noll. Truth/SLC-A parallel verification platform for concurrent systems. In G. Berry, H. Comon, and A. Finkel, editors, CAV 2001, vol. 2102 of LNCS, pp. 255–259, 2001.

    Google Scholar 

  22. Kenneth L. McMillan. Symbolic Model Checking. Kluwer, Boston, 1993.

    MATH  Google Scholar 

  23. S. Miyano and T. Hayashi. Alternating finite automata on ω-words. Theoretical Computer Science, 32:321–330, 1984.

    Article  MATH  MathSciNet  Google Scholar 

  24. Robin Milner. An algebraic definition of simulation between programs. In D. C. Cooper, editor, Proc. of the 2nd Int. Joint Conf. on Artificial Intelligence, pp. 481–489, London, UK, September 1971.William Kaufmann.

    Google Scholar 

  25. David E. Muller, Ahmed Saoudi, and Paul E. Schupp. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In LICS 1988, pp. 422–427, IEEE Computer Society, 1988.

    Google Scholar 

  26. Fabio Somenzi and Roderick Bloem. Efficient Büchi automata from LTL formulae. In E. Allen Emerson and A. Prasad Sistla, editors, CAV 2000, vol. 1855 of LNCS, pp. 248–263, 2000.

    Google Scholar 

  27. Moshe Y. Vardi. Nontraditional applications of automata theory. In Theoretical Aspects of Computer Software, vol. 789 of LNCS, pp. 575–597, 1994.

    Google Scholar 

  28. Moshe Y. Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification. In Dexter Kozen, editor, LICS 1986, pp. 332–344, Cambridge, Mass., 16-18 June 1986.

    Google Scholar 

  29. MosheY. Vardi and Pierre Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1–37, 1994.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität, 24098, Kiel, Germany

    Carsten Fritz & Thomas Wilke

Authors
  1. Carsten Fritz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas Wilke
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Engineering, Indian Institute of Technology, 208016, Kanpur, India

    Manindra Agrawal  & Anil Seth  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fritz, C., Wilke, T. (2002). State Space Reductions for Alternating Büchi Automata Quotienting by Simulation Equivalences. In: Agrawal, M., Seth, A. (eds) FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2002. Lecture Notes in Computer Science, vol 2556. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36206-1_15

Download citation

  • DOI: https://doi.org/10.1007/3-540-36206-1_15

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00225-3

  • Online ISBN: 978-3-540-36206-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation