skip to content

Complete axiomatisation for PDLpath

Thursday 2nd March 2006 - 16:15 to 17:00
INI Seminar Room 1

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.

University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons