Semiring Provenance for Fixed-Point Logic

DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)

Abstract

Semiring provenance is a successful approach, originating in database theory, to providing detailed information on how atomic facts combine to yield the result of a query. In particular, general provenance semirings of polynomials or formal power series provide precise descriptions of the evaluation strategies or "proof trees" for the query. By evaluating these descriptions in specific application semirings, one can extract practical information for instance about the confidence of a query or the cost of its evaluation. This paper develops semiring provenance for very general logical languages featuring the full interaction between negation and fixed-point inductions or, equivalently, arbitrary interleavings of least and greatest fixed points. This also opens the door to provenance analysis applications for modal μ-calculus and temporal logics, as well as for finite and infinite model-checking games. Interestingly, the common approach based on Kleene’s Fixed-Point Theorem for ω-continuous semirings is not sufficient for these general languages. We show that an adequate framework for the provenance analysis of full fixed-point logics is provided by semirings that are (1) fully continuous, and (2) absorptive. Full continuity guarantees that provenance values of least and greatest fixed-points are well-defined. Absorptive semirings provide a symmetry between least and greatest fixed-points and make sure that provenance values of greatest fixed points are informative. We identify semirings of generalized absorptive polynomials S^{∞}[X] and prove universal properties that make them the most general appropriate semirings for our framework. These semirings have the further property of being (3) chain-positive, which is responsible for having truth-preserving interpretations that give non-zero values to all true formulae. We relate the provenance analysis of fixed-point formulae with provenance values of plays and strategies in the associated model-checking games. Specifically, we prove that the provenance value of a fixed point formula gives precise information on the evaluation strategies in these games.

Authors 4

1. Katrin M. Dannert Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Germany

   RWTH Aachen University, Aachen, Germany

2. Erich Grädel Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Germany

   RWTH Aachen University, Aachen, Germany

3. Matthias Naaf Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Germany

   RWTH Aachen University, Aachen, Germany

4. Val Tannen

   University of Pennsylvania

   Affiliation as printed

   University of Pennsylvania, Philadelphia, PA, USA

   University of Pennsylvania, Philadelphia, United States