Finding models through graph saturation

TL;DR

This paper introduces a semi-decision procedure called graph saturation for automatically verifying certain graph invariants expressed with relation operations, proving its correctness and establishing the undecidability of the related decision problem.

Contribution

It presents a novel semi-decision procedure for invariant verification over graphs and proves the problem's undecidability, confirming a prior conjecture.

Findings

The graph saturation procedure is correct for invariant entailment.

The decision problem for these invariants is undecidable.

The method is inspired by graph rewriting techniques.

Abstract

We give a procedure that can be used to automatically satisfy invariants of a certain shape. These invariants may be written with the operations intersection, composition and converse over binary relations, and equality over these operations. We call these invariants \tr{}s that we interpret over graphs. For questions stated through sets of these sentences, this paper gives a semi-decision procedure we call graph saturation. It decides entailment over these \tr{}s, inspired on graph rewriting. We prove correctness of the procedure. Moreover, we show the corresponding decision problem to be undecidable. This confirms a conjecture previously stated by the author.