The Propositional Dynamic Logic of Deterministic, Well-Structured Programs
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 tim...
| Main Authors: | , |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/149009 |
| _version_ | 1811087643469938688 |
|---|---|
| author | Halpern, Joseph Y. Reif, John H. |
| author_facet | Halpern, Joseph Y. Reif, John H. |
| author_sort | Halpern, Joseph Y. |
| collection | MIT |
| description | 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 expensive than PDL. The results rely on structure theorems for models of satifiable SDPDL formulas, and the proods give insight into the effects of nondeterminism on intractability and expressiveness in program logics. |
| first_indexed | 2024-09-23T13:49:43Z |
| id | mit-1721.1/149009 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T13:49:43Z |
| publishDate | 2023 |
| record_format | dspace |
| spelling | mit-1721.1/1490092023-03-30T03:35:50Z The Propositional Dynamic Logic of Deterministic, Well-Structured Programs Halpern, Joseph Y. Reif, John H. 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 expensive than PDL. The results rely on structure theorems for models of satifiable SDPDL formulas, and the proods give insight into the effects of nondeterminism on intractability and expressiveness in program logics. 2023-03-29T14:18:58Z 2023-03-29T14:18:58Z 1981-03 https://hdl.handle.net/1721.1/149009 8012572 MIT-LCS-TM-198 application/pdf |
| spellingShingle | Halpern, Joseph Y. Reif, John H. The Propositional Dynamic Logic of Deterministic, Well-Structured Programs |
| title | The Propositional Dynamic Logic of Deterministic, Well-Structured Programs |
| title_full | The Propositional Dynamic Logic of Deterministic, Well-Structured Programs |
| title_fullStr | The Propositional Dynamic Logic of Deterministic, Well-Structured Programs |
| title_full_unstemmed | The Propositional Dynamic Logic of Deterministic, Well-Structured Programs |
| title_short | The Propositional Dynamic Logic of Deterministic, Well-Structured Programs |
| title_sort | propositional dynamic logic of deterministic well structured programs |
| url | https://hdl.handle.net/1721.1/149009 |
| work_keys_str_mv | AT halpernjosephy thepropositionaldynamiclogicofdeterministicwellstructuredprograms AT reifjohnh thepropositionaldynamiclogicofdeterministicwellstructuredprograms AT halpernjosephy propositionaldynamiclogicofdeterministicwellstructuredprograms AT reifjohnh propositionaldynamiclogicofdeterministicwellstructuredprograms |