up: Publications

C2PDLS: A Combination of Combinatory and Converse PDL with Substitutions

Jon Haël Brenas, Rachid Echahed, Martin Strecker


We introduce a logic called C2PDLS, motivated by some reasoning about graph rewriting systems. C2PDLS is an extension of both combinatory propositional dynamic logic, usually written CPDL, and converse propositional dynamic logic, usually written CPDL too. In addition to the existing features of both CPDLs, the introduced logic offers the possibility to use the notion of substitutions à la Hoare within its formulae. Such substitutions reflect the effect of some actions on graph structures such as addition or deletion of edges or nodes. These last features led us to introduce restricted universal roles over subsets of the universe. We propose a sound and complete deductive system for C2PDLS and show that its validity problem is decidable.
 Online Copy

Online version (as PDF)

BibTeX Entry

  author    = {Jon Ha{\"{e}}l Brenas and
               Rachid Echahed and
               Martin Strecker},
  title     = {{C2PDLS:} {A} Combination of Combinatory and Converse {PDL} with Substitutions},
  booktitle = {{SCSS} 2017, The 8th International Symposium on Symbolic Computation
               in Software Science 2017, April 6-9, 2017, Gammarth, Tunisia},
  pages     = {29--41},
  year      = 2017,
  editor    = {Mohamed Mosbah and Micha{\"{e}}l Rusinowitch},
  url       = {https://easychair.org/publications/paper/dx4z}

Sat Dec 30 15:37:10 CET 2017