@ARTICLE{gargov88:_deter_pdl,
author = {G. Gargov and S. Passy},
title = {Determinism and looping in combinatory PDL},
journal = {Theoretical Computer Science},
year = {1988},
volume = {61},
pages = {259--277},
abstract = {
Combinatory propositional dynamic logic, CPDL, is the variant of PDL
in which proper names of states are added (in every model, every
name corresponds to exactly one state).
Two extensions of CPDL are considered in the paper: the deterministic
version CDPDL, and the CPDL with the looping operator `repeat'.
It was known that the axiom system for CDPDL (containing in addition
to that of CPDL only the axiom scheme $\langle \alpha\rangle A\to[\alpha]A$
for any atomic program $\alpha)$ is complete with respect to deterministic
models. In the paper it is proved that the system has the finite
model property and is decidable.
Considering the CPDL with the `repeat' construct (RCPDL), the authors
prove that the axiom system of RCPDL (which is that of CPDL plus
two axioms proposed by R. Streett) is complete and decidable, and
has the finite model property. }
}