Provenance Analysis for Logic and Games

• Applicant: Professor Dr. Erich Grädel
• Subject Area: Theoretical Computer Science
• Term: since 2020
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 434376062

Provenance analysis and semiring semantics are based on the idea to evaluate logical statements not just by true or false, but by values in some commutative semiring. In this context, the classical semantics re-appears as the special case, when the Boolean semiring is used. Other semirings provide additional information, for instance for cost computations, for the counting of evaluation strategies and proofs, for access levels and security issues, and so on. Further, provenance semirings of polynomials or formal power theories, with universal properties in an algebraic sense, are used to find most general provenance valuations. In particular, they admit the tracking of atomic facts, and give precise insights which combinations of atomic facts yield the truth of a logical statement, and how often these are used in a successful evaluation. For positive database query languages, semiring provenance has been successfully applied for more than 15 years. The objective of this research project is the systematic extension of provenance analysis and semiring semantics to a broad spectrum of logical formalisms which are relevant in various areas of computer science, and as well to classes of finite and infinite games. This also opens the door to new applications of provenance analysis. Important starting points of this project have been our new approach for the treatment of negation in polynomial semirings with dual indeterminate, and the connections of provenance analysis to the theory of finite and infinite games. Tn the first phase of this project, significant progress towards these objectives has been made. Algebraic, logical, and game-theoretic foundations of semiring semantics are now much better understood. Suitable semirings for fixed-point computations have been identified, and an adequate semiring semantics for general fixed-point logics with negation and interleaving of least and greatest fixed points has been found, including algorithmic evaluation strategies and associated model-checking games. Important model-theoretic questions of semiring semantics could be answered. Provenance analysis has also been established as a new method for the strategy analysis in games. Sum-of-Strategies-Theorems have been proved for a number of different game models, and the significance and value of this method has been illustrated by a detailed case analysis for Büchi games. In the second phase of this project, we want to extend and deepen our results in several directions, and close remaining gaps in the theory. This includes logical, algorithmic, and game-theoretic aspects, as well as applications, for instance for repairs of missing or inaccurate data, and logical learning theory. Our goal is to make provenance analysis and semiring semantics a mature field of logic in computer science.

• DFG Programme: Research Grants