Automata vs. Logics on Data Words

Abstract. The relationship between automata and logics has been investigated since the 1960s. In particular, it was shown how to determine, given an automaton, whether or not it is definable in first-order logic with label tests and the order relation, and for first-order logic with the successor relation. In recent years, there has been much interest in languages over an infinite alphabet. Kaminski and Francez introduced a class of automata called finite memory automata (FMA), that represent a natural analog of finite state machines. A FMA can use, in addition to its control state, a (bounded) number of registers to store and compare values from the input word. The class of data languages recognized by FMA is incomparable with the class of data languages defined by firstorder formulas with the order relation and an additional binary relation for data equality. We first compare the expressive power of several variants of FMA with several data word logics. Then we consider the correspon...

• Type: Conference
• Year: 2010
• Where: CSL
• Authors: Michael Benedikt, Clemens Ley, Gabriele Puppis
• Keywords: Automated Reasoning, CSL 2010, First-order Logic, Logic, Order Relation