Location

Laboratoire Spécification et Vérification
École Normale Supérieure de Cachan
Cachan, France

Title: PDL Model-Checking on Trees

Context

Propositional Dynamic Logic (PDL) on trees [1], aka Regular XPath [12], is a widely used formalism to reason on trees. This is a pretty intuitive logic for navigating inside a tree; for instance the formula ⟨ ↓⟩(a∧ ⟨→^∗⟩ b) holds at a tree node with two children, one labeled by a and the other to its right labeled by b (in the more verbose XPath syntax, this would be child::a/following-sibling::b).

PDL on trees has applications in

linguistics

[3, 10], where the trees can be for instance syntactic trees,

databases

[12, 5], where the trees are XML representations of hierarchical data, and

verification

[13], where the trees are simply unfoldings of possible program executions.

Although the PDL model-checking of a single tree can be carried out efficiently in PTime [11], the model-checking of a regular set of trees and the satisfiability problems suffer from a general ExpTime-hardness complexity [7].

Objectives

Depending on the interests of the student, this research internship can take a theoretical or a practical turn.

Theory:

the complexity of model-checking a tree language can vary considerably depending on the considered fragment of PDL and the restrictions put on the tree language [2, 9]. An interesting way of introducing new restrictions on tree languages is to consider the sets of parse trees of a context-free grammar for a sentence. These parse trees have a very specific form, which could be amenable to more efficient processing (e.g. NPTime and PSpace algorithms depending on the restrictions).

Practice:

decision procedures for PDL on trees often rely on the construction of tree automata [5, 6, 8]. Here the issue is that a naive implementation of these algorithms is too explosive, and a symbolic representation of the state space of the automaton is required. Some typical techniques could be employed to this end: binary decision diagrams, which have been very successful in verification problems, and antichain representations [4], which are less well investigated on tree automata. Using a symbolic representation is only the beginning of the story: we next need algorithms working directly on this representation for the most important operations: emptiness, intersection, Hadamard product, etc. These ideas have to be implemented in order to demonstrate their practical value.

This subject is reasonably self-contained, but there is an abundance of practical and theoretical questions that would allow to pursue this line of research during a PhD.

Contact

S. Schmitz
Tél: (+33/0) 147 407 542
Email: schmitz@lsv.ens-cachan.fr

References

[1]

L. Afanasiev, P. Blackburn, I. Dimitriou, B. Gaiffe, E. Goris, M. Marx, and M. de Rijke. PDL for ordered trees. J. Appl. Non-Classical Log., 15(2):115–135, 2005.

[2]

M. Benedikt, W. Fan, and F. Geerts. XPath satisfiability in the presence of DTDs. J. ACM, 55(2:8), 2008.

[3]

P. Blackburn, C. Gardent, and W. Meyer-Viol. Talking about trees. In EACL ’93, pages 21–29. ACL Press, 1993.

[4]

A. Bouajjani, P. Habermehl, L. Holík, T. Touili, and T. Vojnar. Antichain-based universality and inclusion testing over nondeterministic finite tree automata. In CIAA 2008, volume 5148 of LNCS, pages 57–67. Springer, 2008.

[5]

D. Calvanese, G. De Giacomo, M. Lenzerini, and M. Vardi. An automata-theoretic approach to Regular XPath. In DBPL 2009, volume 5708 of LNCS, pages 18–35. Springer, 2009.

[6]

B. T. Cate and L. Segoufin. Transitive closure logic, nested tree walking automata, and XPath. J. ACM, 57(3):18:1–18:41, 2010.

[7]

M. J. Fischer and R. E. Ladner. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci., 18(2):194–211, 1979.

[8]

N. Francis, C. David, and L. Libkin. A direct translation from XPath to nondeterministic automata. In AMW 2011, volume 749 of CEUR Workshop Proceedings. CEUR-WS.org, 2011.

[9]

Y. Ishihara, T. Morimoto, S. Shimizu, K. Hashimoto, and T. Fujiwara. A tractable subclass of DTDs for XPath satisfiability with sibling axes. In DBPL 2009, volume 5708 of LNCS, pages 68–83. Springer, 2009.

[10]

M. Kracht. Syntactic codes and grammar refinement. J. Logic Lang. Inform., 4(1):41–60, 1995.

[11]

M. Lange. Model checking propositional dynamic logic with all extras. J. Appl. Logic, 4(1):39–49, 2006.

[12]

M. Marx. Conditional XPath. ACM Trans. Database Syst., 30(4):929–959, 2005.

[13]

M. Y. Vardi. Reasoning about the past with two-way automata. In ICALP ’98, volume 1443 of LNCS, pages 628–641. Springer, 1998.

This document was translated from L^AT_EX by H^EV^EA.