Skip to main content

Decision Problems for Subclasses of Rational Relations over Finite and Infinite Words

  • Conference paper
  • First Online:
  • 677 Accesses

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

Abstract

We consider decision problems for relations over finite and infinite words defined by finite automata. We prove that the equivalence problem for binary deterministic rational relations over infinite words is undecidable in contrast to the case of finite words, where the problem is decidable. Furthermore, we show that it is decidable in doubly exponential time for an automatic relation over infinite words whether it is a recognizable relation. We also revisit this problem in the context of finite words and improve the complexity of the decision procedure to single exponential time. The procedure is based on a polynomial time regularity test for deterministic visibly pushdown automata, which is a result of independent interest.

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

Buying options

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

Learn about institutional subscriptions

Notes

  1. 1.

    Recognizability is decidable for deterministic rational relations of arbitrary arity [14] but we are not aware of a proof preserving the doubly exponential runtime.

  2. 2.

    The authors of [14] mainly focused on decidability, and they agree that the proof as presented in that paper does not yield an exponential time upper bound.

References

  1. Abdulla, P.A.: Regular model checking. STTT 14(2), 109–118 (2012). doi:10.1007/s10009-011-0216-8

    Article  Google Scholar 

  2. Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proceedings of the Thirty-sixth Annual ACM Symposium on Theory of Computing, pp. 202–211. ACM (2004)

    Google Scholar 

  3. Bárány, V., Löding, C., Serre, O.: Regularity problems for visibly pushdown languages. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol. 3884, pp. 420–431. Springer, Heidelberg (2006). doi:10.1007/11672142_34

    Chapter  Google Scholar 

  4. Berstel, J.: Transductions and Context-Free Languages. Springer, Stuttgart (1979)

    Book  MATH  Google Scholar 

  5. Bird, M.: The equivalence problem for deterministic two-tape automata. J. Comput. Syst. Sci. 7(2), 218–236 (1973)

    Article  MathSciNet  MATH  Google Scholar 

  6. Blumensath, A., Grädel, E.: Automatic structures. In: Proceedings of the 15th IEEE Symposium on Logic in Computer Science, LICS 2000, pp. 51–62. IEEE Computer Society Press (2000)

    Google Scholar 

  7. Böhm, S., Göller, S., Halfon, S., Hofman, P.: On Büchi one-counter automata. In: Vollmer, H., Vallée, B. (eds.) 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), vol. 66, pp. 14:1–14:13 (2017). doi:10.4230/LIPIcs.STACS.2017.14. ISBN 978-3-95977-028-6

  8. Boigelot, B., Jodogne, S., Wolper, P.: An effective decision procedure for linear arithmetic over the integers and reals. ACM Trans. Comput. Log. 6(3), 614–633 (2005). doi:10.1145/1071596.1071601

    Article  MathSciNet  MATH  Google Scholar 

  9. Boigelot, B., Legay, A., Wolper, P.: Omega-regular model checking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 561–575. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24730-2_41

    Chapter  Google Scholar 

  10. Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997). doi:10.1007/3-540-63141-0_10

    Chapter  Google Scholar 

  11. Bozzelli, L., Maubert, B., Pinchinat, S.: Uniform strategies, rational relations and jumping automata. Inf. Comput. 242, 80–107 (2015). doi:10.1016/j.ic.2015.03.012

    Article  MathSciNet  MATH  Google Scholar 

  12. Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Nagel, E. (ed.) Logic, Methodology, and Philosophy of Science: Proceedings of the 1960 International Congress, pp. 1–11. Stanford University Press, Palo Alto (1962)

    Google Scholar 

  13. Calbrix, H., Nivat, M., Podelski, A.: Ultimately periodic words of rational \(\omega \)-languages. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) MFPS 1993. LNCS, vol. 802, pp. 554–566. Springer, Heidelberg (1994). doi:10.1007/3-540-58027-1_27

    Chapter  Google Scholar 

  14. Carton, O., Choffrut, C., Grigorieff, S.: Decision problems among the main subfamilies of rational relations. RAIRO-Theor. Inform. Appl. 40(02), 255–275 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  15. Caucal, D.: Synchronization of pushdown automata. In: Ibarra, O.H., Dang, Z. (eds.) DLT 2006. LNCS, vol. 4036, pp. 120–132. Springer, Heidelberg (2006). doi:10.1007/11779148_12

    Chapter  Google Scholar 

  16. Filiot, E., Jecker, I., Löding, C., Winter, S.: On equivalence and uniformisation problems for finite transducers. In: 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016. LIPIcs, vol. 55, p. 125:1–125:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016). doi:10.4230/LIPIcs.ICALP.2016.125

  17. Frougny, C., Sakarovitch, J.: Synchronized rational relations of finite and infinite words. Theor. Comput. Sci. 108(1), 45–82 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  18. Harju, T., Karhumäki, J.: The equivalence problem of multitape finite automata. Theor. Comput. Sci. 78(2), 347–355 (1991). doi:10.1016/0304-3975(91)90356-7

    Article  MathSciNet  MATH  Google Scholar 

  19. Khoussainov, B., Nerode, A.: Automatic presentations of structures. In: Leivant, D. (ed.) LCC 1994. LNCS, vol. 960, pp. 367–392. Springer, Heidelberg (1995). doi:10.1007/3-540-60178-3_93

    Chapter  Google Scholar 

  20. Kuske, D., Lohrey, M.: First-order and counting theories of \(\omega \)-automatic structures. In: Aceto, L., Ingólfsdóttir, A. (eds.) FoSSaCS 2006. LNCS, vol. 3921, pp. 322–336. Springer, Heidelberg (2006). doi:10.1007/11690634_22

    Chapter  Google Scholar 

  21. Löding, C., Repke, S.: Regularity problems for weak pushdown \(\omega \)-automata and games. In: Rovan, B., Sassone, V., Widmayer, P. (eds.) MFCS 2012. LNCS, vol. 7464, pp. 764–776. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32589-2_66

    Chapter  Google Scholar 

  22. Pǎun, G., Salomaa, A.: Thin and slender languages. Discret. Appl. Math. 61(3), 257–270 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  23. Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. In: 21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006), pp. 255–264. IEEE (2006)

    Google Scholar 

  24. Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM J. Res. Dev. 3(2), 114–125 (1959)

    Article  MathSciNet  MATH  Google Scholar 

  25. Sakarovitch, J.: Elements of Automata Theory. Cambridge University Press, New York (2009)

    Book  MATH  Google Scholar 

  26. Srba, J.: Visibly pushdown automata: from language equivalence to simulation and bisimulation. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 89–103. Springer, Heidelberg (2006). doi:10.1007/11874683_6

    Chapter  Google Scholar 

  27. Stearns, R.E.: A regularity test for pushdown machines. Inf. Control 11(3), 323–340 (1967)

    Article  MATH  Google Scholar 

  28. Tao, Y.: Infinity problems and countability problems for \(\omega \)-automata. Inf. Process. Lett. 100(4), 151–153 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  29. Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, vol. B, pp. 133–191 (1990)

    Google Scholar 

  30. Thomas, W.: Infinite trees and automation-definable relations over \(\omega \)-words. Theor. Comput. Sci. 103(1), 143–159 (1992). doi:10.1016/0304-3975(92)90090-3

    Article  MATH  Google Scholar 

  31. Thomas, W.: Facets of synthesis: revisiting Church’s problem. In: Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 1–14. Springer, Heidelberg (2009). doi:10.1007/978-3-642-00596-1_1

    Chapter  Google Scholar 

  32. Valiant, L.G.: Regularity and related problems for deterministic pushdown automata. J. ACM (JACM) 22(1), 1–10 (1975)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Christopher Spinrath .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer-Verlag GmbH Germany

About this paper

Cite this paper

Löding, C., Spinrath, C. (2017). Decision Problems for Subclasses of Rational Relations over Finite and Infinite Words. In: Klasing, R., Zeitoun, M. (eds) Fundamentals of Computation Theory. FCT 2017. Lecture Notes in Computer Science(), vol 10472. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-55751-8_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-55751-8_27

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-55750-1

  • Online ISBN: 978-3-662-55751-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics