Abstract
We extend the propositional dynamic logic PDL of Fischer and Ladner with a restricted kind of recursive programs using the formalism of visibly pushdown automata (Alur, Madhusudan 2004). We show that the satisfiability problem for this extension remains decidable, generalising known decidability results for extensions of PDL by non-regular programs.
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
Alur, R., Chaudhuri, S., Madhusudan, P.: A fixpoint calculus for local and global program flows. In: Proceedings of POPL 2006 (to appear 2006)
Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 467–481. Springer, Heidelberg (2004)
Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proceedings of STOC 2004, pp. 202–211. ACM, New York (2004)
Danecki, R.: Nondeterministic propositional dynamic logic with intersection is decidable. In: Skowron, A. (ed.) SCT 1984. LNCS, vol. 208, pp. 34–53. Springer, Heidelberg (1985)
Fischer, M.J., Ladner, R.E.: Propositional dyncamic logic of regular programs. Journal of Computer and System Sciences 18(2), 194–211 (1979)
Harel, D., Kaminsky, M.: Strengthened results on nonregular PDL. Technical Report MCS99-13, Weizmann Institute of Science (1999)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. In: Foundations of Computing, MIT Press, Cambridge (2000)
Harel, D., Raz, D.: Deciding properties of nonregular programs. SIAM Journal on Computing 22(4), 857–874 (1993)
Harel, D., Singerman, E.: More on nonregular PDL: Expressive power, finite models, fibonacci programs. In: ISTCS: 3rd Israeli Symposium on the Theory of Computing and Systems (1995)
Löding, C., Madhusudan, P., Serre, O.: Visibly pushdown games. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 408–420. Springer, Heidelberg (2004)
Lutz, C.: PDL with intersection and converse is decidable. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 413–427. Springer, Heidelberg (2005)
Parikh, R.: The logic of games an its applications. Annals of discrete mathematics 24, 111–140 (1985)
Park, D.: Finiteness is μ-ineffable. Theoretical Computer Science 3, 173–181 (1976)
Streett, R.: Propositional dynamic logic of looping and converse is elementary decidable. Information and Control 54, 121–141 (1982)
Thomas, W.: Languages, automata, and logic. In: Handbook of Formal Language Theory, vol. III, pp. 389–455. Springer, Heidelberg (1997)
Vardi, M., Wolper, P.: Automata-theoretic techniques for modal logic of programs. Journal of Computer and System Sciences 32, 183–221 (1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Löding, C., Serre, O. (2006). Propositional Dynamic Logic with Recursive Programs. In: Aceto, L., Ingólfsdóttir, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2006. Lecture Notes in Computer Science, vol 3921. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11690634_20
Download citation
DOI: https://doi.org/10.1007/11690634_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33045-5
Online ISBN: 978-3-540-33046-2
eBook Packages: Computer ScienceComputer Science (R0)