Abduction of trap invariants in parameterized systems

TL;DR

This paper extends a parameterized system verification method to handle variables with ranges dependent on the number of processes, using first-order logic to maintain decidability and enabling practical invariant generation.

Contribution

It introduces a novel reduction to first-order satisfiability for verifying invariants in systems with process-dependent variables, overcoming previous limitations.

Findings

First-order theorem provers can verify non-trivial examples.

The approach produces small, understandable invariant sets.

The method remains effective despite increased variable complexity.

Abstract

In a previous paper we have presented a CEGAR approach for the verification of parameterized systems with an arbitrary number of processes organized in an array or a ring. The technique is based on the iterative computation of parameterized invariants, i.e., infinite families of invariants for the infinitely many instances of the system. Safety properties are proved by checking that every global configuration of the system satisfying all parameterized invariants also satisfies the property; we have shown that this check can be reduced to the satisfiability problem for Monadic Second Order on words, which is decidable. A strong limitation of the approach is that processes can only have a fixed number of variables with a fixed finite range. In particular, they cannot use variables with range [0,N-1], where N is the number of processes, which appear in many standard distributed algorithms. In this paper, we extend our technique to this case. While conducting the check whether a safety property is inductive assuming a computed set of invariants becomes undecidable, we show how to reduce it to checking satisfiability of a first-order formula. We report on experiments showing that automatic first-order theorem provers can still perform this check for a collection of non-trivial examples. Additionally, we can give small sets of readable invariants for these checks.