Skip to main content
SpringerLink
Log in
Book cover

International Colloquium on Automata, Languages, and Programming

ICALP 2010: Automata, Languages and Programming pp 76–87Cite as

Alternation Removal in Büchi Automata

  • Conference paper

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

Abstract

Alternating automata play a key role in the automata-theoretic approach to specification, verification, and synthesis of reactive systems. Many algorithms on alternating automata, and in particular, their nonemptiness test, involve removal of alternation: a translation of the alternating automaton to an equivalent nondeterministic one. For alternating Büchi automata, the best known translation uses the “breakpoint construction” and involves an O(3n) state blow-up. The translation was described by Miyano and Hayashi in 1984, and is widely used since, in both theory and practice. Yet, the best known lower bound is only 2n.

In this paper we develop and present a complete picture of the problem of alternation removal in alternating Büchi automata. In the lower bound front, we show that the breakpoint construction captures the accurate essence of alternation removal, and provide a matching Ω(3n) lower bound. Our lower bound holds already for universal (rather than alternating) automata with an alphabet of a constant size. In the upper-bound front, we point to a class of alternating Büchi automata for which the breakpoint construction can be replaced by a simpler n2n construction. Our class, of ordered alternating Büchi automata, strictly contains the class of very-weak alternating automata, for which an n2n construction is known.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Accellera. Accellera organization inc. (2006), http://www.accellera.org

  2. Daniele, N., Guinchiglia, F., Vardi, M.Y.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 249–260. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  3. Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Heidelberg (2006)

    Google Scholar 

  4. Emerson, E.A., Jutla, C.: Tree automata, μ-calculus and determinacy. In: Proc. 32nd FOCS, pp. 368–377 (1991)

    Google Scholar 

  5. Etessami, K., Holzmann, G.J.: Optimizing Büchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 153–167. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  6. 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  MathSciNet  Google Scholar 

  7. Filiot, E., Jin, N., Raskin, J.-F.: An antichain algorithm for LTL realizability. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification. LNCS, vol. 5643, pp. 263–277. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  8. Fritz, C.: Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata. In: Ibarra, O.H., Dang, Z. (eds.) CIAA 2003. LNCS, vol. 2759, pp. 35–48. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  9. Fritz, C., Wilke, T.: State space reductions for alternating Büchi automata: Quotienting by simulation equivalences. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 157–169. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  10. Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  11. Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods in System Design 19(3), 291–314 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  12. Kupferman, O., Vardi, M.Y.: Complementation constructions for nondeterministic automata on infinite words. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 206–221. Springer, Heidelberg (2005)

    Google Scholar 

  13. Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. Journal of the ACM 47(2), 312–360 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  14. Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Proc. 12th POPL, pp. 97–107 (1985)

    Google Scholar 

  15. Löding, C.: Optimal bounds for transformations of ω-automata. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol. 1738, pp. 97–109. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  17. Morgenstern, A., Schneider, K.: From LTL to symbolically represented deterministic automata. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 279–293. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  18. Mostowski, A.W.: Regular expressions for infinite trees and a standard form of automata. In: Skowron, A. (ed.) SCT 1984. LNCS, vol. 208, pp. 157–168. Springer, Heidelberg (1985)

    Google Scholar 

  19. Muller, D.E., Saoudi, A., Schupp, P.E.: Alternating automata, the weak monadic theory of the tree and its complexity. In: Kott, L. (ed.) ICALP 1986. LNCS, vol. 226, pp. 275–283. Springer, Heidelberg (1986)

    Google Scholar 

  20. Muller, D.E., Schupp, P.E.: Alternating automata on infinite trees. Theoretical Computer Science 54, 267–276 (1987)

    Article  MATH  MathSciNet  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.Y.: Nontraditional applications of automata theory. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 575–597. Springer, Heidelberg (1994)

    Google Scholar 

  23. Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  24. Yan, Q.: Lower bounds for complementation of ω-automata via the full automata technique. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 589–600. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science and Engineering, Hebrew University, Israel

    Udi Boker, Orna Kupferman & Adin Rosenberg

Authors
  1. Udi Boker
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Orna Kupferman
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Adin Rosenberg
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computing Laboratory, Oxford University, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK

    Samson Abramsky

  2. Université de Bordeaux (LaBRI) & INRIA, 351, cours de la Libération, 33405, Talence Cedex, France,

    Cyril Gavoille

  3. INRIA, Centre de Recherche Bordeaux – Sud-Ouest, 351 cours de la Libération, 33405, Talence Cedex, France

    Claude Kirchner

  4. Heinz Nixdorf Institute, University of Paderborn, Fürstenallee 11, 33102, Paderborn, Germany

    Friedhelm Meyer auf der Heide

  5. University of Patras and RACTI, 26500, Patras, Greece

    Paul G. Spirakis

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Boker, U., Kupferman, O., Rosenberg, A. (2010). Alternation Removal in Büchi Automata. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds) Automata, Languages and Programming. ICALP 2010. Lecture Notes in Computer Science, vol 6199. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14162-1_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-14162-1_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-14161-4

  • Online ISBN: 978-3-642-14162-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation