NESTED SIBLING TREE AUTOMATA

In the X ML standard, d ata are represented as unran kedlab e led ord ered trees. R egu lar u n r an ke d t ree au t omata p rov id e a u se-fu l form alism for t h e valid at ion of s ch em as en forcin g r egu lar st ru ct u r alcon st r aint s on X ML d o cu m e nt s. H owe ve r som e c on cret e ap p licat ioncont ex t s n eed t h e e x p ression of m ore gen e ral c on st raint s t h an t h e r eg-u lar on es. I n t h is p ap er we p r op ose a n e w fram e work in wh ich c ont e x t -free sty le st r u c t u ral c on st raint s can b e e x p ressed an d valid at ed . Th isfram ework is ch aract erized by : ( i) t h e int ro d u c t ion of a n ew n ot ion oftrees, t h e so- c alled typedunrankedlabeledtrees ( tul a b trees for s h o r t ) i nwh ich e ach n o d e r eceive s on e of th ree p ossib le ty p es (up, down or fix),an d ( ii) t h e d efi n it ion of a n ew n ot ion of t r ee au t om at a, t h e so- c allednested si bl i n g tul ab tree autom a ta, able to enforce contex t-free stylestru ctu r al con straint s on tul a b tree languages. During their structuralcontrol p ro cess, su ch au tomata are u sing visibly pushdown languagesof words [R. Alur and P. Madhusudan, Visibly pushdown languages,36t h ACM sy m p osiu m on Th e ory of Com p u t in g, Ch icago, U S A ( 2004)202–211] on t h eir alp h ab e t of s t at e s. We sh ow t h at t h e r esu l t i n g classNSTL of tul a b tree lan gu ages r ecogn ized by n e sted sib lin g tul a b treeau tomata is robust, i.e . closed under Bo olean op erations and with deci-sion pro cedures for the classical memb ership, emptin ess and in clusionp r ob lem s. We t h e n give t h r ee ch aract e rizat ion s of NSTL: a logicalch aract e rizat ion by d e fi n in g an ad eq u at e logic in wh ich NSTL happ ensto coin cide with the mo d els of mon ad ic second order sentences; thetwo ot h er ch aract e rizat ion s are u sin g ad e q u at e e n c o d in gs an d m ap t o-get h er lan gu ages of NSTL with some regu lar sets of 3-ary trees or withparticular sets of binary trees