## Determinism and looping in combinatory PDL

G. Gargov and S. Passy. Determinism and looping in combinatory PDL. Theoretical Computer Science, 61:259–277, 1988.

#### 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.

@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. }
}


Generated by bib2html.pl (written by Patrick Riley ) on Mon Aug 10, 2009 14:52:33

Hybrid Logics
Resources