An Automata-Theoretic Approach to Model-Checking Systems and Specifications Over Infinite Data Domains

Data-parameterized systems model systems with finite control over an infinite data domain. VLTL is an extension of LTL that uses variables in order to specify properties of computations over infinite data, and as such, VLTL is suitable for specifying properties of data-parameterized systems. We present alternating variable Büchi word automata (AVBWs), a new model of automata over infinite alphabets, capable of modeling a significant fragment of VLTL. While alternating and non-deterministic Büchi automata over finite alphabets have the same expressive power, we show that this is not the case for infinite data domains, as we prove that AVBWs are strictly stronger than the previously defined non-deterministic variable Büchi word automata (NVBWs). However, while the emptiness problem is easy for NVBWs, it is undecidable for AVBWs. We present an algorithm for translating AVBWs to NVBWs in cases where such a translation is possible. Additionally, we characterize the structure of AVBWs that can be translated to NVBWs with our algorithm. We then rely on the natural iterative behavior of our translation algorithm to describe a bounded model-checking procedure for the logic that we consider. Furthermore, we present several fragments of the logic that can be expressed by NVBWs, as well as a fragment that cannot be expressed by NVBWs, yet whose satisfiability is decidable.