top

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