Proving Cutoff Bounds for Safety Properties in First-Order Logic

TL;DR

This work addresses verifying safety properties of parameterized systems modeled in first-order logic (FO) by introducing a finite-domain semantics that restricts attention to finite structures. It adapts the cutoff method to FO via size-reducing simulations, enabling a reduction from unbounded domains to bounded-domain instances. A concrete FO encoding is developed to represent and validate these simulations using SMT solving, and the authors implement a tool that demonstrates the approach on diverse distributed protocols, including cases not provable by FO inductive invariants. The results indicate that finite-domain cutoffs can be effectively discovered and validated, broadening the applicability of FO verification to finite, yet unbounded, systems with practical implications for automated safety verification.

Abstract

First-order logic has been established as an important tool for modeling and verifying intricate systems such as distributed protocols and concurrent systems. These systems are parametric in the number of nodes in the network or the number of threads, which is finite in any system instance, but unbounded. One disadvantage of first-order logic is that it cannot distinguish between finite and infinite structures, leading to spurious counterexamples. To mitigate this, we offer a verification approach that captures only finite system instances. Our approach is an adaptation of the cutoff method to systems modeled in first-order logic. The idea is to show that any safety violation in a system instance of size larger than some bound can be simulated by a safety violation in a system of a smaller size. The simulation provides an inductive argument for correctness in finite instances, reducing the problem to showing safety of instances with bounded size. To this end, we develop a framework to (i) encode such simulation relations in first-order logic and to (ii) validate the simulation relation by a set of verification conditions given to an SMT solver. We apply our approach to verify safety of a set of examples, some of which cannot be proven by a first-order inductive invariant.

Figures (6)

• Figure 1: First-order specification of the TreeTermination protocol.
• Figure 2: A counterexample to safety of TreeTermination over infinite structures, depicted as a trace of two states related by the transition relation: the first is an initial state, and the second violates safety. The order of nodes is depicted by $\leq$ and terminated nodes are depicted by shading.
• Figure 3: Strengthening of simulation to strong simulation: solid nodes are universally quantified while the dashed node is existentially quantified; solid edges represent assumptions and dashed edges represent conclusions. $R^=$ is a shorthand for $R \cup \mathrm{id}_S$.
• Figure 4: Left: a structure $s=(\mathcal{D}, \mathcal{I}^h \uplus \mathcal{I}^\ell)$ and an assignment $[z \mapsto d_0]$ that satisfy $\eta(z)$. The $h$ and $\ell$ copies of $\mathsf{root}$, $\mathsf{leq}$ and $\mathsf{termd}$ are interpreted in the same way, so these interpretations are depicted jointly. $\mathsf{leq}(\cdot,\cdot)$ is depicted by solid lines and $\mathsf{termd}(\cdot)$ is depicted by shading. The interpretation of the two copies of $\mathsf{ack}(\cdot,\cdot)$ are depicted by dashed and dotted arrows. Right: the derived high and low structures: $s^h=(\mathcal{D},\mathcal{I}^h)$ and $s^\ell=(\mathcal{D}_{\times}, \mathcal{I}_{\times}^\ell)$, with the relations and constants depicted in the same way.
• Figure 5: Verification conditions establishing strong size-reducing simulation for a high-low update $\eta(z)$ with precondition $\theta(z)$, $\mathcal{T}=(\Sigma,\Gamma,\iota,\tau)$, $\varphi$ and $k$.

Theorems & Definitions (31)

• definition 1
• definition 2
• theorem 1
• definition 3
• lemma 1
• definition 4
• lemma 2
• definition 5
• lemma 3
• lemma 4