Propositional dynamic logic of context-free programs
- 1 October 1981
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 02725428,p. 310-321
- https://doi.org/10.1109/sfcs.1981.38
Abstract
The borderline between decidable and undecidable Propositional Dynamic Logic (PDL) is sought when iterative programs represented by regular expressions are augmented with increasingly more complex recursive programs represented by context-free languages. The results in this paper and its companion [HPS] indicate that this line is extremely close to the original regular PDL. The main result of the present paper is: The validity problem for PDL with additional programs αΔ(β)γΔ for regular α, β and γ, defined as Uiαi; β; γi, is Π11-complete. One of the results of [HPS] shows that the single program AΔ(B) AΔ for atomic A and B is actually sufficient for obtaining Π11- completeness. However, the proofs of this paper use different techniques which seem to be worthwhile in their own right.Keywords
This publication has 10 references indexed in Scilit:
- Further results on propositional dynamic logic of nonregular programsPublished by Springer Nature ,2005
- ENUMERABLE SETS ARE DIOPHANTINEPublished by World Scientific Pub Co Pte Ltd ,2003
- The decidability of equivalence for a family of linear grammarsInformation and Control, 1980
- Superdeterministic PDAsJournal of the ACM, 1980
- A near-optimal method for reasoning about actionJournal of Computer and System Sciences, 1980
- Propositional dynamic logic of regular programsJournal of Computer and System Sciences, 1979
- Two decidability results for deterministic pushdown automataJournal of Computer and System Sciences, 1979
- Semantical consideration on floyo-hoare logicPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1976
- Hilbert’s tenth problem: Diophantine equations: positive aspects of a negative solutionPublished by American Mathematical Society (AMS) ,1976
- On the completeness of the inductive assertion methodJournal of Computer and System Sciences, 1975