The Library
Alternation-free modal mu-calculus for data trees
Tools
Jurdzinski, Marcin and Lazic, Ranko (2007) Alternation-free modal mu-calculus for data trees. In: 22nd Annual IEEE Symposium on Logic in Computer Science , Wroclaw, Poland, 10-14 Jul 2007. Published in: 22nd Annual IEEE Symposium on Logic in Computer Science : proceedings : Wroc¿aw, Poland, 10-14 July, 2007 pp. 131-140. ISBN 9780769529080. ISSN 1043-6871.
Research output not available from this repository.
Request-a-Copy directly from author or use local Library Get it For Me service.
Abstract
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 (Paper) | ||||
---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||
Series Name: | PROCEEDINGS/SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE | ||||
Journal or Publication Title: | 22nd Annual IEEE Symposium on Logic in Computer Science : proceedings : Wroc¿aw, Poland, 10-14 July, 2007 | ||||
Publisher: | IEEE Computer Society | ||||
ISBN: | 9780769529080 | ||||
ISSN: | 1043-6871 | ||||
Official Date: | 2007 | ||||
Dates: |
|
||||
Number of Pages: | 10 | ||||
Page Range: | pp. 131-140 | ||||
Status: | Peer Reviewed | ||||
Publication Status: | Published | ||||
Description: | Extended abstract |
||||
Conference Paper Type: | Paper | ||||
Title of Event: | 22nd Annual IEEE Symposium on Logic in Computer Science | ||||
Type of Event: | Other | ||||
Location of Event: | Wroclaw, Poland | ||||
Date(s) of Event: | 10-14 Jul 2007 |
Data sourced from Thomson Reuters' Web of Knowledge
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |