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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 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.
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
Abdulla, P.A.: Regular model checking. STTT 14(2), 109–118 (2012). doi:10.1007/s10009-011-0216-8
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)
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
Berstel, J.: Transductions and Context-Free Languages. Springer, Stuttgart (1979)
Bird, M.: The equivalence problem for deterministic two-tape automata. J. Comput. Syst. Sci. 7(2), 218–236 (1973)
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)
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
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
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
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
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
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)
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
Carton, O., Choffrut, C., Grigorieff, S.: Decision problems among the main subfamilies of rational relations. RAIRO-Theor. Inform. Appl. 40(02), 255–275 (2006)
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
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
Frougny, C., Sakarovitch, J.: Synchronized rational relations of finite and infinite words. Theor. Comput. Sci. 108(1), 45–82 (1993)
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
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
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
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
Pǎun, G., Salomaa, A.: Thin and slender languages. Discret. Appl. Math. 61(3), 257–270 (1995)
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)
Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM J. Res. Dev. 3(2), 114–125 (1959)
Sakarovitch, J.: Elements of Automata Theory. Cambridge University Press, New York (2009)
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
Stearns, R.E.: A regularity test for pushdown machines. Inf. Control 11(3), 323–340 (1967)
Tao, Y.: Infinity problems and countability problems for \(\omega \)-automata. Inf. Process. Lett. 100(4), 151–153 (2006)
Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, vol. B, pp. 133–191 (1990)
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
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
Valiant, L.G.: Regularity and related problems for deterministic pushdown automata. J. ACM (JACM) 22(1), 1–10 (1975)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights 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)