Abstract
It is shown that PDL remains decidable when we allow as programs regular expressions over a finite alphabet as well as over the single context free program A‡B‡ = {AiBi | i ≥ 0}. The decision algorithm constructs a finite push-down model for all satisfiable PDL RG(A‡B‡) formulas. Generalization to additional context free programs whose addition does not destroy decidability is discussed.
This research was supported in part by a grant from the Israeli Academy of Science — the Basic Research Foundation. The work is part of the first author's Ph.D. thesis.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Ben Ari, M. — Complexity of Proofs and Models in Programming Languages. Ph.D. Thesis, Tel Aviv University, June 1981.
Fischer, M.J. and Ladner, R.E. — Propositional Logic of Regular Programs. JCSS 18:2.
Harel, D., Pneuli, A., Stavi, J. — Propositional Dynamic Logic of Nonregular Programs — FOCS 81.
Harel, D., Pnueli, A., Stavi, J. — Further Results on Propositional Dynamic Logic of Nonregular Programs — Workshop on Program Logics, Yorktown Heights, May 1981, Springer Verlag, Ed. D. Kozen.
Pratt, V.R. — Sementical Considerations of Floyd-Hoare Logic — Proc. of 17-th FOCS (1976), 109–121.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1984 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Koren, T., Pnueli, A. (1984). There exist decidable context free propositonal dynamic logics. In: Clarke, E., Kozen, D. (eds) Logics of Programs. Logic of Programs 1983. Lecture Notes in Computer Science, vol 164. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-12896-4_369
Download citation
DOI: https://doi.org/10.1007/3-540-12896-4_369
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-12896-0
Online ISBN: 978-3-540-38775-6
eBook Packages: Springer Book Archive