top

An essay in combinatory dynamic logic

S. Passy and T. Tinchev. An essay in combinatory dynamic logic. Information and Computation, 93:263–332, 1991.

Download: (unavailable)

Abstract:

The language of combinatory propositional dynamic logic (CPDL) is an enrichment of PDL by the universal modality and so-called names. The universal modality is an S5 modality with the extra requirement that the relation is the total relation on every frame; and the names are like proposition variables but are true at exactly one point. These two ingredients in CPDL remedy some deficiencies of PDL that result from its restricted expressive power. In addition to the axioms and rules that follow from the given interpretation the authors add the following rule: $$(\rm cov)\quad \rm If \vdash[\gamma]c \rm for all names c \rm then \vdash[\gamma]0.$$ Given that we have countably many names, only countable frames satisfy (cov), and frames are CPDL-equivalent if and only if they are isomorphic. The essay starts with a historical chapter on PDL and CPDL that is worth reading even if one is not interested in the special topic of this paper. We are presented with the considerations that have led to the particular choice of extension of PDL. Then follows a chapter on "pure" CPDL, its proof theory and semantics. The third part takes us through a maze of possible ways to enrich or strengthen CPDL, starting with the logic of deterministic atomic programs, continuing with definitional extensions such as adding equality statements for programs or negations and converses; and concluding with additions to handle infinities in computations. The fourth and final chapter discusses the effects of adding quantifiers over names.

BibTeX: (download)

@ARTICLE{passy91,
  author = {S. Passy and T. Tinchev},
  title = {An essay in combinatory dynamic logic},
  journal = {Information and Computation},
  year = {1991},
  volume = {93},
  pages = {263-332},
  abstract = {
	The language of combinatory propositional dynamic logic (CPDL) is
	an enrichment of PDL by the universal modality and so-called names.
	The universal modality is an S5 modality with the extra requirement
	that the relation is the total relation on every frame; and the names
	are like proposition variables but are true at exactly one point.
	These two ingredients in CPDL remedy some deficiencies of PDL that
	result from its restricted expressive power. In addition to the axioms
	and rules that follow from the given interpretation the authors add
	the following rule: $$({\rm cov})\quad {\rm If} \vdash[\gamma]c {\rm
	for all names} c\ {\rm then} \vdash[\gamma]0.$$ Given that we have
	countably many names, only countable frames satisfy (cov), and frames
	are CPDL-equivalent if and only if they are isomorphic.
	The essay starts with a historical chapter on PDL and CPDL that is
	worth reading even if one is not interested in the special topic
	of this paper. We are presented with the considerations that have
	led to the particular choice of extension of PDL. Then follows a
	chapter on "pure" CPDL, its proof theory and semantics. The third
	part takes us through a maze of possible ways to enrich or strengthen
	CPDL, starting with the logic of deterministic atomic programs, continuing
	with definitional extensions such as adding equality statements for
	programs or negations and converses; and concluding with additions
	to handle infinities in computations. The fourth and final chapter
	discusses the effects of adding quantifiers over names. }
}

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