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