A Myhill-Nerode theorem for register automata and symbolic trace languages (Q5918650)

The contribution proposes a new Myhill-Nerode theorem for register automata based on symbolic trace languages. A register automaton is a finite-state automaton that is additionally equipped with several (finitely many) registers each of which carries a data value. Instead of a single input symbol, the automaton additionally receives a data value and the transitions can compare data values with the help of guards and re-assign the values stored in the registers, constants, as well as the data value that is provided together with the input symbol. These register automata are required to be deterministic in the sense that in each situation at most one transition can be applied, so the conjuction of the guards of two different transitions for a given input symbol must be unsatisfiable. As usual, the register automaton accepts a sequence of input symbol and data value pairs if the automaton can process this sequence of pairs starting in the initial state and stopping in a final state. These sequences of pairs are also called data words. The authors propose a new semantics that makes several internals of the automata more explicit. In particular, the guards applied by a transition are now explicitly represented in the input, so each input symbol is now joined by a data value as well as a guard and a transition can only process this triple if additionally its guard matches exactly the guard present in the input. For such inputs (of triples), which are called symbolic traces, the authors derive a Myhill-Nerode characterization for the symbolic-trace languages accepted by register automata. Their characterization relies on three (device-independent) equivalence relations defined on the symbolic-trace language, only that if they all have finite index and satisfy additional properties ensures that the language can be accepted by some register automaton, which can also effectively be constructed from the equivalence relations. The converse is also true: If a register automaton accepts a symbolic-trace language, then those equivalences have finite index and fulfill the additional properties. The paper is well written and properly motivates its adjustment of the standard semantics, which arguably makes the problem simpler. It is argued that in certain scenarios the traditional automaton-internal guards can be extracted, made visible in the input, and thus assist the learning process for which the Myhill-Nerode characterizations are traditionally the basis. Examples and illustrations are generously provided and the full text can be appreciated by any graduate, but some exposure to register automata will prove very beneficial.