Abstract
Post’s Embedding Problem is a new variant of Post’s Correspondence Problem where words are compared with embedding rather than equality. It has been shown recently that adding regular constraints on the form of admissible solutions makes the problem highly non-trivial, and relevant to the study of lossy channel systems. Here we consider the infinitary version and its application to recurrent reachability in lossy channel systems.
Work supported by the Agence Nationale de la Recherche, grant ANR-06-SETIN-001.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
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.: Undecidable verification problems for programs with unreliable channels. Information and Computation 130(1), 71–90 (1996)
Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Information and Computation 127(2), 91–101 (1996)
Amadio, R., Meyssonnier, C.: On decidability of the control reachability problem in the asynchronous π-calculus. Nordic Journal of Computing 9(2), 70–101 (2002)
Baier, C., Bertrand, N., Schnoebelen, P.: On computing fixpoints in well-structured regular model checking, with applications to lossy channel systems. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 347–361. Springer, Heidelberg (2006)
Chambart, P.: Canaux fiables et non-fiables: frontières de la décidabilité. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France (September 2007)
Chambart, P., Schnoebelen, P.: Post embedding problem is not primitive recursive, with applications to channel systems. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 265–276. Springer, Heidelberg (2007)
Delzanno, G.: Constraint-based automatic verification of abstract models of multithreaded programs. Theory and Practice of Logic Programming 7(1–2), 67–91 (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.: Une généralisation des théorèmes de Higman et de Simon aux mots infinis. Theoretical Computer Science 38(1), 137–142 (1985)
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)
Jurdziński, M., Lazić, R.: Alternation-free modal mu-calculus for data trees. In: Proc. LICS 2007, pp. 131–140. IEEE Comp. Soc. Press, Los Alamitos (2007)
Konev, B., Wolter, F., Zakharyaschev, M.: Temporal logics over transitive states. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 182–203. Springer, Heidelberg (2005)
Kurucz, A.: Combining modal logics. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logics, vol. 3, ch. 15, pp. 869–926. Elsevier, Amsterdam (2006)
Lasota, S., Walukiewicz, I.: Alternating timed automata. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 250–265. Springer, Heidelberg (2005)
Lazić, R., Newcomb, T., Ouaknine, J., Roscoe, A.W., Worrell, J.: Nets with tokens which carry data. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 301–320. Springer, Heidelberg (2007)
Ouaknine, J., Worrell, J.: On metric temporal logic and faulty Turing machines. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, pp. 217–230. Springer, Heidelberg (2006)
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)
Pachl, J.K.: Protocol description and analysis based on a state transition model with channel expressions. In: Proc. PSTV 1987, pp. 207–219. North-Holland, Amsterdam (1987)
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
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chambart, P., Schnoebelen, P. (2008). The ω-Regular Post Embedding Problem. In: Amadio, R. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2008. Lecture Notes in Computer Science, vol 4962. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78499-9_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-78499-9_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78497-5
Online ISBN: 978-3-540-78499-9
eBook Packages: Computer ScienceComputer Science (R0)