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.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
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