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.

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 (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
ISBN:	978-0-7695-2908-0
ISSN:	1043-6871
Date:	2007
Number of Pages:	10
Page Range:	pp. 131-140
Publication Status:	Published
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
URI:	http://wrap.warwick.ac.uk/id/eprint/31012

Data sourced from Thomson Reuters' Web of Knowledge

Request changes to a record

Actions (login required)

View Item