The prepositional dynamic logic of deterministic, well-structured programs
- 1 October 1981
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 02725428,p. 322-334
- https://doi.org/10.1109/sfcs.1981.49
Abstract
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. 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.Keywords
This publication has 6 references indexed in Scilit:
- An elementary proof of the completeness of PDLTheoretical Computer Science, 1981
- Finite models for deterministic propositional dynamic logicLecture Notes in Computer Science, 1981
- Models of program logicsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1979
- Propositional modal logic of programsPublished by Association for Computing Machinery (ACM) ,1977
- Theory of Program Structures: Schemes, Semantics, VerificationPublished by Springer Nature ,1975
- Relationships between nondeterministic and deterministic tape complexitiesJournal of Computer and System Sciences, 1970