Regular Abstractions for Array Systems

TL;DR

This work tackles the challenge of verifying safety and liveness for array systems, whose unbounded element domains and quantified properties defy traditional finite-state methods. It introduces a novel predicate abstraction based on indexed predicates that overapproximates array formulae as words over a finite alphabet and then further abstracts to regular languages, enabling the application of regular model checking to both safety and liveness problems. The authors formulate a FO-LTL-like specification framework, establish a sound Galois connection between concrete and abstract domains, and provide concrete procedures for computing regular abstractions, including constraint-based and template-driven approaches. Through case studies on Dijkstra's self-stabilizing protocol, Chang-Roberts, and sorting algorithms, the approach demonstrates automatic, scalable proofs of complex properties, highlighting both the potential and the current limitations (e.g., alphabet size and predicate generation). Overall, the method offers a principled pathway to leverage regular model checking for parameterized array systems, with practical implications for verifying distributed protocols and array-based programs.

Abstract

Verifying safety and liveness over array systems is a highly challenging problem. Array systems naturally capture parameterized systems such as distributed protocols with an unbounded number of processes. Such distributed protocols often exploit process IDs during their computation, resulting in array systems whose element values range over an infinite domain. In this paper, we develop a novel framework for proving safety and liveness over array systems. The crux of the framework is to overapproximate an array system as a string rewriting system (i.e. over a finite alphabet) by means of a new predicate abstraction that exploits the so-called indexed predicates. This allows us to tap into powerful verification methods for string rewriting systems that have been heavily developed in the last few decades (e.g. regular model checking). We demonstrate how our method yields simple, automatically verifiable proofs of safety and liveness properties for challenging examples, including Dijkstra's self-stabilizing protocol and the Chang-Roberts leader election protocol.

Figures (1)

• Figure 1: Example constraint templates for updating and copying array contents, where $\bowtie\; \in \{=, \neq, <, \le, >, \ge\}$. Each template consists of multiple premises and a consequence. The leftmost premise corresponds to an update (i.e. the assignment part of a guarded command), and the rest of the premises come from the guard. The consequence copies a predicate value from the current state to the next state. These templates exploit a simplifying assumption that one guarded command updates precisely one index variable or array element.

Theorems & Definitions (21)

• proposition 1
• definition 1: Indexed predicate
• lemma 1
• lemma 2
• proposition 2
• definition 2: Regular abstraction for state formulae
• definition 3: Regular abstraction for transition formulae
• theorem 1
• proposition 3
• lemma 3