First-order finite satisfiability vs tree automata in safety verification

TL;DR

This paper presents a novel approach to safety verification of term-rewriting systems by translating the problem into first-order logic and using finite model finding, offering efficiency and clear invariants.

Contribution

It introduces a method that reduces safety verification to finite model finding, providing a concise invariant and demonstrating relative completeness with tree automata techniques.

Findings

Finite model finding efficiently verifies safety properties.

Countermodels serve as system invariants.

Approach shows explanatory power and practical efficiency.

Abstract

In this paper we deal with verification of safety properties of term-rewriting systems. The verification problem is translated to a purely logical problem of finding a finite countermodel for a first-order formula, which further resolved by a generic finite model finding procedure. A finite countermodel produced during successful verification provides with a concise description of the system invariant sufficient to demonstrate a specific safety property. We show the relative completeness of this approach with respect to the tree automata completion technique. On a set of examples taken from the literature we demonstrate the efficiency of finite model finding approach as well as its explanatory power.