Inductive First-Order Formula Synthesis by ASP: A Case Study in Invariant Inference

TL;DR

This paper introduces a novel ASP-based framework for synthesising first-order logic formulas from examples, significantly improving the efficiency of invariant inference in distributed systems.

Contribution

It proposes orthogonal slices, a new technique for formula enumeration, enabling incremental pruning and faster invariant synthesis in distributed systems.

Findings

Accelerates state-of-the-art invariant inference algorithms

Enables composition of different invariant inference frameworks

Demonstrates significant speedups in distributed system invariant inference

Abstract

We present a framework for synthesising formulas in first-order logic (FOL) from examples, which unifies and advances state-of-the-art approaches for inference of transition system invariants. To do so, we study and categorise the existing methodologies, encoding techniques in their formula synthesis via answer set programming (ASP). Based on the derived categorisation, we propose orthogonal slices, a new technique for formula enumeration that partitions the search space into manageable chunks, enabling two approaches for incremental candidate pruning. Using a combination of existing techniques for first-order (FO) invariant synthesis and the orthogonal slices implemented in our framework FORCE, we significantly accelerate a state-of-the-art algorithm for distributed system invariant inference. We also show that our approach facilitates composition of different invariant inference frameworks, allowing for novel optimisations.