Skip to main content
SpringerLink
Log in

Inherent Size Blowup in \(\omega \)-Automata

  • Conference paper
  • First Online:
Developments in Language Theory (DLT 2019)

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

Included in the following conference series:

Abstract

We clarify the succinctness of the different \(\omega \)-automata types and the size blowup involved in boolean operations on them. We argue that there are good reasons for the classic acceptance conditions, while there is also place for additional acceptance conditions, especially in the deterministic setting; Boolean operations on deterministic automata with the classic acceptance conditions involve an exponential size blowup, which can be avoided by using stronger acceptance conditions. In particular, we analyze the combination of hyper-Rabin and hyper-Streett automata, which we call hyper-dual, and show that in the deterministic setting it allows for exponential succinctness compared to the classic types, boolean operations on it only involve a quadratic size blowup, and its nonemptiness, universality, and containment checks are in PTIME.

This work was supported by the Israel Science Foundation grant 1373/16.

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 EPUB and 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

References

  1. Babiak, T., et al.: The Hanoi omega-automata format. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 479–486. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_31

    Chapter  Google Scholar 

  2. Blahoudek, F.: Translation of an LTL fragment to deterministic Rabin and Streett automata. Master’s thesis, Masarykova Univerzita (2012)

    Google Scholar 

  3. Boker, U.: Word-automata translations (2010). http://www.faculty.idc.ac.il/udiboker/automata

  4. Boker, U.: On the (in)succinctness of muller automata. In: CSL, pp. 12:1–12:16 (2017)

    Google Scholar 

  5. Boker, U.: Rabin vs. Streett automata. In: FSTTCS, pp. 17:1–17:15 (2017)

    Google Scholar 

  6. Boker, U.: Why these automata types? In: Proceedings of LPAR, pp. 143–163 (2018)

    Google Scholar 

  7. Boker, U., Kuperberg, D., Kupferman, O., Skrzypczak, M.: Nondeterminism in the presence of a diverse or unknown future. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013. LNCS, vol. 7966, pp. 89–100. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39212-2_11

    Chapter  Google Scholar 

  8. Boker, U., Kupferman, O.: Translating to co-Büchi made tight, unified, and useful. ACM Trans. Comput. Log. 13(4), 29:1–29:29 (2012)

    Article  Google Scholar 

  9. Boker, U., Kupferman, O., Skrzypczak, M.: How deterministic are good-for-games automata? In: Proceedings of FSTTCS, pp. 18:1–18:14 (2017)

    Google Scholar 

  10. Cai, Y., Zhang, T.: A tight lower bound for Streett complementation. In: Proceedings of FSTTCS, pp. 339–350 (2011)

    Google Scholar 

  11. Cai, Y., Zhang, T.: Tight upper bounds for Streett and parity complementation. In: Proceedings of CSL, pp. 112–128 (2011)

    Google Scholar 

  12. Cai, Y., Zhang, T., Luo, H.: An improved lower bound for the complementation of Rabin automata. In: Proceedings of LICS, pp. 167–176 (2009)

    Google Scholar 

  13. Chatterjee, K., Gaiser, A., Křetínský, J.: Automata with generalized rabin pairs for probabilistic model checking and LTL synthesis. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 559–575. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_37

    Chapter  Google Scholar 

  14. Choueka, Y.: Theories of automata on \(\omega \)-tapes: a simplified approach. J. Comput. Syst. Sci. 8, 117–141 (1974)

    Article  MathSciNet  Google Scholar 

  15. Clarke, E.M., Browne, I.A., Kurshan, R.P.: A unified approach for showing language containment and equivalence between various types of \(\omega \)-automata. In: Arnold, A. (ed.) CAAP 1990. LNCS, vol. 431, pp. 103–116. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52590-4_43

    Chapter  Google Scholar 

  16. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Sys. 8(2), 244–263 (1986)

    Article  Google Scholar 

  17. Colcombet, T., Zdanowski, K.: A tight lower bound for determinization of transition labeled Büchi automata. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 151–162. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02930-1_13

    Chapter  MATH  Google Scholar 

  18. Emerson, E.A., Lei, C.-L.: Modalities for model checking: branching time logic strikes back. Sci. Comput. Program. 8, 275–306 (1987)

    Article  MathSciNet  Google Scholar 

  19. Esparza, J., Křetínský, J., Sickert, S.: From LTL to deterministic automata: a safraless compositional approach. Form. Methods Syst. Des. 49(3), 219–271 (2016)

    Article  Google Scholar 

  20. Filiot, E., Gentilini, R., Raskin, J.F.: Rational synthesis under imperfect information. In: Proceedings of LICS, pp. 422–431 (2018)

    Google Scholar 

  21. Henzinger, T.A., Piterman, N.: Solving games without determinization. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 395–410. Springer, Heidelberg (2006). https://doi.org/10.1007/11874683_26

    Chapter  Google Scholar 

  22. Hunter, P., Dawar, A.: Complexity bounds for regular games. In: Jȩdrzejowicz, J., Szepietowski, A. (eds.) MFCS 2005. LNCS, vol. 3618, pp. 495–506. Springer, Heidelberg (2005). https://doi.org/10.1007/11549345_43

    Chapter  Google Scholar 

  23. King, V., Kupferman, O., Vardi, M.Y.: On the complexity of parity word automata. In: Honsell, F., Miculan, M. (eds.) FoSSaCS 2001. LNCS, vol. 2030, pp. 276–286. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45315-6_18

    Chapter  MATH  Google Scholar 

  24. Křetínský, J., Esparza, J.: Deterministic automata for the (F,G)-fragment of LTL. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 7–22. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_7

    Chapter  Google Scholar 

  25. Kupferman, O., Morgenstern, G., Murano, A.: Typeness for \(\omega \)-regular automata. In: Wang, F. (ed.) ATVA 2004. LNCS, vol. 3299, pp. 324–338. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30476-0_27

    Chapter  MATH  Google Scholar 

  26. 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). https://doi.org/10.1007/978-3-540-31980-1_14

    Chapter  MATH  Google Scholar 

  27. Liu, W., Wang, J.: A tighter analysis of Piterman’s Büchi determinization. Inf. Process. Lett. 109(16), 941–945 (2009)

    Article  Google Scholar 

  28. Löding, C.: Optimal bounds for transformations of \(\omega \)-automata. In: Rangan, C.P., Raman, V., Ramanujam, R. (eds.) FSTTCS 1999. LNCS, vol. 1738, pp. 97–109. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-46691-6_8

    Chapter  MATH  Google Scholar 

  29. Löding, C., Yue, H.: Memory bounds for winning strategies in infinite games (2008, unpublished)

    Google Scholar 

  30. Michel, M.: Complementation is more difficult with automata on infinite words. CNET, Paris (1988)

    Google Scholar 

  31. Miyano, S., Hayashi, T.: Alternating finite automata on \(\omega \)-words. Theor. Comput. Sci. 32, 321–330 (1984)

    Article  MathSciNet  Google Scholar 

  32. Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. Log. Methods Comput. Sci. 3(3), 5 (2007)

    Article  Google Scholar 

  33. Safra, S.: Complexity of automata on infinite objects. Ph.D. thesis, Weizmann Institute of Science (1989)

    Google Scholar 

  34. Safra, S.: Exponential determinization for \(\omega \)-automata with strong-fairness acceptance condition. In: Proceedings of 24th ACM Symposium on Theory of Computing (1992)

    Google Scholar 

  35. Safra, S., Vardi, M.Y.: On \(\omega \)-automata and temporal logic. In: Proceedings of 21st ACM Symposium on Theory of Computing, pp. 127–137 (1989)

    Google Scholar 

  36. Schewe, S.: Büchi complementation made tight. In: Proceedings of 26th Symposium on Theoretical Aspects of Computer Science, volume 3 of LIPIcs, pp. 661–672 (2009)

    Google Scholar 

  37. Schewe, S., Varghese, T.: Determinising parity automata. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014. LNCS, vol. 8634, pp. 486–498. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44522-8_41

    Chapter  Google Scholar 

  38. Vardi, M.: The Büchi complementation saga. In: Proceedings of STACS, pp. 12–22 (2007)

    Google Scholar 

  39. Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proceedings of FOCS, pp. 327–338 (1985)

    Google Scholar 

  40. Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994)

    Article  MathSciNet  Google Scholar 

  41. Yan, Q.: Lower bounds for complementation of \(\omega \)-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). https://doi.org/10.1007/11787006_50

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Interdisciplinary Center (IDC) Herzliya, Herzliya, Israel

    Udi Boker

Authors
  1. Udi Boker
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Udi Boker .

Editor information

Editors and Affiliations

  1. University of Warsaw, Warsaw, Poland

    Piotrek Hofman

  2. University of Warsaw, Warsaw, Poland

    Michał Skrzypczak

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Boker, U. (2019). Inherent Size Blowup in \(\omega \)-Automata. In: Hofman, P., Skrzypczak, M. (eds) Developments in Language Theory. DLT 2019. Lecture Notes in Computer Science(), vol 11647. Springer, Cham. https://doi.org/10.1007/978-3-030-24886-4_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-24886-4_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-24885-7

  • Online ISBN: 978-3-030-24886-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation