Semiring Provenance for First-Order Model Checking

TL;DR

This paper introduces a novel semiring-based approach to data provenance in first-order model checking, effectively handling negation and enabling reverse provenance analysis for models with provenance tracking.

Contribution

It extends provenance methods to include negation by developing a new semiring of polynomials with dual indeterminates, allowing for more comprehensive provenance analysis.

Findings

Introduced a semiring of polynomials with dual indeterminates for negation handling.

Enabled reverse provenance analysis in first-order model checking.

Extended provenance abstractions beyond negation-free fragments.

Abstract

Given a first-order sentence, a model-checking computation tests whether the sentence holds true in a given finite structure. Data provenance extracts from this computation an abstraction of the manner in which its result depends on the data items that describe the model. Previous work on provenance was, to a large extent, restricted to the negation-free fragment of first-order logic and showed how provenance abstractions can be usefully described as elements of commutative semirings --- most generally as multivariate polynomials with positive integer coefficients. In this paper we introduce a novel approach to dealing with negation and a corresponding commutative semiring of polynomials with dual indeterminates. These polynomials are used to perform reverse provenance analysis, i.e., finding models that satisfy various properties under given provenance tracking assumptions.