The propositional dynamic logic of deterministic, well-structured programs
Publication
, Journal Article
Halpern, JY; Reif, JH
Published in: Theoretical Computer Science
January 1, 1983
We consider a restricted propositional dynamic logic, Strict Deterministic Propositional Dynamic Logic (SDPDL), which is appropriate for reasoning about deterministic well-structured programs. In contrast to PDL, for which the validity problem is known to be complete in deterministic exponential time, the validity problem for SDPDL is shown to be polynomial space complete. We also show that SDPDL is less expressive than PDL, and give a complete axiomatization for it. The results rely on structure theorems for models of satisfiable SDPDL formulas, and the proofs give insight into the effects of nondeterminism on intractability and expressiveness in program logics. © 1983.
Duke Scholars
Published In
Theoretical Computer Science
DOI
ISSN
0304-3975
Publication Date
January 1, 1983
Volume
27
Issue
1-2
Start / End Page
127 / 165
Related Subject Headings
- Computation Theory & Mathematics
- 49 Mathematical sciences
- 46 Information and computing sciences
- 08 Information and Computing Sciences
- 01 Mathematical Sciences
Citation
APA
Chicago
ICMJE
MLA
NLM
Halpern, J. Y., & Reif, J. H. (1983). The propositional dynamic logic of deterministic, well-structured programs. Theoretical Computer Science, 27(1–2), 127–165. https://doi.org/10.1016/0304-3975(83)90097-X
Halpern, J. Y., and J. H. Reif. “The propositional dynamic logic of deterministic, well-structured programs.” Theoretical Computer Science 27, no. 1–2 (January 1, 1983): 127–65. https://doi.org/10.1016/0304-3975(83)90097-X.
Halpern JY, Reif JH. The propositional dynamic logic of deterministic, well-structured programs. Theoretical Computer Science. 1983 Jan 1;27(1–2):127–65.
Halpern, J. Y., and J. H. Reif. “The propositional dynamic logic of deterministic, well-structured programs.” Theoretical Computer Science, vol. 27, no. 1–2, Jan. 1983, pp. 127–65. Scopus, doi:10.1016/0304-3975(83)90097-X.
Halpern JY, Reif JH. The propositional dynamic logic of deterministic, well-structured programs. Theoretical Computer Science. 1983 Jan 1;27(1–2):127–165.
Published In
Theoretical Computer Science
DOI
ISSN
0304-3975
Publication Date
January 1, 1983
Volume
27
Issue
1-2
Start / End Page
127 / 165
Related Subject Headings
- Computation Theory & Mathematics
- 49 Mathematical sciences
- 46 Information and computing sciences
- 08 Information and Computing Sciences
- 01 Mathematical Sciences