Campus Event Calendar
Event Entry
What and Who
On the Count of Trees
Everardo Barcenas
INRIA, University of Grenoble
Talk
RG1
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 25 November 2010
14:00
60 Minutes
E1 7
2.01
Saarbrücken
Abstract
Regular tree grammars and regular path expressions constitute core
constructs widely used in programming languages and type systems.
Nevertheless, there has been little research so far on frameworks for
reasoning about path expressions where node cardinality constraints
occur along a path in a tree. We present a logic capable of expressing
deep counting along paths which may include arbitrary recursive
forward and backward navigation. The counting extensions can be seen
as a generalization of graded modalities that count immediate
successor nodes. While the combination of graded modalities, nominals,
and inverse modalities yields undecidable logics over graphs, we show
that these features can be combined in a decidable tree logic whose
main features can be decided in exponential time. Our logic being
closed under negation, it may be used to decide typical problems on
XPath queries such as satisfiability, type checking with relation to
regular types, containment, or equivalence.
constructs widely used in programming languages and type systems.
Nevertheless, there has been little research so far on frameworks for
reasoning about path expressions where node cardinality constraints
occur along a path in a tree. We present a logic capable of expressing
deep counting along paths which may include arbitrary recursive
forward and backward navigation. The counting extensions can be seen
as a generalization of graded modalities that count immediate
successor nodes. While the combination of graded modalities, nominals,
and inverse modalities yields undecidable logics over graphs, we show
that these features can be combined in a decidable tree logic whose
main features can be decided in exponential time. Our logic being
closed under negation, it may be used to decide typical problems on
XPath queries such as satisfiability, type checking with relation to
regular types, containment, or equivalence.
Contact
Jennifer Müller
900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 11/23/2010 08:49
Jennifer Müller, 11/23/2010 08:49 -- Created document.
Jennifer Müller, 11/23/2010 08:49 -- Created document.