Logics on data words

Abstract

We investigate logics on data words, i.e., words where each position is labelled by some propositions from a finite set and by some data values from an infinite domain. A basic motivation for the study of these logics, called data logics in this work, is that data words are a suitable model to represent traces of concurrent systems with unboundedly many interacting processes. In such representations data values stand for process IDs. Thus, data logics can be used to formulate requirements on such traces. We first study the expressivity and complexity of the satisfiability problem for these logics. Then, we investigate suitable models for concurrent systems with unboundedly many processes. Finally, we analyse the model checking problem for such systems in the case that data logics are used to specify system requirements. One of our main results is that, despite the bad properties of data logics with respect to satisfiability, there are important cases in which model checking with data logics has moderate complexity. Hence, our results motivate for further investigations with the aim to find interesting models and data logics which can be used in practical model checking tools.