Alternation-free modal mu-calculus for data trees (Extended abstract)
Jurdzinski, Marcin and Lazic, Ranko (2007) Alternation-free modal mu-calculus for data trees (Extended abstract). In: 22nd Annual IEEE Symposium on Logic in Computer Science, Wroclaw, POLAND, JUL 10-14, 2007. Published in: 22nd Annual IEEE Symposium on Logic in Computer Science, Proceedings pp. 131-140.Full text not available from this repository.
An alternation-firee modal mu-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 fieeze 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 establish correspon-, dences with nondeterministic tree, automata which have faulty counters. Allowing backward modal operators or two registers causes undecidability.
As consequences, decidability is obtained for two datasensitive fragments of the XPath query language.
The paper shows that, for reasoning about data trees, the forward fragment of the calculus with one register is a powerful alternative to a recently proposed first-order logic with two, variables.
|Item Type:||Conference Item (UNSPECIFIED)|
|Subjects:||Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software|
|Series Name:||PROCEEDINGS/SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE|
|Journal or Publication Title:||22nd Annual IEEE Symposium on Logic in Computer Science, Proceedings|
|Publisher:||IEEE COMPUTER SOC|
|Number of Pages:||10|
|Page Range:||pp. 131-140|
|Title of Event:||22nd Annual IEEE Symposium on Logic in Computer Science|
|Location of Event:||Wroclaw, POLAND|
|Date(s) of Event:||JUL 10-14, 2007|
Actions (login required)