id: 06109856
dt: a
an: 06109856
au: Wu, Zhilin
ti: Commutative data automata.
so: Cégielski, Patrick (ed.) et al., Computer science logic (CSL’12). 26th
    international workshop, 21th annual conference of the EACSL, September
    3‒6, 2012, Fontainebleau, France. Selected papers based on the
    presentations at the conference. Wadern: Schloss Dagstuhl ‒ Leibniz
    Zentrum für Informatik (ISBN 978-3-939897-42-2). LIPICS ‒ Leibniz
    International Proceedings in Informatics 16, 528-542, electronic only
    (2012).
py: 2012
pu: Wadern: Schloss Dagstuhl ‒ Leibniz Zentrum für Informatik
la: EN
cc: 
ut: data automata; commutative regular languages; Presburger arithmetic;
    existential monadic second-order logic; Büchi automata
ci: 
li: doi:10.4230/LIPIcs.CSL.2012.528
ab: Summary: Formalisms over infinite alphabets have recently received much
    focus in the community of theoretical computer science. Data automaton
    is a formal model for words over an infinite alphabet, that is, the
    product of a finite set of labels and an infinite set of data values,
    proposed by Bojanczyk, Muscholl, Schwentick et al. in 2006. A data
    automaton consists of two parts, a nondeterministic letter-to-letter
    transducer, and a class condition specified by a finite automaton,
    which acts as a condition on each subword of the outputs of the
    transducer in corresponding to a maximal set of positions with the same
    data value. It is open whether the nonemptiness of data automata can be
    decided with elementary complexity, since this problem is equivalent to
    the reachability of Petri nets. Very recently, a restriction of data
    automata with elementary complexity, called weak data automata, was
    proposed by Kara, Schwentick and Tan and its nonemptiness problem was
    shown to be in 2-NEXPTIME. In weak data automata, the class conditions
    are specified by some simple constraints on the number of occurrences
    of labels occurring in every class. The aim of this paper is to
    demonstrate that the commutativity of class conditions is the genuine
    reason accounting for the elementary complexity of weak data automata.
    For this purpose, we define and investigate commutative data automata,
    which are data automata with class conditions restricted to commutative
    regular languages. We show that while the expressive power of
    commutative data automata is strictly stronger than that of weak data
    automata, the nonemptiness problem of this model can still be decided
    with elementary complexity, more precisely, in 3-NEXPTIME. In addition,
    we extend the results to data $ω$-words and prove that the
    nonemptiness of commutative Büchi data automata can be decided in
    4-NEXPTIME. We also provide logical characterizations for commutative
    (Büchi) data automata, similar to those for weak (Büchi) data
    automata.
rv: