Abstract

Provenance analysis aims at understanding how the result of a computational process with a complex input, consisting of multiple items, depends on the various parts of this input. Here we investigate this for the model checking problem of guarded logics on finite relational structures. Semiring provenance was originally developed for positive database query languages, to understand which combinations of the atomic facts in a database can be used for computing the result of a given query. Based on interpretations of the atomic facts not just by true or false, but by values in an appropriate semiring, one can then answer questions such as the minimal cost of a query evaluation, the confidence one can have that the result is true, or the clearance level that is required for obtaining the output. Semiring provenance was recently extended by Grädel and Tannen to logics with negation, notably first-order logic, dealing with negation by transformation into negation normal form and by semirings of polynomials with a duality on the indeterminates. Here we develop this approach further for the guarded fragment, introduced by Andréka, van Benthem and Németi, based on an analysis of the associated model checking games. Guarded quantification permits to control the complexity of the semiring computations since once has to take sums or products only over those tuples of elements that appear in the guards. Finally, we extend our provenance analysis to the more powerful guarded negation fragment of first-order logics.