An Isaac Newton Institute Workshop

Logic and Databases

Complete axiomatisation for PDLpath.

Authors: Natasha Alechina (University of Nottingham), Dmitry Shkatov (University of Nottingham)


PDLpath is a logic introduced in [1] to express path constraints on graphs of semistructured data. Its language contains one nominal r, which is true at the root node, standard PDL modalities, converse, and a new modality #, which stands for "some edge label". We assume that the language contains countably infinitely many atomic modalities or labels. We provide a complete axiomatisation of PDLpath and a new decidability proof for it (another proof is in [1]).

[1] N. Alechina, S. Demri and M. de Rijke. A modal perspective on path constraints. Journal of Logic and Computation, 6(3), 2003, pages 939-956.