Alternation-free modal mu-calculus for data trees

d abstract) Marcin Jurdzi´nski and Ranko Lazi´c∗ Department of Computer Science, University of Warwick, UK An alternation-free modal µ-calculus over data trees is introduced and studied. A data tree is an unranked ordered tree whose every node is labelled by a letter from a finite alphabet and an element (“datum”) from an infinite set. For expressing data-sensitive properties, the calculus is equipped with freeze quantification. A freeze quantifier stores in a register the datum labelling the current tree node, which can then be accessed for equality comparisons deeper in the formula. The main results in the paper are that, for the fragment with forward modal operators and one register, satisfiability over finite data trees is decidable but not primitive recursive, and that for the subfragment consisting of safety formulae, satisfiability over countable data trees is decidable but not elementary. The proofs use alternating tree automata which have registers, and establ...

• Type: Conference
• Year: 2007
• Where: LICS
• Authors: Marcin Jurdzinski, Ranko Lazic
• Keywords: Computer Science, Data Trees, LICS 2007, Tree, Unranked Ordered Tree