|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
22nd Annual Symposium on Foundations of Computer Science (FOCS 1981)
Propositional dynamic logic of context-free programs
October 28-October 30
| ASCII Text | x | ||
| David Harel, Amir Pnueli, Jonathan Stavi, "Propositional dynamic logic of context-free programs," Foundations of Computer Science, IEEE Annual Symposium on, pp. 310-321, 22nd Annual Symposium on Foundations of Computer Science (FOCS 1981), 1981. | |||
| BibTex | x | ||
| @article{ 10.1109/SFCS.1981.38, author = {David Harel and Amir Pnueli and Jonathan Stavi}, title = {Propositional dynamic logic of context-free programs}, journal ={Foundations of Computer Science, IEEE Annual Symposium on}, volume = {0}, year = {1981}, issn = {0272-5428}, pages = {310-321}, doi = {http://doi.ieeecomputersociety.org/10.1109/SFCS.1981.38}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - Foundations of Computer Science, IEEE Annual Symposium on TI - Propositional dynamic logic of context-free programs SN - 0272-5428 SP310 EP321 A1 - David Harel, A1 - Amir Pnueli, A1 - Jonathan Stavi, PY - 1981 VL - 0 JA - Foundations of Computer Science, IEEE Annual Symposium on ER - | |||
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SFCS.1981.38
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.
Citation:
David Harel, Amir Pnueli, Jonathan Stavi, "Propositional dynamic logic of context-free programs," focs, pp.310-321, 22nd Annual Symposium on Foundations of Computer Science (FOCS 1981), 1981
Usage of this product signifies your acceptance of the Terms of Use.