Abstract
We introduce PEP, the Post Embedding Problem, a variant of PCP where one compares strings with the subword relation, and PEP reg, a further variant where solutions are constrained and must belong to a given regular language. PEP reg is decidable but not primitive recursive. This entails the decidability of reachability for unidirectional systems with one reliable and one lossy channel.
Work supported by the Agence Nationale de la Recherche, grant ANR-06-SETIN-001.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abdulla, P.A., Baier, C., Purushothaman Iyer, S., Jonsson, B.: Simulating perfect channels with probabilistic lossy channels. Information and Computation 197(1–2), 22–40 (2005)
Abdulla, P.A., Deneux, J., Ouaknine, J., Worrell, J.: Decidability and complexity results for timed automata via channel machines. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1089–1101. Springer, Heidelberg (2005)
Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Information and Computation 127(2), 91–101 (1996)
Amadio, R., Meyssonnier, Ch.: On decidability of the control reachability problem in the asynchronous π-calculus. Nordic Journal of Computing 9(2), 70–101 (2002)
Chambard, P., Schnoebelen, Ph.: Post embedding problem is not primitive recursive, with applications to channel systems. Research Report LSV-07-28, Lab. Specification and Verification, ENS de Cachan, Cachan, France (September 2007)
Demri, S., Lazić, R.: LTL with the freeze quantifier and register automata. In: Proc. LICS 2006, pp. 17–26. IEEE Comp. Soc. Press, Los Alamitos (2006)
Finkel, A.: Decidability of the termination problem for completely specificied protocols. Distributed Computing 7(3), 129–135 (1994)
Gabelaia, D., Kurucz, A., Wolter, F., Zakharyaschev, M.: Non-primitive recursive decidability of products of modal logics with expanding domains. Annals of Pure and Applied Logic 142(1–3), 245–268 (2006)
Halava, V., Hirvensalo, M., de Wolf, R.: Marked PCP is decidable. Theoretical Computer Science 255(1–2), 193–204 (2001)
Konev, B., Wolter, F., Zakharyaschev, M.: Temporal logics over transitive states. In: Nieuwenhuis, R. (ed.) Automated Deduction – CADE-20. LNCS (LNAI), vol. 3632, pp. 182–203. Springer, Heidelberg (2005)
Lasota, S., Walukiewicz, I.: Alternating timed automata. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 250–265. Springer, Heidelberg (2005)
Ouaknine, J., Worrell, J.: On the decidability and complexity of Metric Temporal Logic over finite words. Logical Methods in Comp. Science 3(1), 1–27 (2007)
Ruohonen, K.: On some variants of Post’s correspondence problem. Acta Informatica 4(19), 357–367 (1983)
Schnoebelen, P.: Bisimulation and other undecidable equivalences for lossy channel systems. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 385–399. Springer, Heidelberg (2001)
Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity. Information Processing Letters 83(5), 251–261 (2002)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chambart, P., Schnoebelen, P. (2007). Post Embedding Problem Is Not Primitive Recursive, with Applications to Channel Systems. In: Arvind, V., Prasad, S. (eds) FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2007. Lecture Notes in Computer Science, vol 4855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-77050-3_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-77050-3_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-77049-7
Online ISBN: 978-3-540-77050-3
eBook Packages: Computer ScienceComputer Science (R0)