C2PDLS: A Combination of Combinatory and Converse PDL with Substitutions
Keyword(s):
We introduce a logic called C2PDLS, motivated by some reasoningabout graph rewriting systems. C2PDLS is an extension of bothcombinatory propositional dynamic logic, usually written CPDL,and converse propositional dynamic logic, usually written CPDLtoo. In addition to the existing features of both CPDLs, theintroduced logic offers the possibility to use the notion ofsubstitutions à la Hoare within its formulae. Such substitutionsreflect the effect of some actions on graph structures such asaddition or deletion of edges or nodes. These last features ledus to introduce restricted universal roles over subsets of theuniverse. We propose a sound and complete deductive system forC2PDLS and show that its validity problem is decidable.
2005 ◽
Vol 127
(5)
◽
pp. 113-132
2019 ◽
Vol 286
◽
pp. 65-78