PDL with data constants

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

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$), $&oslash;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.

@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

Hybrid Logics
Resources