Feasible automata for two-variable logic with successor on data words

DOI10.1007/978-3-642-28332-1_30zbMATH Open1351.03026arXiv1110.1221OpenAlexW1878133323MaRDI QIDQ2890205FDOQ2890205

Authors: Ahmet Kara, Thomas Schwentick, Tony Tan 

Publication date: 8 June 2012

Published in: Language and Automata Theory and Applications (Search for Journal in Brave)

Abstract: We introduce an automata model for data words, that is words that carry at each position a symbol from a finite alphabet and a value from an unbounded data domain. The model is (semantically) a restriction of data automata, introduced by Bojanczyk, et. al. in 2006, therefore it is called weak data automata. It is strictly less expressive than data automata and the expressive power is incomparable with register automata. The expressive power of weak data automata corresponds exactly to existential monadic second order logic with successor +1 and data value equality sim, EMSO2(+1,sim). It follows from previous work, David, et. al. in 2010, that the nonemptiness problem for weak data automata can be decided in 2-NEXPTIME. Furthermore, we study weak B"uchi automata on data omega-strings. They can be characterized by the extension of EMSO2(+1,sim) with existential quantifiers for infinite sets. Finally, the same complexity bound for its nonemptiness problem is established by a nondeterministic polynomial time reduction to the nonemptiness problem of weak data automata.

Full work available at URL: https://arxiv.org/abs/1110.1221

Recommendations

• Two-variable logic on data words
• scientific article; zbMATH DE number 6109856
• Two-variable logic on 2-dimensional structures
• Automata vs. Logics on Data Words
• On the satisfiability of two-variable logic over data words

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05)

Cited In (11)

• Walking on data words
• Weak and nested class memory automata
• Generalized data automata and fixpoint logic
• An automaton over data words that captures EMSO logic
• Automata based verification over linearly ordered data domains
• On temporal logics with data variable quantifications: decidability and complexity
• Extending two-variable logic on data trees with order on data values and its automata
• Pebble-intervals automata and \(\text{FO}^2\) with two orders
• Walking on data words
• Two-variable logic on data words
• A class of automata for the verification of infinite, resource-allocating behaviours

This page was built for publication: Feasible automata for two-variable logic with successor on data words

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2890205)