
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. } }
Generated by bib2html.pl (written by Patrick Riley ) on Mon Aug 10, 2009 14:52:33