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.

翻译：验证数组系统的安全性与活跃性是一个极具挑战性的问题。数组系统自然地描述了参数化系统，例如具有无界进程数量的分布式协议。这类分布式协议在计算过程中常利用进程标识符，导致数组系统的元素取值范围为无穷域。本文提出了一种新颖的框架，用于证明数组系统的安全性与活跃性。该框架的核心是通过一种新的谓词抽象（利用所谓的索引谓词），将数组系统过度近似为字符串重写系统（即基于有限字母表）。这使得我们能够利用过去几十年中高度发展的字符串重写系统强验证方法（例如正则模型检测）。我们通过包括迪杰斯特拉自稳定协议和张-罗伯茨领导者选举协议在内的具有挑战性实例，展示了该方法如何生成简单、可自动验证的安全性与活跃性属性证明。