Data Words: Logic, Automata, and Model Checking

Benedikt Bollig
LSV, ENS Cachan
Friday, 16 December, 2011 - 14:00
Room: NO5 Solvay

We consider data words, i.e, strings where each position carries both a label from a finite alphabet and some values from an infinite domain. The latter can be used to represent an unbounded number of process identifiers so that data words are suitable to model the behavior of a concurrent program with dynamic process creation. A variety of formalisms, including logic and automata, have been studied to specify sets of data words in the context of verification. We survey some well established notions and describe two recent contributions to the area.

First, we develop a general framework for the specification and implementation of sets of data words. On the specification side, we consider monadic second-order (MSO) logic, which comes with a predicate to test two word positions for data equality. As a model of an implementation, we introduce class register automata. Our model combines the well known models of register automata and class memory automata, and it captures dynamic communicating automata, whose semantics can be described as a set of message sequence charts. We study the realizability problem and show that every formula from an existential fragment of MSO logic can be effectively translated into a class register automaton.

Second, we consider the model-checking problem with respect to MSO properties. As model checking is undecidable for nearly all known automata models (including the model presented in the first part of the talk), we introduce data grammars. Data grammars come with multiple rewrite tapes and are enriched with parameters that can be instantiated with data values. We present an example grammar describing a leader election protocol with an unknown number of processes. While satisfiability for MSO logic is undecidable (even for weaker fragments such as first-order logic), we show that one can decide if all words generated by a data grammar satisfy a given formula from the full MSO logic. The model checking part of this talk reports on joint work with Aiswarya Cyriac, Paul Gastin, and K. Narayan Kumar.