## Determinism and looping in combinatory PDL

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

#### Download: (unavailable)

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

#### BibTeX: (download)

@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