Campus Event Calendar
Event Entry
New for: D2, D3
What and Who
Emptiness decision for tree automata with global equality and disequality constraints
Florent Jacquemard
INRIA, Cachan
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 8 February 2011
14:15
45 Minutes
E1 4
019
Saarbrücken
Abstract
We present a class of ranked tree automata with global constraints (TABG).
They able to test for equality and disequality modulo a given flat
equational theory locally, between brother subterms
and globally, between subterms whose positions are defined by the
states reached during a computation.
In particular, TABG can check that all the subterms reaching a given
state are distinct.
This constraint is related to monadic key constraints for XML documents,
meaning that every two distinct positions of a given type have different values.
We prove decidability of the emptiness problem for TABG.
This solves, in particular, the open question of the decidability of
emptiness for a subclass called TAGED.
We further extend our result by allowing global arithmetic constraints
for counting the number of occurrences of some state or the number of
different equivalence classes of subterms (modulo a given flat
equational theory)
reaching some state during a computation.
We also extend the model to unranked ordered terms.
As a consequence of our results for TABG, we prove the decidability
of a fragment of the monadic second order logic on trees extended with
predicates for equality and disequality between subtrees, and cardinality.
They able to test for equality and disequality modulo a given flat
equational theory locally, between brother subterms
and globally, between subterms whose positions are defined by the
states reached during a computation.
In particular, TABG can check that all the subterms reaching a given
state are distinct.
This constraint is related to monadic key constraints for XML documents,
meaning that every two distinct positions of a given type have different values.
We prove decidability of the emptiness problem for TABG.
This solves, in particular, the open question of the decidability of
emptiness for a subclass called TAGED.
We further extend our result by allowing global arithmetic constraints
for counting the number of occurrences of some state or the number of
different equivalence classes of subterms (modulo a given flat
equational theory)
reaching some state during a computation.
We also extend the model to unranked ordered terms.
As a consequence of our results for TABG, we prove the decidability
of a fragment of the monadic second order logic on trees extended with
predicates for equality and disequality between subtrees, and cardinality.
Contact
Jennifer Müller
900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 02/02/2011 12:16 -- Created document.