The propositional dynamic logic of deterministic, well-structured programs
type: Item
instance of: scholarly article
title: The propositional dynamic logic of deterministic, well-structured programs
zbMATH Open document ID: 0552.68035
DOI: 10.1016/0304-3975(83)90097-X
author: Joseph Y. Halpern
author: J. Reif
published in: Theoretical Computer Science
publication date: 1983-01-01T00:00:00Z
review text: PDL is the propositional dynamic logic of regular programs. DPDL is the propositional dynamic logic of regular programs built from deterministic atomic programs. SDPDL is the propositional dynamic logic of deterministic well-structured programs, i.e., programs that are built from deterministic atomic programs by means of the while and if constructs. The main results of the paper are that SDPDL is strictly less expressive than DPDL, and that the validity problem for SDPDL is logspace complete for PSPACE (the validity problems for PDL and DPDL are logspace complete for EXPTIME). The results carry a special significance, since they indicate that the exponential lower bound by Fischer and Ladner for PDL may not be all that realistic.
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03D15
Mathematics Subject Classification ID: 03B45
zbMATH DE Number: 3880103
zbMATH Keywords: determinism
zbMATH Keywords: decision procedure
zbMATH Keywords: expressiveness
zbMATH Keywords: polynomial space completeness
zbMATH Keywords: regular programs
zbMATH Keywords: propositional dynamic logic
zbMATH Keywords: well- structured programs
zbMATH Keywords: validity problems
MaRDI profile type: Publication
cites work: Deterministic propositional dynamic logic: finite models, complexity, and completeness
cites work: Q3957927
cites work: Q4746782
cites work: Propositional dynamic logic of regular programs
cites work: Theory of program structures: Schemes, semantics, verification
cites work: Q3862379
cites work: An elementary proof of the completeness of PDL
cites work: Q3968454
cites work: Expressing program looping in regular dynamic logic
cites work: Q5626601
cites work: Q4748128
cites work: A near-optimal method for reasoning about action
cites work: Q3953158
cites work: Q5596237
cites work: Relationships between nondeterministic and deterministic tape complexities
full work available at URL: 0304-3975(83)90097-x
OpenAlex ID: W2101982422
description: scientific article; zbMATH DE number 3880103