PDL with data constants

S. Passy and T. Tinchev. PDL with data constants. Information Processing Letters, 20:35–41, 1985.

Download: (unavailable)

Abstract:

Extending the propositional dynamic logic with new (propositional) constants and axioms for them, we obtain a conservative extension and call it combinatory PDL (CPDL). Due to capturing the `identity of states' in CPDL, its expressive power, as compared to PDL, strongly increases. In CPDL we include $\alpha\cap\beta$ (the intersection of the programs $\alpha$ and $\beta$), $øverline\alpha$ (the complement of the program $\alpha$)---both of them being inexpressible in PDL---and formulas $\alpha\subset\beta$ and $\alpha=\beta$ as well as all traditional PDL operators $(\alpha\sp -1,\alpha\cup\beta,\alpha\sp *,\alpha\beta,A?)$. The axioms proposed are shown to be Kripke complete. CPDL is shown to be highly undecidable.

BibTeX: (download)

@ARTICLE{passy85:_pdl,
  author = {S. Passy and T. Tinchev},
  title = {PDL with data constants},
  journal = {Information Processing Letters},
  year = {1985},
  volume = {20},
  pages = {35--41},
  abstract = {
	Extending the propositional dynamic logic with new (propositional)
	constants and axioms for them, we obtain a conservative extension
	and call it combinatory PDL (CPDL). Due to capturing the `identity
	of states' in CPDL, its expressive power, as compared to PDL, strongly
	increases. In CPDL we include $\alpha\cap\beta$ (the intersection
	of the programs $\alpha$ and $\beta$), $\overline\alpha$ (the complement
	of the program $\alpha$)---both of them being inexpressible in PDL---and
	formulas $\alpha\subset\beta$ and $\alpha=\beta$ as well as all traditional
	PDL operators $(\alpha\sp {-1},\alpha\cup\beta,\alpha\sp *,\alpha\beta,A?)$.
	The axioms proposed are shown to be Kripke complete. CPDL is shown
	to be highly undecidable. }
}