Skip to main content
SpringerLink
Log in

Büchi Automata Can Have Smaller Quotients

  • Conference paper
Automata, Languages and Programming (ICALP 2011)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6756))

Included in the following conference series:

Abstract

We study novel simulation-like preorders for quotienting nondeterministic Büchi automata. We define fixed-word delayed simulation, a new preorder coarser than delayed simulation. We argue that fixed-word simulation is the coarsest forward simulation-like preorder which can be used for quotienting Büchi automata, thus improving our understanding of the limits of quotienting. Also, we show that computing fixed-word simulation is PSPACE-complete.

On the practical side, we introduce proxy simulations, which are novel polynomial-time computable preorders sound for quotienting. In particular, delayed proxy simulation induce quotients that can be smaller by an arbitrarily large factor than direct backward simulation. We derive proxy simulations as the product of a theory of refinement transformers: A refinement transformer maps preorders nondecreasingly, preserving certain properties. We study under which general conditions refinement transformers are sound for quotienting.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. Abdulla, P., Chen, Y.-F., Holik, L., Vojnar, T.: Mediating for Reduction. In: FSTTCS, pp. 1–12. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2009)

    Google Scholar 

  2. Aziz, A., Singhal, V., Swamy, G.M., Brayton, R.K.: Minimizing Interacting Finite State Machines. Technical Report UCB/ERL M93/68, UoC, Berkeley (1993)

    Google Scholar 

  3. Clemente, L.: Büchi Automata can have Smaller Quotients. Technical Report EDI-INF-RR-1399, LFCS, University of Edinburgh (April 2011)

    Google Scholar 

  4. Clemente, L., Mayr, R.: Multipebble Simulations for Alternating Automata. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 297–312. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  5. Dill, D.L., Hu, A.J., Wont-Toi, H.: Checking for Language Inclusion Using Simulation Preorders. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  6. Etessami, K.: A Hierarchy of Polynomial-Time Computable Simulations for Automata. In: Brim, L., Jančar, P., Křetínský, M., Kučera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 131–144. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  7. Etessami, K., Wilke, T., Schuller, R.A.: Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata. SIAM J. Comput. 34(5), 1159–1175 (2005)

    Article  MATH  Google Scholar 

  8. Fritz, C., Wilke, T.: Simulation Relations for Alternating Büchi Automata. Theor. Comput. Sci. 338(1-3), 275–314 (2005)

    Article  MATH  Google Scholar 

  9. Gramlich, G., Schnitger, G.: Minimizing NFA’s and Regular Expressions. Journal of Computer and System Sciences 73(6), 908–923 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  10. Gurumurthy, S., Bloem, R., Somenzi, F.: Fair Simulation Minimization. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 610–624. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  11. Henzinger, T.A., Kupferman, O., Rajamani, S.K.: Fair Simulation. Information and Computation 173, 64–81 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  12. Henzinger, T.A., Rajamani, S.K.: Fair Bisimulation. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, pp. 299–314. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  13. Jiang, T., Ravikumar, B.: Minimal NFA Problems are Hard. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510, pp. 629–640. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  14. Juvekar, S., Piterman, N.: Minimizing Generalized Büchi Automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 45–58. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  15. Kupferman, O., Vardi, M.: Verification of Fair Transition Systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 372–382. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  16. Kupferman, O., Vardi, M.: Weak Alternating Automata Are Not That Weak. ACM Trans. Comput. Logic 2, 408–429 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  17. Lynch, N.A., Vaandrager, F.W.: Forward and Backward Simulations. Part I: Untimed Systems. Information and Computation 121(2), 214–233 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  18. Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  19. Raimi, R.S.: Environment Modeling and Efficient State Reachability Checking. PhD thesis, The University of Texas at Austin (1999)

    Google Scholar 

  20. Schewe, S.: Beyond Hyper-Minimisation—Minimising DBAs and DPAs is NP-Complete. In: FSTTCS. LIPIcs, vol. 8, pp. 400–411. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2010)

    Google Scholar 

  21. Somenzi, F., Bloem, R.: Efficient Büchi Automata from LTL Formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248–263. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  22. Vardi, M.: Alternating Automata and Program Verification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol. 1000, pp. 471–485. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LFCS, School of Informatics, University of Edinburgh, UK

    Lorenzo Clemente

Authors
  1. Lorenzo Clemente
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. ICE-TCS, School of Computer Science, Reykjavik University, Menntavegur 1, IS 101, Reykjavik, Iceland

    Luca Aceto

  2. Fakultät für Informatik, Universität Wien, Universitätsstraße10/9, 1090, Wien, Österreich, Austria

    Monika Henzinger

  3. Department of Applied Mathematics, Charles University, Malostranské nám. 25, 118 00, Praha 1, Czech Republic

    Jiří Sgall

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Clemente, L. (2011). Büchi Automata Can Have Smaller Quotients. In: Aceto, L., Henzinger, M., Sgall, J. (eds) Automata, Languages and Programming. ICALP 2011. Lecture Notes in Computer Science, vol 6756. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22012-8_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-22012-8_20

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-22011-1

  • Online ISBN: 978-3-642-22012-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation