Provenance Analysis for Logic and Games

TL;DR

This paper introduces a novel provenance analysis method for logics with negation, using dual-indeterminate semirings, enhancing understanding of logical computations and game strategies.

Contribution

It develops a new provenance framework for logics with negation, extending existing methods to include negative information and strategies in game analysis.

Findings

Proposes dual-indeterminate semirings for provenance analysis.

Provides detailed insights into strategies in logic games.

Extends provenance analysis to logics with negation.

Abstract

A model checking computation checks whether a given logical sentence is true in a given finite structure. Provenance analysis abstracts from such a computation mathematical information on how the result depends on the atomic data that describe the structure. In database theory, provenance analysis by interpretations in commutative semirings has been rather succesful for positive query languages (such a unions of conjunctive queries, positive relational algebra, or datalog). However, it did not really offer an adequate treatment of negation or missing information. Here we propose a new approach for the provenance analysis of logics with negation, such as first-order logic and fixed-point logics. It is closely related to a provenance analysis of the associated model-checking games, and based on new semirings of dual-indeterminate polynomials or dual-indeterminate formal power series. These are obtained by taking quotients of traditional provenance semirings by congruences that are generated by products of positive and negative provenance tokens. Beyond the use for model-checking problems in logics, provenance analysis of games is of independent interest. Provenance values in games provide detailed information about the number and properties of the strategies of the players, far beyond the question whether or not a player has a winning strategy from a given position.

Equations

$$f_{\sigma }(v):=\{\begin{array}{ll}{\sum }_{w\in vE}{h}_{\sigma }(vw)\cdot f_{\sigma }(w)& \text{ if }v\in V_{\sigma }\\ {\prod }_{w\in vE}{h}_{\sigma }(vw)\cdot f_{\sigma }(w)& \text{ if }v\in V_{1-\sigma }.\end{array}$$

$${\#}_{\mathcal{S}}(v):=|{\rho }_{\mathcal{S}}^{-1}(v)|\text{and}{\#}_{\mathcal{S}}(e):=|{\rho }_{\mathcal{S}}^{-1}(e)|$$

$$F(\mathcal{S}):=\prod _{e\in E}{h}_{\sigma }(e{)}^{{\#}_{\mathcal{S}}(e)}\cdot \prod _{v\in T}{f}_{\sigma }(v{)}^{{\#}_{\mathcal{S}}(v)}.$$

$$f_{\sigma }(v)=\sum _{\mathcal{S}\in {\mathrm{Strat}}_{\sigma }(v)}F(\mathcal{S}).$$

$$f_{\sigma }(v)=\sum _{w\in vE}{h}_{\sigma }(vw)\cdot f_{\sigma }(w)=\sum _{w\in vE}\sum _{{\mathcal{S}}^{\prime }\in {\mathrm{Strat}}_{\sigma }(w)}{h}_{\sigma }(vw)\cdot F({\mathcal{S}}^{\prime })=\sum _{\mathcal{S}\in {\mathrm{Strat}}_{\sigma }(v)}F(\mathcal{S}).$$

$$f_{\sigma }(v)$$

$$=\sum _{v\cdot ({\mathcal{S}}_1\cup \dots {\mathcal{S}}_n)\in {\mathrm{Strat}}_{\sigma }(v)}\prod _{w_i\in vE}{h}_{\sigma }(v{w}_i)\cdot F({\mathcal{S}}_i))=\sum _{\mathcal{S}\in {\mathrm{Strat}}_{\sigma }(v)}F(\mathcal{S}).$$

$$f_0(v)=\underset{\mathcal{S}\in {\mathrm{Strat}}_0(v)}{\min }F(\mathcal{S})$$

$$f_{\sigma }(v)=\sum _{w\in vE}h(vw)f_{\sigma }(w)\text{ and }{f}_{1-\sigma }(v)=\prod _{w\in vE}h(vw)f_{1-\sigma }(w).$$

$$f_{\sigma }(v)f_{1-\sigma }(v)=$$

$$\displaystyle\sum_{w\in vE}\Bigl{(}h_{\sigma}(vw)f_{\sigma}(w)\prod_{w^{\prime}\in vE}h_{1-\sigma}(vw^{\prime})f_{1-\sigma}(w^{\prime})\Bigr{)}=$$

$$\displaystyle\sum_{w\in vE}\bigl{(}h_{\sigma}(vw)h_{1-\sigma}(vw)f_{\sigma}(w)f_{1-\sigma}(w)\prod_{w^{\prime}\in vE\setminus\{w\}}h_{1-\sigma}(vw^{\prime})f_{1-\sigma}(w^{\prime})\bigr{)}.$$

$${\mathrm{Lit}}_A(\tau ):={\mathrm{Atoms}}_A(\tau )\cup {\mathrm{NegAtoms}}_A(\tau )\cup \{a\mathrm{op}b:a,b\in A\},$$

$$\pi [[\psi \vee \phi ]]:=\pi [[\psi ]]+\pi [[\phi )]]$$

$$\pi [[\exists x\phi (x)]]:=\sum _{a\in A}\pi [[\phi (a)]]$$

$$\sum _{i\in \omega }{b}_i:=\sup \{a_0+\cdots +a_n:n\in \omega \}$$

$$X_1=g_1(X_1,\dots ,x_n),\dots ,X_n=g_n(X_1,\dots ,X_n),$$

$$X_v$$

$$(G_{\sigma })X_v$$

$$X_v$$

$$T^{(n)}:=\{\pi v\in V^{(n)}:v\in T\}\cup \{\pi v\in V^{(n)}:|\pi |=n-1,v\in V\setminus T\}.$$

$$F(\mathcal{S}):=\prod _{e\in E}{h}_{\sigma }(e{)}^{{\#}_{\mathcal{S}}(e)}\cdot \prod _{v\in T}{f}_{\sigma }(v{)}^{{\#}_{\mathcal{S}}(v)}$$

$$\sum _{\mathcal{S}\in {\mathrm{Strat}}_{\sigma }(v)}F({\mathcal{S}}^{(n)})=\sum _{\mathcal{T}\in {\mathrm{Strat}}_{\sigma }^{(n)}(v)}F(\mathcal{T}).$$

$$f_{\sigma }(v):=(\mathrm{lfp}{G}_{\sigma })(v)=\sum _{\mathcal{S}\in {\mathrm{Strat}}_{\sigma }(v)}F(\mathcal{S}).$$

$$f_{\sigma }(v)=\sum _{\mathcal{S}\in {\mathrm{Strat}}_{\sigma }(v)}\prod _{x\in \mathrm{Plays}(\mathcal{S})}{f}_{\sigma }(x).$$

$$G^n(v)=f_{\sigma }^n(v)=\sum _{\mathcal{T}\in {\mathrm{Strat}}_{\sigma }^{(n)}(v)}F(\mathcal{T})=\sum _{\mathcal{S}\in {\mathrm{Strat}}_{\sigma }(v)}F({\mathcal{S}}^{(n)}).$$

$$[\mathrm{gfp}R\overline{x}.\psi ](\overline{x})\equiv \neg [\mathrm{lfp}R\overline{x}.\neg \psi [R/\neg R]](\overline{x}).$$

$$F_{\pi }^{\phi }(g):\overline{a}\mapsto \pi [R\mapsto g][[\phi (R,\overline{a})]].$$

$$c+\underset{i\in \omega }{\inf }{a}_i=\underset{i\in \omega }{\inf }(c+a_i)\text{ and }c\cdot \underset{i\in \omega }{\inf }{a}_i=\underset{i\in \omega }{\inf }(c\cdot a_i).$$

$$F^{\mu }(\mathcal{S}):=\prod _{x\in \mathrm{Plays}(\mathcal{S})}{f}_{\sigma }^{\mu }(x)\text{ and }{F}^{\nu }(\mathcal{S}):=\prod _{x\in \mathrm{Plays}(\mathcal{S})}{f}_{\sigma }^{\nu }(x)=\prod _{t\in T}{t}^{{\#}_{\mathcal{S}}(t)}.$$

$$(\mathrm{lfp}{G}_{\sigma })(v):=\sum _{\mathcal{S}\in {\mathrm{Strat}}_{\sigma }(v)}{F}^{\mu }(\mathcal{S})\text{ and }(\mathrm{gfp}{G}_{\sigma })(v):=\sum _{\mathcal{S}\in {\mathrm{Strat}}_{\sigma }(v)}{F}^{\nu }(\mathcal{S}).$$

$$f_{\sigma }^n(v)=\sum _{\mathcal{T}\in {\mathrm{Strat}}_{\sigma }^{(n)}(v)}F(\mathcal{T}).$$

$$\sum _{\mathcal{S}\in {\mathrm{Strat}}_{\sigma }(v)}F({\mathcal{S}}^{(n)})=\sum _{\mathcal{T}\in {\mathrm{Strat}}_{\sigma }^{(n)}(v)}F(\mathcal{T}).$$

Full text

1 Introduction

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. In database theory, provenance analysis based on interpretations in commutative semirings has been developed for positive database query languages, to understand which combinations of the atomic facts in a database can be used for deriving the result of a given query. In this approach, atomic facts are interpreted not just by true or false, but by values in an appropriate semiring, where 0 is the value of false statements, whereas any element $a\neq 0$ of the semiring stands for some shade of truth. These values are then propagated from the atomic facts to arbitrary queries in the language, which permits to answer questions such as the minimal cost of a query evaluation, the confidence one can have that the result is true, the number of different ways in which the result can be computed, or the clearance level that is required for obtaining the output, under the assumption that some facts are labelled as confidential, secret, top secret, etc. We refer to [15] for a recent account and many references on the semiring framework for database provenance.

Scenarios to which the semiring provenance approach has been successfully applied include unions of conjunctive queries, positive relational algebra, nested relations, Datalog, XQuery, SQL-aggregates and several others, and it has been implemented in software systems such as Orchestra and Propolis. For details, see e.g. [2, 6, 7, 12, 14, 17]. A main limitation of this approach is that is has been largely confined to positive query languages. Attempts to add operations that capture difference of relations have led to interesting and algebraically challenging, but divergent approaches [1, 8, 9, 13]. In particular there has been no systematic approach in database theory for tracking negative information, and no convincing provenance analysis for languages with full negation.

Here, we would like to develop a new approach for a semiring provenance analysis for model checking problems of logics with negation, in particular first-order logic and fixed-point logic. This approach is based on several ideas:

• •

Provenance analysis of logics is intimately connected to provenance analysis of games. In the same way as formula evaluation or model checking can be formulated in game theoretic terms, also the propagation of provenance values from atomic facts to arbitrary formulae can be viewed as a process on the associated games. Also the typical results of a provenance analysis of database queries or logical formulae, concerning for instance confidence scores, costs, required clearance level, or number of ‘proof trees’ have natural game-theoretic interpretations. In fact, provenance analysis of games is of independent interest, and provenance values of positions in a game provide detailed information about the number and properties of the strategies of the players, far beyond the question whether or not a player has a winning strategy from a given position.

• •

We deal with negation by transformation to negation normal form. This is the common approach for the design of model checking games and game-based evaluation algorithms. But while this is there mainly a matter of convenience (to avoid role switches between players during a play), provenance semantics imposes even stronger reasons for transformations to negation normal form. Indeed, beyond Boolean semantics, negation is not a compositional logical operation: the provenance value of $\neg\varphi$ is not necessarily determined by the provenance value of $\varphi$.

• •

On the algebraic side, we introduce new provenance semirings of polynomials and formal power series, which take negation into account. They are obtained by taking quotients of traditional provenance semirings by congruences generated by products of positive and negative provenance tokens; they are called semirings of dual-indeterminate polynomials or dual-indeterminate power series.

Preliminary accounts of our approach, confined to first-order logic and without the connection to games, but discussing potential applications to issues such as model updates, and reverse provenance analysis (e.g., confidence maximization), have been given in [18] and [10]. Here we put also the provenance analysis of games into focus, in fact we develop our approach here from the perspectives of games. We shall first discuss the case of finite acyclic games which are sufficient for the provenance analysis of first-order logic and its fragments. Most of the central issues of our approach, in particular the view of provenance values in terms of valuations of strategies and plays, appear already in this simple scenario. We shall then discuss reachability games on graphs that admit cycles. These are the games that are relevant for the provenance analysis of logics with least (but without greatest) fixed points. For these it will be necessary to restrict from arbitrary commutative semirings to $\omega$-continuous ones. Such an analysis has previously been carried out for Datalog, but to deal with (atomic) negation we have to combine this with the idea of taking quotients by the duality on indeterminates, which will lead us to semirings of dual-indeterminate power series. Finally we shall outline a provenance approach for safety games and greatest fixed points. Our central algebraic tools here are absorptive semirings, in particular the semiring ${\mathbb{S}}^{\infty}[X]$ of generalized absorptive polynomials, admitting also infinite exponents.

This paper is intended to lay foundations for our general approach to a provenance analysis of logic and games, that should take us far beyond the specific cases studied here. The application of the acyclic case to modal and guarded logics has been analysed in [5]. In [19] our approach has been applied to database repairs; it has been shown how our treatment of negation, or absent information, can be used to explain and repair missing query answers and the failure of integrity constraints in databases. Further, the potential of the provenance methods developed here for applications in knowledge represenation and description logics has been discussed in [4]. Work in progress includes the provenance analysis of temporal and dynamic logics in the setting of absorptive semirings, the study of logics of dependence and independence from the point of view of provenance, and the algorithmic analysis of computing provenance values in various settings.

2 Commutative semirings

Definition \thetheorem.

A commutative semiring is an algebraic structure $(K,+,\cdot,0,1)$, with $0\neq 1$, such that $(K,+,0)$ and $(K,\cdot,1)$ are commutative monoids, $\cdot$ distributes over $+$, and $0\cdot a=a\cdot 0=0$. A semiring is +-positive if $a+b=0$ implies $a=0$ and $b=0$. This excludes rings. A semiring is root-integral if $a\cdot a=0$ implies $a=0$. All semirings considered in this paper are commutative, +-positive and root-integral. Further, a commutative semiring is positive if it is +-positive and has no divisors of 0 (i.e. $a\cdot b=0$ implies that $a=0$ and $b=0$). The standard semirings considered in provenance analysis are in fact positive, but for an appropriate treatment of negation we shall introduce later in this paper semirings (of dual-indeterminate polynomials or power series) that have divisors of 0.

Notice that a semiring $K$ is positive if, and only if, the unique function $h:K\rightarrow\{0,1\}$ with $h^{-1}(0)=\{0\}$ is a homomorphism from $K$ into the Boolean semiring ${\mathbb{B}}=(\{0,1\},\lor,\land,0,1)$. A semiring $K$ is (+)-idempotent if $a+a=a$, for all $a\in K$, and $(+,\cdot)$-idempotent if, in addition, $a\cdot a=a$ for all $a$. Further, $K$ is absorptive if $a+ab=a$, for all $a,b\in K$. Obviousy, every absorptive semiring is (+)-idempotent.

Elements of a commutative semiring will be used as truth values for logical statements and as values for positions in games. The intuition is that + describes the alternative use of information, as in disjunctions or existential quantifications, or for different possible choices of a player in a game, whereas $\cdot$ stands for the joint use of information, as in conjunctions or universal quantifications, or for choices in a game that are controlled by the opponent of the given player. Further, 0 is the value of false statements or losing positions, whereas any element $a\neq 0$ of a semiring $K$ stands for a “nuanced” interpretation of true or as a value of a non-losing position.

**Application semirings. ** We briefly discuss some specific semirings that provide interesting information but about a logical statement or a position in a game.

• •

The Boolean semiring $\mathbb{B}=(\{0,1\},\vee,\wedge,0,1)$ is the standard habitat of logical truth.

• •

$\mathbb{N}=(\mathbb{N},+,\cdot,0,1)$ is used here for counting winning strategies in games. It also plays an important role for bag semantics in databases.

• •

$\mathbb{T}=(\mathbb{R}_{+}^{\infty},\min,+,\infty,0)$ is called the tropical semiring. It has many applications in several areas of computer science. It is used here for measuring the cost of strategies.

• •

The Viterbi semiring $\mathbb{V}=([0,1],\max,\cdot,0,1)$ is isomorhic to $\mathbb{T}$ via $x\mapsto e^{-x}$ and $y\mapsto-\ln y$. We will think of the elements of $\mathbb{V}$ as confidence scores and use it to describe the confidence that a player can win from a given position or the confidence assigned to a logical statement.

• •

The min-max semiring on a totally ordered set $(A,\leq)$ with least element $a$ and greatest element $b$ is the semiring $(A,\max,\min,a,b)$.

**Provenance semirings. ** Beyond the traditional application semirings, there are some important provenance semirings of polynomials that are used for a general provenance analysis. These semirings have algebraic universality properties (they are freely generated) for various classes of semirings. This allows us to compute provenance values once in a general such semiring and then to specialise it via homomorphisms (i.e. evaluation of the polynomials) to specific application semirings as needed.

• •

For any set $X$, the semiring $\mathbb{N}[X]=(\mathbb{N}[X],+,\cdot,0,1)$ consists of the multivariate polynomials in indeterminates from $X$ and with coefficients from $\mathbb{N}$. This is the commutative semiring freely generated by the set $X$.

• •

By dropping coefficients from $\mathbb{N}[X]$, we get the semiring ${\mathbb{B}}[X]$ whose elements are just finite sets of distinct monomials. It is the free (+)-idempotent semiring over $X$.

• •

By dropping also exponents, we get the semiring ${\mathbb{W}}[X]$ of finite sums of monomials that are linear in each argument. It is sometimes called the Why-semiring.

• •

The free absorptive semiring ${\mathbb{S}}[X]$ over $X$ consists of 0,1 and all antichains of monomials with respect to the component-wise order on their exponents. It is the quotient of ${\mathbb{N}}[X]$ by the congruence induced by $p\sim q$ for monomials $p,q$ with $p=qr$.

• •

Finally $\mathsf{PosBool}(X)=(\mathsf{PosBool}(X),\vee,\wedge,\bot,\top)$ is the semiring whose elements are classes of equivalent positive (monotone) boolean expressions with variables from $X$ (its elements are in bijection with the positive boolean expressions in irredundant disjunctive normal form). This is the distributive lattice freely generated by the set $X$.

3 Games

We consider two-player turn-based games on graphs. Such a game is defined by the game graph on which it is played, and by the objectives of the players.

Definition \thetheorem.

A game graph is a structure ${\cal G}=(V,V_{0},V_{1},T,E)$, where $V=V_{0}\cup V_{1}\cup T$ is the set of positions, partitioned into the sets $V_{0}$, $V_{1}$ of the two players and the set $T$ of terminal positions, and where $E\subseteq V\times V$ is the set of moves. We denote the set of immediate successors of a position $v$ by $vE:=\{w:(v,w)\in E\}$ and require that $vE=\varnothing$ if, and only if, $v\in T$. A play from an initial position $v_{0}$ is a finite or infinite path $v_{0}v_{1}v_{2}\dots$ through ${\cal G}$ where the successor $v_{i+1}\in v_{i}E$ is chosen by Player 0 if $v_{i}\in V_{0}$ and by Player 1 if $v_{1}\in V_{1}$. A play ends when it reaches a terminal node $v_{m}\in T$.

Definition \thetheorem.

For every game graph ${\cal G}=(V,V_{0},V_{1},T,E)$, and every initial position $v_{0}\in V$, the tree unraveling of ${\cal G}$ from $v_{0}$ is the game tree ${\cal T}({\cal G},v_{0})$ consisting of all finite paths from $v_{0}$. More precisely, ${\cal T}({\cal G},v)=(V^{\#},V_{0}^{\#},V_{1}^{\#},T^{\#},E^{\#})$, where $V^{\#}$ is the set of all finite paths $\pi=v_{0}v_{1}\dots v_{m}$ through ${\cal G}$, with $V_{\sigma}^{\#}=\{\pi v\in V^{\#}:v\in V_{\sigma}\}$, $T^{\#}=\{\pi t\in V^{\#}:t\in T\}$, and $E^{\#}=\{(\pi v,\pi vv^{\prime}):(v,v^{\prime})\in E\}$. For most game-theoretic considerations, the games played on ${\cal G}$ and its unravelings are equivalent, via the canonical projection $\rho:{\cal T}({\cal G},v_{0})\rightarrow{\cal G}$ that maps every path $\pi v$ to its end point $v$.

A strategy for a player in a game is a function that selects moves at points that are controlled by that player. A strategy need not be defined at all positions of a player, but it must be closed in the sense that it defines a move from each position that is reachable by a play that is admitted by the strategy. There are several possibilities to define the notion of a strategy formally. For our purposes it is convenient to identify a strategy with the histories of plays that it admits, i.e. to view it as an appropriate subtree of ${\cal T}({\cal G},v_{0})$.

Definition \thetheorem.

A strategy of Player $\sigma$ (for $\sigma\in\{0,1\}$) from $v_{0}$ in a game ${\cal G}$ is a subtree of ${\cal T}({\cal G},v_{0})$, of the form ${\cal S}=(W,F)$ with $W\subseteq V^{\#}$ and $F\subseteq(W\times W)\cap E^{\#}$, satisfying the following conditions:

• •

$W$ is closed under predecessors: if $\pi v\in W$ then also $\pi\in W$.

• •

If $\pi v\in W\cap V^{\#}_{\sigma}$, then $|(\pi v)F|=1$.

• •

If $\pi v\in W\cap V^{\#}_{1-\sigma}$ then $(\pi v)F=(\pi v)E^{\#}$.

We write $\mathrm{Strat}_{\sigma}(v_{0})$ for the set of all strategies of Player $\sigma$ from $v_{0}$.

In a strategy ${\cal S}=(W,F)$, the set $W$ is the part of ${\cal T}({\cal G},v_{0})$ on which the strategy is defined, and $F$ is the set of moves that are admitted by the strategy. A strategy ${\cal S}\in\mathrm{Strat}_{\sigma}(v_{0})$ induces the set $\operatorname{\mathrm{Plays}}({\cal S})$ of those plays from $v_{0}$ whose moves are consistent with ${\cal S}$. We call ${\cal S}$ well-founded if it does not admit any infinite plays; this is always the case on finite acyclic game graphs, but need not be the case otherwise. The set of possible outcomes of a strategy ${\cal S}$ is the set of terminal nodes that are reachable by a play that is consistent with ${\cal S}$. A strategy can also be viewed as a function ${\cal S}:W\cap V_{\sigma}^{\#}\rightarrow V$ such that ${\cal S}(\pi v)\in vE$ defines the node to which Player $\sigma$ moves from $\pi v$.

The simplest objectives of players are reachability and safety objectives.

Definition \thetheorem.

A reachability objective for Player $\sigma$ is given by a set $T_{\sigma}\subseteq T$ of winning terminal positions. With such an objective, Player $\sigma$ wins every play that reaches a position in $T_{\sigma}$. Dually, a safety objective for Player $\sigma$ is given by a set $L_{\sigma}\subseteq T$ of ‘losing’ positions that the player has to avoid, or equivalently, by its complement $S_{\sigma}=V\setminus L_{\sigma}$, the region of safe positions inside of which the Player has to keep the play. With such an objective Player $\sigma$ wins every play, finite or infinite, that never reaches a position in $L_{\sigma}$.

Notice that the difference between reachability and safety objectives is relevant only in cases where infinite plays are possible. Indeed, in a game that admits only finite plays, Player $\sigma$ wins a play with the reachability objective $T_{\sigma}$ if, and only if, she wins that play with the safety objective given by $L_{\sigma}=T\setminus T_{\sigma}$, so we can always reformulate reachability by safety and vice versa. However, in a game that admits infinite plays, Player $\sigma$ wins with a reachability objective $T_{\sigma}$ if, and only if, her opponent, Player $1-\sigma$, loses with the safety condition $L_{1-\sigma}=T_{\sigma}$, Hence winning with a reachability objective corresponds to defeating an opponent who plays with a safety objectives. If both players play with reachability objectives, then infinite plays are won by neither player.

4 Provenance for well-founded games

We first study the provenance analysis of games for well-founded games, i.e. games that are played on finite acyclic game graphs ${\cal G}=(V,V_{0},V_{1},T,E)$, and hence do not admit infinite plays. We introduce $K$-valuations $f_{0}$ and $f_{1}$ that associate with every position $v\in V$ provenance values $f_{0}(v)$ and $f_{1}(v)$, respectively. The idea is that, for $\sigma\in\{0,1\}$, the function $f_{\sigma}$ describes the value of each position from the point if view of Player $\sigma$. Such a valuation is induced by its values on the terminal positions, i.e. by a function $f_{\sigma}:T\rightarrow K$, and by a valuation of the moves, i.e. by a function $h_{\sigma}:E\rightarrow K\setminus\{0\}$. Here, the function $f_{\sigma}:T\rightarrow K$ defines the value, for Player $\sigma$, of every terminal position where, intuitively, $f_{\sigma}(t)=0$ means that position $t$ is losing for Player $\sigma$. In the simplest case, we can specify reachability objectives $T_{\sigma}$ by setting $f_{\sigma}(t)=1$ for $t\in T_{\sigma}$ and $f_{\sigma}(t)=0$ otherwise. The functions $h_{\sigma}:E\rightarrow K\setminus\{0\}$ provide a value (or cost) for Player $\sigma$ of the moves. In many cases valuations of moves are not relevant; we then just put $h_{\sigma}(vw)=1$ for all edges $(v,w)\in E$.

The extension of the basic valuations $f_{\sigma}:T\rightarrow K$ and $h_{\sigma}:E\rightarrow K\setminus\{0\}$ to valuations $f_{\sigma}:V\rightarrow K$ for all positions then relies on the idea that a move from $v$ to $w$ contributes to $f_{\sigma}(v)$ the value $h_{\sigma}(vw)\cdot f_{\sigma}(w)$. These contributions are summed up in the case that $v$ is a position for Player $\sigma$ (i.e. when she choses herself the successors), and multiplied in the case that $v$ is a position of the opponent (i.e. when she has to cope with any of the possible successors). This is summarized by the following definition.

Definition 4.1**.**

Let $K$ be a commutative semiring, let ${\cal G}=(V,V_{0},V_{1},T,E)$ be a finite acyclic game graph, and let $\sigma\in\{0,1\}$ denote one of the two players. A $K$-valuation of ${\cal G}$ for Player $\sigma$ is a function $f_{\sigma}:V\rightarrow K$. It is defined from basic valuations $f_{\sigma}:T\rightarrow K$ and $h_{\sigma}:E\rightarrow K\setminus\{0\}$ via backwards induction, by

[TABLE]

An equivalent characterization of the $K$-valuation $f_{\sigma}$ can be obtained by defining provenance values for plays and strategies.

Definition 4.2**.**

For a play $x=v_{0}v_{1}\dots v_{m}$ from $v_{0}$ to a terminal node $v_{m}$, we define its valuation for Player $\sigma$ as $f_{\sigma}(x):=h_{\sigma}(v_{0}v_{1})\cdots h_{\sigma}(v_{m-1}v_{m})\cdot f_{\sigma}(v_{m})$. Let now ${\cal S}=(W,F)\subseteq{\cal T}({\cal G},v_{0})$ be a strategy for Player $\sigma$ from $v_{0}$ and $\rho_{S}:(W,F)\rightarrow(V,E)$ be the restriction of of the canonical homomorphism $\rho:{\cal T}({\cal G},v_{0})\rightarrow{\cal G}$ to ${\cal S}$. For any position $v\in V$ and any move $e\in E$, the values

[TABLE]

indicate how often the position $v$ and the move $e$ appear in the strategy ${\cal S}$. We then define the provenance value ${\cal S}\in\mathrm{Strat}_{\sigma}(v_{0})$ as

[TABLE]

In some important special cases, provenance values of strategies coincides with the product of the provenance values over all plays that they admit.

Lemma 4.3**.**

If $h_{\sigma}(e)=1$ for all moves $e\in E$, or if the underlying semiring is multiplicatively idempotent (i.e. $a^{2}=a$ for all $a$) we have that $F({\cal S})=\prod_{x\in\operatorname{\mathrm{Plays}}({\cal S})}f_{\sigma}(x)$ for all ${\cal S}\in\mathrm{Strat}_{\sigma}(v)$.

However, there are simple games where this is not the case. Consider, for instance, the valuation for Player 0 in a game where only the opponent, Player 1, moves: from position $v$, Player  1 can proceed to $w$ by a move with value $h_{0}(vw)=a$, and from $w$ he has the choice of moving to either $s$ or $t$, both options having value 1 for Player 0. There is only one strategy ${\cal S}$ for Player 0 (do nothing), with provenance value $a$. However, the strategy admits two plays, ending in $s$ and $t$, respectively, both of which have value $a$. Thus the product over the provenance value of the plays is $a^{2}$.

Theorem 4.4**.**

For any commutative semiring $K$ and any finite acyclic game ${\cal G}$, let $f_{\sigma}:V\rightarrow K$ be the provenance valuation for Player $\sigma$, induced by the valuation $f_{\sigma}:T\rightarrow K$ of the terminal nodes and $h_{\sigma}:E\rightarrow K\setminus\{0\}$ of the moves. Then, for every position $v$

[TABLE]

Proof 4.5**.**

For terminal positions $v$ the claim is trivially true. So suppose that $v\in V_{\sigma}$. Then any strategy ${\cal S}\in\mathrm{Strat}_{\sigma}(v)$ can be written in the form ${\cal S}=v\cdot{\cal S}^{\prime}$ for some successor $w\in vE$ and some strategy ${\cal S}^{\prime}\in\mathrm{Strat}_{\sigma}(w)$. Clearly, $\#_{\cal S}(t)=\#_{{\cal S}^{\prime}}(t)$ for every terminal position $t\in T$. For the moves we have that $\#_{\cal S}(e)=\#_{{\cal S}^{\prime}}(e)$ for all $e\neq(v,w)$ but $\#_{S}(e)=1$ and $\#_{{\cal S}^{\prime}}(e)=0$ for $e=(v,w)$. This implies that $F(S)=h(vw)\cdot F({\cal S}^{\prime})$. By induction hypothesis $f_{\sigma}(w)=\sum_{{\cal S}^{\prime}\in\mathrm{Strat}_{\sigma}(w)}\ F({\cal S}^{\prime})$. Hence

[TABLE]

Finally, let $v\in V_{1-\sigma}$ with $vE=\{w_{1},\dots,w_{n}\}$. Every strategy ${\cal S}\in\mathrm{Strat}_{\sigma}(v)$ has the form ${\cal S}=v({\cal S}_{1}\cup\dots\cup{\cal S}_{n})$ with ${\cal S}_{i}\in\mathrm{Strat}_{\sigma}(w_{i})$. For the terminal nodes $t\in T$ we have that $\#_{\cal S}(t)=\sum_{i\leq n}\#_{{\cal S}_{i}}(t)$; similarly, for all moves $e$ from a different position than $v$, we have $\#_{\cal S}(e)=\sum_{i\leq n}\#_{{\cal S}_{i}}(e)$, but for the moves $e=(v,w_{i})$ we have $\#_{\cal S}(e)=1$ and $\#_{{\cal S}_{i}}(e)=0$ for all $i$. Thus $F({\cal S})=\prod_{w_{i}\in vE}h_{\sigma}(vw_{i})\cdot F({\cal S}_{i}))$. It follows that

[TABLE]

From this description, we can derive a number of applications of provenance valuations on games. We first consider the information provided by valuations in the general provenance semirings of polynomials. Let ${\mathbb{N}}[T]$ be the semiring of polynomials with coefficients in ${\mathbb{N}}$ over indeterminates $t\in T$, where $T$ is the set of terminal positions in an acyclic game graph ${\cal G}=(V,V_{0},V_{1},T,E)$. Let $f_{\sigma}:V\rightarrow{\mathbb{N}}[T]$ be the valuation induced by setting $f_{\sigma}(t)=t$ for $t\in T$ and $h_{\sigma}(vw)=1$ for all edges $(v,w)$, so that the value of a play is just its outcome, i.e. the terminal position where it ends.

Clearly, we can write $f_{\sigma}(v)$ as a sum of monomials $m\cdot t_{1}^{j_{1}}\dots t_{k}^{j_{k}}$. This provides a detailed description of the number and properties of the strategies that Player $\sigma$ has from position $v$.

Theorem 4.6**.**

The valuation $f_{\sigma}(v)\in{\mathbb{N}}[T]$ is the sum of those monomials $m\cdot t_{1}^{j_{1}}\dots t_{k}^{j_{k}}$ (with $m,j_{1}\dots,j_{k}>0$) such that Player $\sigma$ has precisely $m$ strategies ${\cal S}\in\mathrm{Strat}_{\sigma}(v)$ with the property that the set of possible outcomes for ${\cal S}$ is precisely $\{t_{1},\dots,t_{k}\}$, and precisely $j_{i}$ plays that are consistent with ${\cal S}$ have the outcome $t_{i}$.

This is an immediate consequence of Theorem 4.4 and Lemma 4.3. In many cases, somewhat less detailed information is sufficient, which can be obtained by valuations in less informative provenance semirings than ${\mathbb{N}}[T]$:

• •

Evaluating $f_{\sigma}(v)$ in the idempotent semiring ${\mathbb{B}}[T]$ gives us the sum of monomials $t_{1}^{j_{1}}\dots t_{k}^{j_{k}}$ for which Player $\sigma$ has at least one strategy whose multiset of admitted outcomes consists of $t_{1},\dots,t_{k}$ with multiplicities $j_{1},\dots,j_{k}$, respectively.

• •

If we evaluate $f_{\sigma}(v)$ in ${\mathbb{W}}[T]$ we get the sum of monomials $t_{1}\dots t_{m}$ such that Player $\sigma$ has a strategy whose set of outcomes is $\{t_{1},\dots t_{m}\}$. The information on multiplicities of strategies and outcomes is dropped.

• •

An interesting case is the evaluation in the absorptive semiring ${\mathbb{S}}[X]$. For two strategies ${\cal S},{\cal S}^{\prime}\in\mathrm{Strat}_{\sigma}(v)$, we say that ${\cal S}$ absorbs ${\cal S}^{\prime}$ if for every terminal position $t\in T$, ${\cal S}$ admits less plays with outcome $t$ than ${\cal S}^{\prime}$. We call ${\cal S}$ absorption-dominant if it is not absorbed by any other strategy. Now, $f_{\sigma}(v)\in{\mathbb{S}}[X]$ is the sum of monomials $t_{1}^{j_{1}}\dots t_{k}^{j_{k}}$ that describe precisely the (multiset of outcomes of the) absorption dominant strategies of Player $\sigma$ from $v$. See Sect. 11 below for a more detailed analysis of absorption among strategies.

• •

Finally, the evaluation of $f_{\sigma}(v)\in\mathsf{PosBool}[T]$ consists of those monomials $t_{1}\dots t_{k}$ such that $\{t_{1},\dots,t_{k}\}$ a minimal set among the sets of outcomes of strategies ${\cal S}\in\mathrm{Strat}_{\sigma}(v)$.

Fix any reachability objective $W\subseteq T$. In any of these provenance semirings, we can write the polynomial $f_{\sigma}(v)$ as a sum $f_{\sigma}(v)=f^{W}_{\sigma}(v)+g^{W}_{\sigma}(v)$ where $f^{W}_{\sigma}(v)$ is the sum of those monomials that only contain indeterminates in $W$ and $g^{W}_{\sigma}(v)$ contains the rest.

Theorem 4.7**.**

For every subset $W\subseteq T$ and every $v\in V$, Player $\sigma$ has a strategy to reach $W$ from $v$ if, and only if, $f^{W}_{\sigma}(v)\neq 0$ (in any of the provenance semirings given above). Moreover, if we set $f(t)=1$ for $t\in W$ and $f(t)=0$ for $t\in T\setminus W$, and evaluate $f_{\sigma}$ in the semiring ${\mathbb{N}}$ of natural numbers, then $f_{\sigma}(v)$ is the number of distinct winning strategies for Player $\sigma$ to reach $W$ from $v$.

Evaluation in other application semirings gives further interesting information about strategies:

**Cost of strategies. ** Given a game ${\cal G}$, we associate with Player 0 cost functions $f_{0}:T\rightarrow{\mathbb{R}}_{+}$ and $h:E\rightarrow{\mathbb{R}}_{+}$ for the terminal positions and the moves. We define the cost of a strategy ${\cal S}\in\mathrm{Strat}_{0}(v)$ as the sum of the costs of all moves and outcomes that it admits, weighted by the number of their occurrences.

Proposition 4.8**.**

The cost of an optimal strategy from $v$ in ${\cal G}$ is given by the valuation $f_{0}(v)$ in the tropical semiring $\mathbb{T}=({\mathbb{R}}_{+}^{\infty},\min,+,\infty,0)$.

Proof 4.9**.**

Since the product in $\mathbb{T}$ is addition in ${\mathbb{R}}_{+}^{\infty}$, the cost of a strategy ${\cal S}$ for Player 0, as defined above, coincides with the valuation $f_{0}({\cal S})$ in $\mathbb{T}$. The summation in $\mathbb{T}$ is minimization in ${\mathbb{R}}_{+}^{\infty}$, so from Theorem 4.4 we get that

[TABLE]

describes indeed the minimial cost of a strategy for Player 0 from position $v$.

**Clearance levels. ** The access control semiring is $\mathbb{A}=(\{\mathsf{P}<\mathsf{C}<\mathsf{S}<\mathsf{T}<0\},\min,\max,0,\mathsf{P})$ where $\mathsf{P}$ is “public”, $\mathsf{C}$ is “confidential”, $\mathsf{S}$ is “secret”, $\mathsf{T}$ is “top secret”, and [math] is “so secret that nobody can access it!”. Let $f_{\sigma}:T\rightarrow\mathbb{A}$ and $h_{\sigma}:E\rightarrow\mathbb{A}\setminus\{0\}$ define access levels for the terminal positions and the moves for Player $\sigma$, in the sense that Player $\sigma$ can make a move $e$ if, and only if, his personal clearance level is at least $h(e)$ and similarly, he can access a terminal position $t$ if, and only if, his clearance level is at least $f_{\sigma}(t)$.

Proposition 4.10**.**

The valuation $f_{\sigma}(v)\in\mathbb{A}$ describes the minimal clearance level that Player 0 needs to win from position $v$, i.e. to have a strategy that guarantees to reach a terminal position that is accessible for him.

The proof is a straightforward induction.

**Confidence in games. ** Suppose that $f_{\sigma}:T\rightarrow[0,1]$ describes the confidence that Player $\sigma$ puts into $t$ being a winning position for her. We want to compute confidence scores $f_{\sigma}(v)$ to describe the confidence of Player $\sigma$ that she can win from $v$. It is natural to define the confidence score $f_{\sigma}(v)$ as the maximum of the confidence scores of the successors $w\in vE$ in the case that $v\in V_{\sigma}$. For confidence scores of combinations of events whose choice is taken by an opponent, such as for the possible moves from a position $v\in V_{1-\sigma}$, there are different approaches in the literature. A popular one, with which we work here, takes the product of the confidence scores of the events from which the opponent choses. Adopting this definition, the following proposition is immediate.

Proposition 4.11**.**

Confidence scores are computed as semiring valuations $f_{\sigma}:V\rightarrow{\mathbb{V}}$ in the Viterbi semiring ${\mathbb{V}}=([0,1],\max,\,\cdot\,,0,1)$.

**Min-Max Games. ** Finally note that valuations in a min-max semiring $(A,\max,\min,a,b)$ describe the value of positions in games where Player 0 tries to maximize and Player 1 tries to minimize the outcome of the play.

**Separating Valuations. ** The $K$-valuations $f_{0},f_{1}$ for the two players in a game ${\cal G}$, as defined by Definition 4.1, are a priori completely independent of each other. This admits the treatment of a wide variety of games, without any restrictions on how the objectives of the two players relate to each other. For instance, in a completely cooperative game, the basic valuations of of the terminal positions would be the same for Player 0 and Player 1. However, in many games, the objectives of the two players are antagonistic, and valuations $f_{0}$ and $f_{1}$ should reflect this. This motivates the following definition.

Definition 1**.**

Let ${\cal G}$ be a game graph, with valuations $f_{0},f_{1}$ for the two players in a semiring $K$, and let $U\subseteq V$ be a set of positions. We say that

• (1)

$f_{0},f_{1}$* for the two players are separating on $U$ if for all $u\in U$, either $f_{0}(u)=0$ or $f_{1}(u)=0$.*

• (2)

$f_{0},f_{1}$* are weakly separating on $U$ if $f_{0}(u)f_{1}(u)=0$ for all $u\in U$. Notice that in the case where $K$ has no divisors of 0, weakly separating valuations are in fact separating.*

• (3)

$f_{0}$* and $f_{1}$ are strongly separating on $U$, if they are separating, and in addition, $f_{0}(u)+f_{1}(u)\neq 0$ for all $u\in U$.*

Proposition 2**.**

If two valuations $f_{0}$ and $f_{1}$ are (weakly) separating on the the terminal positions of ${\cal G}$, then they are (weakly) separating on all positions of ${\cal G}$.

Proof 4.12**.**

Recall that all our semirings are assumed to be +-positive. For $v\in V_{\sigma}$, we have that

[TABLE]

It follows that $f_{0}$ and $f_{1}$ are separating on $v$ if they are separating on all $w\in vE$. Further,

[TABLE]

This proves that $f_{0}$ and $f_{1}$ are weakly separating on $v$ if they are so on all $w\in vE$.

The corresponding implication for strongly separating valuations does not hold for all +-positive semirings, but it holds for positive ones.

Proposition 3**.**

If two valuations $f_{0}$ and $f_{1}$ into a positive semiring are strongly separating on the the terminal positions of ${\cal G}$, then they are so on all positions of ${\cal G}$.

Proof 4.13**.**

By induction. Assume that $f_{0}$ and $f_{1}$ are strongly separating on all $w\in vE$. Then $f_{\sigma}(v)+f_{1-\sigma}(v)=0$ only if $f_{\sigma}(w)=0$ for all $w\in vE$ and $f_{1-\sigma}(w)=0$ for at least one $w\in vE$. But this implies that $f_{0}(w)+f_{1}(w)=0$ for some $w\in vE$ which contradicts our assumption.

*Note that for the Boolean semiring $K={\mathbb{B}}$, this is just Zermelo’s Theorem on the determinacy of reachability games on well-founded game graphs: from every position, one of the two players has a winning strategy. **Counting positional winning strategies? *** A strategy is positional if it only depends on the current position, and not on the history of the play, i.e. if ${\cal S}(\pi v)={\cal S}(\pi^{\prime}v)$ for all $v$ and all paths $\pi v$, $\pi^{\prime}v$ that lead to $v$. A positional strategy can be described by a function $s:V_{\sigma}\rightarrow V$ or by a subgraph ${\cal S}$ of ${\cal G}$ (rather than of ${\cal T}({\cal G},v_{0})$). Given that in the study of games there is (for instance for algorithmic reasons) a strong interest in positional strategies, it is reasonable to ask whether there exist valuations in different semirings that count just the positional strategies. However, invariance under counting bisimulation shows that this is not possible.

Definition 4**.**

Let ${\cal G}=(V,V_{0},V_{1},T,E)$ and ${\cal G}^{\prime}=(V^{\prime},V^{\prime}_{0},V^{\prime}_{1},T^{\prime},E^{\prime})$ be two game graphs. A counting bisimulation between ${\cal G}$ and ${\cal G}^{\prime}$ is a relation $Z\subseteq V\times V$ such that for every pair $(v,v^{\prime})\in Z$ we have that

• (1)

$v\in V_{\sigma}$* if, and only if, $v^{\prime}\in V^{\prime}_{\sigma}$ and $v\in T$ if, and only if, $v^{\prime}\in T^{\prime}$, and*

• (2)

there is a local bijection $z_{vv^{\prime}}:vE\rightarrow v^{\prime}E^{\prime}$ between the immediate successors of $v$ and $v^{\prime}$ such that $(w,z_{vv^{\prime}}(w))\in Z$, for every $w\in vE$.

We write ${\cal G},v\sim{\cal G}^{\prime},v^{\prime}$ if there is a counting bisimulation $Z$ between ${\cal G}$ and ${\cal G}^{\prime}$ such that $(v,v^{\prime})\in Z$. Notice that for any game graph ${\cal G}$, the relation $Z=\{(v,\pi v):v\in V,\pi v\in V^{\#}\}$ is a counting bisimulation between ${\cal G}$ and its unraveling ${\cal T}({\cal G},v_{0})$.

$K$-valuations of games are invariant under counting bisimilarity in the following sense. Let ${\cal G}$ and ${\cal G}^{\prime}$ be two acyclic game graphs with $K$-valuations $f_{\sigma}:T\rightarrow K$ and $f^{\prime}_{\sigma}:T^{\prime}\rightarrow K$ of the terminal positions and $h:E\rightarrow K$ and $h^{\prime}:E^{\prime}\rightarrow K$ of the moves. We say that a counting bisimulation $Z\subseteq V\times V^{\prime}$ respects these valuations if $f_{\sigma}(t)=f^{\prime}_{\sigma}(t^{\prime})$ for all $(t,t^{\prime})\in Z\cap T\times T^{\prime}$, and $h_{\sigma}(vw)=h^{\prime}_{\sigma}(v^{\prime}w^{\prime})$ whenever $(v,v^{\prime})\in Z$ and $(w,w^{\prime})\in Z$.

Proposition 5**.**

Let $Z$ be a counting bisimulation between ${\cal G}$ and ${\cal G}^{\prime}$ that respects the basic valuations of the terminal positions and the moves. Then $Z$ respects the valuations of all positions, i.e. $f_{\sigma}(v)=f^{\prime}_{\sigma}(v^{\prime})$ for all $(v,v^{\prime})\in Z$.

Proof 4.14**.**

Let $(v,v^{\prime})\in Z$. If $v$ and $v^{\prime}$ are terminal positions, then $f_{\sigma}(v)=f^{\prime}_{\sigma}(v^{\prime})$ by assumption. Otherwise, $v$ and $v^{\prime}$ are both positions of the same player. If they belong to Player $\sigma$, then $f_{\sigma}(v)=\sum_{w\in vE}f_{\sigma}(w)$. The local bijection $z_{vv^{\prime}}$ maps every $w\in vE$ to some $w^{\prime}\in v^{\prime}E^{\prime}$ such that, by induction hypothesis, $f_{\sigma}(w)=f^{\prime}_{\sigma}(w^{\prime})$. Hence $f^{\prime}_{\sigma}(v^{\prime})=\sum_{w^{\prime}\in v^{\prime}E^{\prime}}f^{\prime}_{\sigma}(w^{\prime})=\sum_{w\in vE}f_{\sigma}(w)=f_{\sigma}(v)$. If $v$ and $v^{\prime}$ belong to Player ($1-\sigma$) the reasoning is completely analogous, taking a product rather than a sum.

In particular $K$-valuations of acyclic games do not change if we replace a game graph ${\cal G}$ by one of its unravelings ${\cal T}({\cal G},v)$. Indeed, every valuation $f_{\sigma}:T\rightarrow K$ on the terminal positions of a game graph ${\cal G}$ extends to the same valuation for $v$ on ${\cal G}$ as on the tree unraveling ${\cal T}({\cal G},v)$. On the other side, every strategy on a tree-shaped game graph is positional. Thus the number of positional winning strategies is certainly not invariant under unraveling and hence not definable by valuations in a semiring.

5 Provenance for first-order logic via model checking games and dual-indeterminate polynomials

Given a finite relational vocabulary $\tau$ and a finite non-empty universe $A$, we denote by $\operatorname{\mathrm{Atoms}}_{A}(\tau)$ the set of all atoms $R\overline{a}$ with $R\in\tau$ and $\overline{a}\in A^{k}$. Further, let $\operatorname{\mathrm{NegAtoms}}_{A}(\tau)$ be the set of all negated atoms $\neg R\overline{a}$ where $R\overline{a}\in\operatorname{\mathrm{Atoms}}_{A}(\tau)$, and consider the set of all $\tau$-literals on $A$,

[TABLE]

where $\operatorname{\mathrm{\,op\,}}$ stands for $=$ or $\neq$.

Definition 6**.**

Given any commutative semiring $K$, a $K$-interpretation (for $\tau$ and $A$) is a function $\pi:\operatorname{\mathrm{Lit}}_{A}(\tau)\rightarrow K$ that maps equalities and inequalities to their truth values 0 or 1.

We have defined in **[10]** how a semiring interpretation extends to a full valuation $\pi:{\rm FO}(\tau)\rightarrow K$ mapping any fully instantiated formula $\psi(\overline{a})$ (or equivalently, any first-order sentence of vocabulary $\tau\cup A$), to a value $\pi[\![\psi]\!]$, by setting

[TABLE]

Negation is handled via negation normal forms: we set $\pi[\![\neg\varphi]\!]:=\pi[\![\operatorname{\mathrm{nnf}}(\neg\varphi)]\!]$ where $\operatorname{\mathrm{nnf}}(\varphi)$ is the negation normal form of $\varphi$. This is equivalent to the game provenance, as defined above, for the model checking game associated with the formula $\psi$ and the $K$-interpretation $\pi:\operatorname{\mathrm{Lit}}_{A}(\tau)\rightarrow K$. Notice that classically, model checking games are defined for a formula (assumed to be given in negation normal form) and a fixed structure ${\mathfrak{A}}$ (see e.g. **[3, Chap. 4]**). However, the game graph of such a model checking game depends only on the formula $\psi$ and the universe $A$ of the given structure ${\mathfrak{A}}$. It is only the labelling of the terminal positions of the game, as winning for either the Verifier (Player 0) or the Falsifier (Player 1), that depends on which of the literals in $\operatorname{\mathrm{Lit}}_{A}(\tau)$ are true in ${\mathfrak{A}}$. Hence the definition of a model checking game readily generalizes to our more abstract provenance scenario.

Definition 7**.**

Let $\psi(\overline{x})\in{\rm FO}(\tau)$ be a first-order formula in negation normal form with a relational vocabulary $\tau$, and let $A$ be a (finite) universe. The model checking game ${\cal G}(A,\psi)$ has positions $\varphi(\overline{a})$, obtained from a subformula $\varphi(\overline{x})$ of $\psi$, by instantiating the free variables $\overline{x}$ by a tuple $\overline{a}$ of elements of $A$. At a disjunction $(\psi\lor\varphi)$, Player 0 (Verifier) moves to either $\psi$ or $\varphi$, and at a conjunction, Player 1 (Falsifier) makes an analogous move. At a position $\exists x\varphi(\overline{a},x)$, Verifier selects an element $b$ and moves to $\varphi(\overline{a},b)$, whereas at positions $\forall x\varphi(\overline{a},x)$ the move to to the next position $\varphi(\overline{a},b)$ is done by Falsifier. The terminal positions of ${\cal G}(A,\psi)$ are the literals in $\operatorname{\mathrm{Lit}}_{A}(\tau)$.

A $K$-interpretation $\pi:\operatorname{\mathrm{Lit}}_{A}(\tau)\rightarrow K$ thus provides a valuation of the set $T\subseteq\operatorname{\mathrm{Lit}}_{A}(\tau)$ of terminal positions of the model checking game ${\cal G}(A,\psi)$, for any sentence $\psi\in{\rm FO}(\tau\cup A)$. We view it as a valuation $f_{0}$ for Player 0. The associated valuation $f_{1}$ for Player 1 is obtained by setting $f_{1}(\varphi)=\pi[\![\neg\varphi]\!]$ for any literal $\varphi\in\operatorname{\mathrm{Lit}}_{A}(\tau)$. Both valuations then extend to full valuations $f_{0}$ and $f_{1}$ of all positions of ${\cal G}(A,\psi)$, including the position $\psi$ itself. The following result is proved by a straightforward induction on formulae.

Theorem 5.1**.**

For all positions $\varphi$ of ${\cal G}(A,\psi)$ we have that $f_{0}(\varphi)=\pi[\![\varphi]\!]$ and $f_{1}(\varphi)=\pi[\![\neg\varphi]\!]$.

Although this theorem holds without any restrictions on the semiring $K$ and the $K$-interpretation $\pi$, not all such $K$-interpretations are really meaningful for logic. Indeed the provenance value of complementary literals $R\overline{a}$ and $\neg R\overline{a}$ have to be related in a reasonable way, and as a consequence also the general provenance semirings of polynomials need to be modified. In the simplest case a $K$-interpretation defines a unique $\tau$-structure.

Definition 8**.**

A semiring interpretation $\pi:\operatorname{\mathrm{Lit}}_{A}(\tau)\rightarrow K$ is model-defining if for every atom $\varphi\in\operatorname{\mathrm{Atoms}}_{A}(\tau)$ one of $\pi(\varphi)$ and $\pi(\neg\varphi)$ is 0, and the other is $\neq 0$. It uniquely defines the $\tau$-structure ${\mathfrak{A}}_{\pi}$ that has universe $A$, and in which precisely those literals $\varphi$ are true for which $\pi(\varphi)\neq 0$.

Notice that if $K$ is not the Boolean semiring, then several different $K$-interpretations may define the same structure. Further, $K$-interpretations are interesting, and have a number of applications, also in cases where they do not specify a single model, see **[10*]** and the references given there. **Dual-Indeterminate Polynomials. *** Let $X,\overline{X}$ be two disjoint sets together with a one-to-one correspondence $X\leftrightarrow\overline{X}$. We denote by $p\in X$ and $\overline{p}\in\overline{X}$ two elements that are in this correspondence. We refer to the elements of $X\cup\overline{X}$ as provenance tokens and we shall use “positive” and “negative" tokens $p$ and $\overline{p}$ to annotate atoms $R\overline{a}\in\operatorname{\mathrm{Atoms}}_{A}(\tau)$ and negated atoms $\neg R\overline{a}\in\operatorname{\mathrm{NegAtoms}}_{A}(\tau)$, respectively. By convention, if we annotate $R(\overline{a})$ with $p$ then the “negative” token $\overline{p}$ can only be used to annotate $\neg R(\overline{a})$, and vice versa. We refer to $p$ and $\overline{p}$ as complementary tokens.

Definition 9**.**

The semiring ${\mathbb{N}}[X,\overline{X}]$ is the quotient of the semiring of polynomials ${\mathbb{N}}[X\cup\overline{X}]$ by the congruence generated by the equalities $p\cdot\overline{p}=0$ for all $p\in X$. This is the same as quotienting by the ideal generated by the polynomials $p\overline{p}$ for all $p\in X$. Observe that two polynomials $g,g^{\prime}\in{\mathbb{N}}[X\cup\overline{X}]$ are congruent if, and only if, they become identical after deleting from each of them the monomials that contain complementary tokens. Hence, the congruence classes in ${\mathbb{N}}[X,\overline{X}]$ are in one-to-one correspondence with the polynomials in ${\mathbb{N}}[X\cup\overline{X}]$ such that none of their monomials contain complementary tokens. We shall call these dual-indeterminate polynomials.

Note that ${\mathbb{N}}[X,\overline{X}]$ is $+$-positive and root-integral, but not positive, since it has divisors of [math]. Further, we have the following universality property:

Proposition 5.2**.**

Every function $f:X\cup\overline{X}\rightarrow K$ into any commutative semiring $K$ with the property that $f(p)\cdot f(\overline{p})=0$ for all $p\in X$ extends uniquely to a semiring homomorphism $h:{\mathbb{N}}[X,\overline{X}]\rightarrow K$ that coincides with $f$ on $X\cup\overline{X}$.

Definition 10**.**

A provenance-tracking interpretation is a mapping $\pi:\operatorname{\mathrm{Lit}}_{A}(\tau)\rightarrow X\cup\overline{X}\cup\{0,1\}$ such that $\pi(\operatorname{\mathrm{Atoms}}_{A}(\tau))\subseteq X\cup\{0,1\}$ and $\pi(\operatorname{\mathrm{NegAtoms}}_{A}(\tau))\subseteq\overline{X}\cup\{0,1\}$. Further, $\pi$ maps equalities and inequalities to their truth values 0 or 1.

The idea is that if $\pi$ annotates a positive or negative atom with a token, then we wish to track that literal through the model-checking computation. On the other hand annotating with [math] or $1$ is done when we do not track the literal, yet we need to recall whether it holds or not in the model. See **[10]** for more details and potential applications of provenance-tracking interpretations.

6 Semirings of dual-indeterminate power series and least fixed point solutions

It is known that the general properties of commutative semirings are not sufficient to deal with unbounded iterations as they occur in fixed-point logic. Even for Datalog, one of the simplest fixed-point formalism that omits the complications arising with universal quantification and negation, appropriate semirings have the additional property of being $\omega$-continuous. The general $\omega$-continuous provenance semirings are no longer semirings of polynomials, but semirings of formal power series, such as ${\mathbb{N}}^{\infty}[\![X]\!]$. We combine this here with our approach for dealing with negation by taking quotients with respect to the congruence generated by products $p\overline{p}$ of positive and negative provenance tokens. What we obtain are $\omega$-continuous provenance semirings of dual-indeterminate power series, such as ${\mathbb{N}}^{\infty}[\![X,\overline{X}]\!]$, as well as idempotent, absorptive, and other variants thereof. A semiring $K$ is naturally ordered if the relation $a\leq b:\Leftrightarrow\exists x(a+x=b)$ is a partial order. Note that this relation is reflexive and transitive in every semiring, but it is not always antisymmetric. An $\omega$-chain is a sequence $(a_{i})_{i\in\omega}$ with $a_{i}\leq a_{i+1}$ for all $i\in\omega$.

Definition 11**.**

A commutative semiring $K$ is $\omega$-continuous if it is naturally ordered and satisfies the following additional conditions:

• •

Every $\omega$-chain $(a_{i})_{i}\in\omega$ has a supremum $\sup_{i\in\omega}a_{i}$ in $K$. As a consequence, we have a well-defined infinite summation operator $\sum$, such that for every sequence $(b_{i})_{i\in\omega}$,

[TABLE]

• •

For every sequence $(a_{i})_{i\in\omega}$ in $K$, every $c\in K$, and every partition $(I_{j})_{j\in J}$ of $\omega$, we have that $c\cdot\sum_{i\in\omega}a_{i}=\sum_{i\in\omega}c\cdot a_{i}$ and $\sum_{j\in J}\sum_{i\in I_{j}}a_{i}=\sum_{i\in\omega}a_{i}$.

In an $\omega$-continuous semiring we further have the Kleene star operation, $a^{*}:=\sum_{i\in\omega}a^{i}=\sup_{i\in\omega}(1+a+a^{2}+\cdots+a^{i})$. A function $f:K\rightarrow K$ is $\omega$-continuous if, $\sup_{i\in\omega}f(a_{i})=f(\sup_{i\in\omega}a_{i})$ for every $\omega$-chain $(a_{i})_{i\in\omega}$. A consequence of the definition is that any function defined by a polynomial or a power series is $\omega$-continuous in each argument.

Definition 12**.**

Given a semiring $K$ and a finite set $X$ of indeterminates, we denote by $K[\![X]\!]$ the semiring of formal power series (i.e. possibly infinite sums of monomials) with coefficients in $K$ and indeterminates in $X$, with addition and multiplication defined in the obvious way. If $K$ is $\omega$-continuous and $|X|=n$, then every formal power series $f\in K[\![X]\!]$ induces a well-defined function $f:K^{n}\rightarrow K$ which is $\omega$-continuous in each argument. Further, if $K$ is $\omega$-continuous, then so is $K[\![X]\!]$ [16].

A system of power series with indeterminates $X_{1}\dots,X_{n}$ is a sequence $G=(g_{1}\dots g_{n})$ with $g_{i}\in K[\![X]\!]$ for each $i$. It induces a function $G:K^{n}\rightarrow K^{n}$ that is monotone in each argument. By Kleene’s Fixed-Point Theorem $G$ has a least fixed point $\operatorname{\mathbf{lfp}}G$ which coincides with the supremum of the Kleene approximants $G^{k}$, defined by $G^{0}=0$, $G^{k+1}=G(G^{k})$, i.e. $\operatorname{\mathbf{lfp}}G=\sup_{k\in\omega}G^{k}$. We also refer to $\operatorname{\mathbf{lfp}}G$ as the least fixed-point solution of the equation system

[TABLE]

*in short, $X=G(X)$. **Dual-indeterminate power series. *** Semirings $K[\![X]\!]$ of power series turn out to be appropriate as general provenance semirings for (not necessarily acyclic) reachability games, without any further structure on the terminal nodes, as well as for purely positive fixed-point formalisms, without negation even on the atomic level. However, as soon as we want to deal with fixed-point logics with (atomic) negation we again need to take quotients with respect to the congruence generated by an appropriate correspondence $X\leftrightarrow\overline{X}$ between positive and negative tokens (with the same conventions as in Definition 9).

Definition 13**.**

The semiring $K[\![X,\overline{X}]\!]$ is the quotient of the semiring of power series $K[\![X\cup\overline{X}]\!]$ by the congruence generated by the equalities $p\cdot\overline{p}=0$ for all $p\in X$. The congruence classes in $K[\![X,\overline{X}]\!]$ are in one-to-one correspondence with the power series in $K[\![X\cup\overline{X}]\!]$ such that none of their monomials contain complementary tokens. We call these dual-indeterminate power series.

Again we have a universality property.

Proposition 6.1**.**

Every function $f:X\cup\overline{X}\rightarrow K$ into an $\omega$-continuous semiring $K$ with the property that $f(p)\cdot f(\overline{p})=0$ for all $p\in X$ extends uniquely to an $\omega$-continuous semiring homomorphism $h:{\mathbb{N}}[\![X,\overline{X}]\!]\rightarrow K$ that coincides with $f$ on $X\cup\overline{X}$.

7 Provenance for reachability games with cycles

We now extend our provenance approach to games that admit infinite plays. We assume that the game graphs are finite, but no longer acyclic. Given a valuation $f_{\sigma}:T\rightarrow K$ in a semiring $K$ for the terminal nodes of a game graph ${\cal G}$, the rules defining valuations for the other nodes have now to be read as an equation system $(G_{\sigma})$ in indeterminates $X_{v}$ (for $v\in V$):

[TABLE]

If we assume that the underlying semiring $K$ is $\omega$-continuous, then such a system $(G_{\sigma})$ always has a least fixed-point solution $\operatorname{\mathbf{lfp}}G_{\sigma}$, which can be computed as the limit of its Kleene approximants $G^{n}:V\rightarrow K$, for $n\in\omega$. These Kleene approximants can be seen as valuations in the unravellings ${\cal G}^{n}$ of the game ${\cal G}$ up to $n$ moves, defined as follows. Recall that, for every game graph ${\cal G}=(V,V_{0},V_{1},T,E)$, and every initial position $v_{0}\in V$, we have the tree unraveling ${\cal T}({\cal G},v_{0})=(V^{\#},V_{0}^{\#},V_{1}^{\#},T^{\#},E^{\#})$ consisting of all finite paths from $v_{0}$, with the canonical projection $\rho:{\cal T}({\cal G},v_{0})\rightarrow{\cal G}$ that maps every path $\pi v$ to its end point $v$.

Definition 14**.**

Given ${\cal G}$ with basic valuations $f_{\sigma}:T\rightarrow K$ and $h_{\sigma}:E\rightarrow K\setminus\{0\}$ of the terminal positions and moves, the truncation ${\cal G}^{n}=(V^{(n)},V_{0}^{(n)},V_{1}^{(n)},T^{(n)},E^{(n)})$, for $n>0$, is the restriction of the union of the trees ${\cal T}({\cal G},v)$ (with $v\in V$) to paths of less than $n$ moves, and $\rho^{n}:{\cal G}^{n}\rightarrow{\cal G}$ is the restriction of the canonical homomorphism $\rho$ to ${\cal G}^{n}$. Notice that the truncation induces new terminal nodes:

[TABLE]

In ${\cal G}^{n}$, we define the basic valuation of the moves, $h_{\sigma}^{n}:E^{(n)}\rightarrow K\setminus\{0\}$, in the obvious way, by $h_{\sigma}^{n}(e):=h_{\sigma}(\rho^{n}(e))$. For the valuation of the terminal nodes $\pi v\in T^{(n)}$, we put $f^{n}_{\sigma}(\pi v)=f_{\sigma}(v)$ if $v\in T$, and $f^{n}_{\sigma}(\pi v)=0$ otherwise, i.e. if $\pi v$ is an initial segment of a play in ${\cal G}$, with $n-1$ moves, that has not reached a terminal position in $T$.

The games ${\cal G}^{n}$ are finite acyclic games, and the basic valuations extend to valuations $f^{n}_{\sigma}:V^{(n)}\rightarrow K$ for all nodes of ${\cal G}^{n}$. By induction, it readily follows that, for all nodes $v$ of ${\cal G}$, the Kleene approximants $G^{n}$ of $(G_{\sigma})$ coincide with these valuations.

Lemma 7.1**.**

For all $n$ and all positions $v$ of $G$, we have that $G^{n}(v)=f^{n}_{\sigma}(v)$.

We denote the strategy space of Player $\sigma$ from $v$ in ${\cal G}^{n}$ by $\mathrm{Strat}_{\sigma}^{(n)}(v)$. Since the games ${\cal G}^{n}$ are acyclic, Theorem 4.4 applies.

Lemma 7.2**.**

For every $n$, and every position $v$, $f^{n}_{\sigma}(v)=\sum_{{\cal T}\in\mathrm{Strat}_{\sigma}^{(n)}(v)}F({\cal T})$.

*Valuations of plays and strategies in games with cycles. *** To generalize Theorem 4.4 to reachability games with cycles, we first need to extend the valuations of plays and strategies to such games. As in Sect. 4 a finite play $x=v_{0}v_{1}\dots v_{m}$ in ${\cal G}$ from $v_{0}$ to a terminal node $v_{m}\in T$ gets the valuation $f_{\sigma}(x)=h_{\sigma}(v_{0}v_{1})\cdots h_{\sigma}(v_{m-1}v_{m})\cdot f_{\sigma}(v_{m})$. The provenance value of an infinite play is defined to be 0. For a strategy ${\cal S}\in\mathrm{Strat}_{\sigma}(v)$, we put $F({\cal S}):=0$ if ${\cal S}$ admits any infinite play. Hence a strategy ${\cal S}$ can have a non-zero provenance value only when it admits just finite plays. By König’s Lemma, it then admits only a finite number of plays, and putting, as in Sect. 4,

[TABLE]

is well-defined for such strategies, as the values $\#_{\cal S}(e)$ and $\#_{\cal S}(v)$ are finite, for all $e\in E$ and $v\in T$. Although the number of different strategies ${\cal S}\in\mathrm{Strat}_{\sigma}(v)$ may well be infinite, Theorem 4.4 generalizes to reachability games with cycles, with a proof based on Kleene’s fixed-point theorem, and the unravellings of ${\cal G}$ to finite acyclic games ${\cal G}^{n}$. Notice that every strategy ${\cal S}\in\mathrm{Strat}_{\sigma}(v)$ for the original game ${\cal G}$ induces, in every game ${\cal G}^{n}$, a strategy ${\cal S}^{(n)}\in\mathrm{Strat}^{(n)}_{\sigma}(v)$ for the game ${\cal G}_{n}$.

Lemma 7.3**.**

For every strategy ${\cal S}\in\mathrm{Strat}_{\sigma}(v)$ in ${\cal G}$ with $F(S)\neq 0$ there exists some $n_{\cal S}<\omega$ such that

• •

${\cal S}={\cal S}^{(n)}$* for all $n\geq n_{\cal S}$,*

• •

$F({\cal S}^{(m)})=0$* for all $m<n_{\cal S}$.*

Proof 7.4**.**

This readily follows from the fact that a strategy ${\cal S}$ with $F({\cal S})\neq 0$ admits only a finite number of plays, all of which are finite. Let $n_{\cal S}$ be the maximal length of these plays. Then, for $n\geq n_{\cal S}$, all plays in ${\cal S}$ are already contained in ${\cal S}^{(n)}$. For any $m<n_{s}$, the induced strategy admits an unfinished play, hence $F({\cal S}^{m})=0$.

Every strategy ${\cal T}\in\mathrm{Strat}_{\sigma}^{(n)}(v)$ can be obtained as the induced strategy of some ${\cal S}\in\mathrm{Strat}_{\sigma}(v)$, such that ${\cal T}={\cal S}^{(n)}$. In general ${\cal S}$ is not uniquely determined by ${\cal T}$ and $n$. Nevertheless, we have the following.

Lemma 7.5**.**

For every position $v$ of ${\cal G}$ and every $n<\omega$, we have that in ${\cal G}^{n}$,

[TABLE]

Proof 7.6**.**

If we have two strategies ${\cal S}_{1}\neq{\cal S}_{2}$ in $\mathrm{Strat}_{\sigma}(v)$ with ${\cal T}={\cal S}_{1}^{(n)}={\cal S}_{2}^{(n)}$, then ${\cal T}$ must contain an unfinished play (otherwise ${\cal T}={\cal S}_{1}={\cal S}_{2}$), which implies that $F({\cal T})=0$. Thus, although the strategy spaces $\mathrm{Strat}_{\sigma}(v)$ are in general infinite, whereas $\mathrm{Strat}^{(n)}_{\sigma}(v)$ is finite for each fixed $n$, those strategies that provide non-zero values to the sums are in one-to-one correspondence, and the two sums have the same value.

Putting these observations together, we obtain the desired generalization of Theorem 4.4.

Theorem 7.7**.**

For every game graph ${\cal G}$ with basic valuations $f_{\sigma}$ and $h_{\sigma}$ of the terminal positions and moves in an $\omega$-continuous semiring $K$, we have that, for every position $v$

[TABLE]

In the cases where $h(e)=1$ for all $e$, or where $K$ is multiplicatively idempotent, we further have that

[TABLE]

Proof 7.8**.**

By the lemmata above, we have that, for every $n<\omega$,

[TABLE]

Since, for every strategy ${\cal S}\in\mathrm{Strat}_{\sigma}(v)$ we have that $F({\cal S})=F({\cal S}^{n})$ for sufficiently large $n$, the result follows by taking suprema.

For the case of game valuations $f_{\sigma}:V\rightarrow{\mathbb{N}}[\![T]\!]$, given by the basic valuations $f_{\sigma}(t)=t$ for terminal positions $t\in T$ and $h_{\sigma}(vw)=1$ for all moves $(v,w)\in E$, we again get precise information about the number of strategies that a player has for a specific outcome. Indeed, $f_{\sigma}(v)$ is a (possibly) infinite sum of monomials $m\cdot t_{1}^{j_{1}}\dots t_{k}^{j_{k}}$

Corollary 7.9**.**

Let $f_{\sigma}:V\rightarrow{\mathbb{N}}[\![T]\!]$ be the valuation of Player $\sigma$ for the game ${\cal G}$ in ${\mathbb{N}}[\![T]\!]$. For every monomial $m\cdot t_{1}^{j_{1}}\dots t_{k}^{j_{k}}$ in $f_{\sigma}(v)$ (with $m\in{\mathbb{N}}$ and $j_{i}>0$) Player $\sigma$ has precisely $m$ strategies ${\cal S}$ from $v$ with the property that the set of possible outcomes for ${\cal S}$ is precisely $\{t_{1},\dots,t_{k}\}$, and precisely $j_{i}$ plays that are consistent with ${\cal S}$ have the outcome $t_{i}$.

Let ${\cal G}=(V,V_{0},V_{1},T,E)$ be a game with reachability objectives $T_{0},T_{1}$ for the two players, such that $T_{0}\cap T_{1}=\varnothing$. Let $W_{0},W_{1}\subseteq V$ be the winning regions for the two players, i.e., $W_{\sigma}$ is the set of those positions $v\in V$ such that Player $\sigma$ has a strategy from $v$ to force the play to $T_{\sigma}$. Note that $V$ is the disjoint union of the $W_{0}$, $W_{1}$ and $U$, the set of those positions from which none of the two players has a winning strategy. By Zermelo’s Theorem both players have strategies to guarantee that each play from $U$ will be at least a draw.

Corollary 7.10**.**

Let $f_{\sigma}:T\rightarrow K$ be a valuation of the terminal positions of ${\cal G}$ in an $\omega$-continuous semiring, with $f_{\sigma}(t)\neq 0$ if, and only if, $t\in T_{\sigma}$. The least fixed point solution of the equation system $F_{\sigma}$ extends this to a valuation $f_{\sigma}:V\rightarrow K$, with $f_{\sigma}(v)\neq 0$ if, and only if, $v\in W_{\sigma}$.

Notice that weakly contradictory valuations $f_{0}$ an $f_{1}$ on the terminal positions extend to weakly contradictory valuations on all positions. However, even valuations into $\omega$-continuous semirings that are strongly contradictory on the terminal positions, are in general only weakly contradictory on the set of all positions, unless $W_{0}\cup W_{1}=V$, since $f_{0}(U)=f_{1}(U)=0$.

Example 7.11**.**

We illustrate our findings by the following very simple example of a game where Player 0 moves from $v$, Player 1 moves from $w$, and $s$ and $t$ are terminal nodes.

s$$v$$w$$t

The corresponding equation system for Player 0 has the equations $X_{v}=s+X_{w}$ and $X_{w}=t\cdot X_{v}$. In ${\mathbb{N}}^{\infty}[\![s,t]\!]$ the least fixed-point solution is $f(v)=s\cdot(1+t+t^{2}\dots)$ and $f(w)=s\cdot(t+t^{2}+\dots)$. If we evaluate it for the reachability objectives $\{s\}$ and $\{t\}$, respectively, we obtain $f(v)[0,t]=f(w)[0,t]=0$ which illustrates that neither from $v$ nor from $w$, Player 0 has a strategy to reach $t$. On the other side, $f(v)[s,0]=s$ and $f(w)[s,0]=0$ which is consistent with the fact that Player 0 has a strategy to reach $s$ from $v$ but not from $w$. But the formal power series $f(v)$ and $f(w)$ reveal more information than that. For instance, the fact that $f(v)$ contains, for every $n$, the monomial $s\cdot t^{n}$ implies that Player 0 has precisely one strategy $S$ from $v$ that admits precisely $n+1$ consistent plays, one of which has outcome $s$ and the other $n$ have outcome $t$; this is the strategy where Player 0 moves from $v$ to $w$ the first $n$ times, and then to $s$. Notice that Player 0 also has one further strategy, namely the (positional) strategy to move always to $w$. However, this strategy does not guarantee that the play terminates and therefore has value 0, so it is not visible in the provenance values $f(v)$ and $f(w)$.

8 Provenance analysis for positive LFP

Least fixed-point logic, denoted LFP, extends first order logic by least and greatest fixed points of definable monotone operators on relations: If $\psi(R,\overline{x})$ is a formula of vocabulary $\tau\cup\{R\}$, in which the relational variable $R$ occurs only positively, and if $\overline{x}$ is a tuple of variables such that the length of $\overline{x}$ matches the arity of $R$, then $[\operatorname{\mathbf{lfp}}R\overline{x}\,.\,\psi](\overline{x})$ and $[\operatorname{\mathbf{gfp}}R\overline{x}\,.\,\psi](\overline{x})$ are also formulae (of vocabulary $\tau$). The semantics of these formulae is that $\overline{x}$ is contained in the least (respectively the greatest) fixed point of the update operator $F_{\psi}:R\mapsto\{\overline{a}:\psi(R,\overline{a})\}$. Due to the positivity of $R$ in $\psi$, any such operator $F_{\psi}$ is monotone and therefore has, by the Knaster-Tarski-Theorem, a least fixed point $\operatorname{\mathbf{lfp}}(F_{\psi})$ and a greatest fixed point $\operatorname{\mathbf{gfp}}(F_{\psi})$. See e.g. **[11]** for background on ${\rm LFP\ }$. Note that in formulae $[\operatorname{\mathbf{lfp}}R\overline{x}\,.\,\psi](\overline{x})$ one may allow $\psi$ to have other free variables besides $\overline{x}$; these are called parameters of the fixed-point formula. However, at the expense of increasing the arity of the fixed-point predicates and the number of variables one can always eliminate parameters. For the construction of model-checking games and also for provenance analysis it is convenient to assume that formulae are parameter-free. The duality between least and greatest fixed point implies that for any $\psi$,

[TABLE]

Using this duality together with de Morgan’s laws, every LFP-formula can be brought into negation normal form, where negation applies to atoms only. **The fragment of positive least fixed points. *** We denote by ${\rm posLFP}$ the fragment of LFP consisting of formulae in negation normal form such that all its fixed-point operators are least fixed-points. It is known that, on finite structures (but not in general), ${\rm posLFP}$ has the same expressive power as full LFP, and thus captures all polynomial-time computable properties of ordered finite structures **[11]** . An advantage of dealing with ${\rm posLFP}$, rather than full LFP, is that it admits much simpler model checking games. Indeed the appropriate games for LFP are parity games, whereas for ${\rm posLFP}$, reachability games are sufficient. This can be exploited to define provenance interpretations for fixed-point formulae, along the lines described in the previous section. Definition 7 of model checking games ${\cal G}(A,\psi)$ for $\psi\in{\rm FO}(\tau)$ extends to formulae $\psi(\overline{x})\in{\rm posLFP}(\tau)$ as follows: For every subformula of $\psi$ of form $\vartheta:=[\operatorname{\mathbf{lfp}}R\overline{x}\,.\,\varphi(R,\overline{x})](\overline{x})$ we add moves from positions $\vartheta(\overline{a})$ to $\varphi(\overline{a})$, and from positions $R\overline{a}$ to $\varphi(\overline{a})$ for every tuple $\overline{a}$. Since these moves are unique it makes no difference to which of the two players we assign the positions $\vartheta(\overline{a})$ and $R\overline{a}$. The resulting game graphs ${\cal G}(A,\psi)$ may contain cycles, but the set $T$ of terminal nodes is again a subset of $\operatorname{\mathrm{Lit}}_{A}(\tau)$. A $K$-interpretation $\pi:\operatorname{\mathrm{Lit}}_{A}(\tau)\rightarrow K$ into an $\omega$-continuous semiring thus provides a valuation of the terminal positions of the game graph ${\cal G}(A,\psi)$ for any $\psi\in{\rm posLFP}(\tau)$. By Theorem 7.10 this extends to a valuation $f_{0}:V\rightarrow K$ on the set $V$ of all positions $\varphi(\overline{a})$ of ${\cal G}(A,\psi)$, including position $\psi$ itself.*

Definition 15**.**

For any instantiated subformula $\varphi$ of a sentence $\psi\in{\rm posLFP}$, we define the provenance value $\pi[\![\varphi]\!]$ by its game valuation: $\pi[\![\varphi]\!]:=f_{0}(\varphi)$.

In particular, if $\pi$ is model-defining, then $f_{0}$ provides truth values for all fully instantiated subformula $\varphi$ of $\psi$ on the structure ${\mathfrak{A}}_{\pi}$ that $\pi$ describes. Indeed ${\mathfrak{A}}_{\pi}\models\varphi$ if, and only if, $\pi[\![\varphi]\!]\neq 0$, and in that case the value $\pi[\![\varphi]\!]$ gives us additional information, how and why $\varphi$ holds in ${\mathfrak{A}}$, for instance by information on the winning strategies that Verifier has available for establishing the truth of $\varphi$ in ${\mathfrak{A}}_{\pi}$. However, contrary to the case of first-order logic, in the case where ${\mathfrak{A}}_{\pi}\not\models\varphi$, and hence $\pi[\![\varphi]\!]=0$, we do not get additional information on the reasons why $\varphi$ is false. The possibility to move to $\neg\varphi$ (or more precisely, its negation normal form) and to do the provenance analysis for that formula, does not exist here since $\neg\varphi$ is not a formula of posLFP. In fact, the model checking-game for $\neg\varphi$ is not a reachability game, but a safety game. To deal with safety games and greatest fixed points we shall have to impose additional restrictions on the underlying semirings. We shall discuss this below. One can define provenance values for posLFP-sentences also directly by a fixed-point interpretation in $\omega$-commutative semirings. The goal is to extend, by induction over the syntax, a $K$-interpretation $\pi:\operatorname{\mathrm{Lit}}_{A}(\tau)\rightarrow K$ to valuations $\pi[\![\psi]\!]\in K$ for all sentences $\psi\in{\rm posLFP}(\tau\cup A)$. The rules for first-order operations are defined already, so we just have to consider sentences of form $\psi(\overline{a})=[\operatorname{\mathbf{lfp}}R\overline{x}.\varphi(R,\overline{x})](\overline{a})$, with $\varphi\in{\rm posLFP}(\tau\cup\{R\})$. If $R$ has arity $m$, then its $K$-interpretations of $A$ are functions $g:A^{m}\rightarrow K$. These functions are ordered, by $g\leq g^{\prime}$ if, and only if, $g(\overline{a})\leq g^{\prime}(\overline{a})$ for all $\overline{a}\in A^{m}$. Given a $K$-interpretation $\pi:\operatorname{\mathrm{Lit}}_{A}(\tau)\rightarrow K$, we denote by $\pi[R\mapsto g]$ the $K$-interpretation of $\operatorname{\mathrm{Lit}}_{A}(\tau)\cup\operatorname{\mathrm{Atoms}}_{A}(\{R\})$ obtained from $\pi$ by adding values $g(\overline{c})$ for the atoms $R\overline{c}$. (Notice that $R$ appears only positively in $\varphi$, so negated atoms are not needed). The formula $\varphi(R,\overline{x})$ now defines, together with $\pi$, a monotone update operator $F_{\pi}^{\varphi}$ on functions $g:A^{m}\rightarrow K$. More precisely, it maps $g$ to

[TABLE]

By Kleene’s Fixed-Point Theorem, the operator $F_{\pi}^{\varphi}$ has a least fixed point $\operatorname{\mathbf{lfp}}(F_{\pi}^{\varphi})$ which coincides with the limit of the sequence $(g^{n})_{n<\omega}$ with $g^{0}:=0$ and $g^{n+1}:=F^{\varphi}_{\pi}(g^{n})$, and which we may define as the provenance value of $[\operatorname{\mathbf{lfp}}R\overline{x}.\varphi(R,\overline{x})](\overline{a})$. The two definitions coincide.

Proposition 8.1**.**

For every formula $[\operatorname{\mathbf{lfp}}R\overline{x}.\varphi(R,\overline{x})]\in{\rm posLFP}$ and every $K$-interpretation $\pi:\operatorname{\mathrm{Lit}}_{A}(\tau)\rightarrow K$ into an $\omega$-continuous semiring, $\pi[\]\!]=\operatorname{\mathbf{lfp}}(F_{\pi}^{\varphi})(\overline{a}).$

The proof is a rather straightforward adaptation of the correctness proof for model checking games for LFP, see e.g. **[11, Chapter 3.3]**.

9 Beyond reachability: safety games and greatest fixed points

While the restriction of LFP to its positive fragment comes with no loss of expressive power (on finite structures) and while ${\rm posLFP}$ is sufficiently powerful to capture a number of interesting and relevant other fixed-point formalisms in computer science, it is nevertheless not really satisfactory. One reason is that the transformation from a fixed-point formula with non-atomic negation into one in ${\rm posLFP}$ is (contrary to transformations into negation normal form) not a simple syntactic translation. It goes through the Stage Comparison Theorem and can make a formula much longer and more complicated. Further, such transformations are not available for important fixed-point formalism such as the modal $\mu$-calculus, stratified Datalog, transitive closure logics, and even simple temporal languages such as CTL. On the game-theoretic side, reachability games are just the simplest kind of games on graphs, and in many applications players have different and more ambitious goals such as safety, Büchi, parity or Muller, objectives. It is thus an important and interesting challenge to lay the foundations of a provenance analysis for full LFP and infinite games with more general objectives, and to apply this approach to the numerous other fixed-point formalisms, in particular in databases and verification. We defer a detailed treatment of this to forthcoming work. Here we discuss some of the mathematical concepts and challenges that arise in this project, and apply them to the provenance of safety games. Recall that the computation of winning positions for safety objectives is a simple, but also in some sense universal, application of greatest fixed points. The first observation is that we need to impose additional requirements on the semirings that we consider. While $\omega$-continuous semirings are appropriate for a provenance analysis of least fixed points and reachability objectives, they are not always adequate for greatest fixed points. The property of $\omega$-continuity is not sufficient to guarantee the existence of greatest fixed points, and in cases where they exist they do not necessarily provide the information that we are interested in.

Example 9.1**.**

We consider the game graph

s$$w$$v$$z$$t

with associated equation system for Player 0 consisting of $X_{v}=X_{w}+X_{z}$, $X_{w}=f(s)\cdot X_{v}$, and $X_{z}=f(t)\cdot X_{v}$. The least fixed-point solution (in whatever semiring) has values $f(v)=f(w)=f(z)=0$ which reflects the fact that Player 0 has no strategy to guarantee a finite play. It is not difficult to see that in ${\mathbb{N}}^{\infty}[\![s,t]\!]$ this in fact the unique fixed point, hence in particular the greatest one, which however gives us no information about safety strategies. In ${\mathbb{N}}^{\infty}$ instead, under a valuation of the terminal nodes with $f(s)=a\neq 0$ and $f(t)=0$, we get the greatest fixed point $f(v)=f(w)=\infty$ and $f(z)=0$. In particular, greatest fixed-points do not specialise correctly from ${\mathbb{N}}^{\infty}[\![s,t]\!]$ to ${\mathbb{N}}^{\infty}$. We shall see below that get interesting information on safety strategies by provenance values in the absorptive semiring ${\mathbb{S}}^{\infty}[s,t]$.

To make sure that also greatest fixed points of polynomial equation systems exist, we shall require that our semirings are not just $\omega$-continuous, but also also $\omega$-co-continuous, i.e. that every descending $\omega$-chain $(a_{i})_{i\in\omega}$, with $a_{i+1}\leq a_{i}$ for all $i\in\omega$, has an infimum $\inf_{i\in\omega}a_{i}$ in $K$, which is compatible with the semiring operations in the sense that, for every $c\in K$,

[TABLE]

We call such semirings fully $\omega$-continuous. Our most important example of such a semiring is ${\mathbb{S}}^{\infty}[X]$, the semiring of generalized absorptive polynomials, that we are going to discuss next.

10 Absorptive semirings and generalized absorptive polynomials

Recall that a semiring $K$ is absorptive if $a+ab=a$ for all $a,b\in K$ which is equivalent to $1+a=1$ for all $a\in K$. Examples include the Viterbi semiring, the tropical semiring, min-max semirings, further the semiring ${\mathbb{S}}[X]$ of absorptive polynomials over $X$. Absorptive semirings are +-idempotent and naturally ordered, 1 is the top element, and multiplication decreases elements: $ab\leq b$. In particular, the powers of an element form a descending $\omega$-chain $1\geq a\geq a^{2}\geq\cdots$. If this chain has an infimum then we denote it by $a^{\infty}$. In the semiring ${\mathbb{S}}[X]$, the infima of descending $\omega$-chains $(x^{n})_{n<\omega}$ are always 0 and thus not very informative. We therefore complete ${\mathbb{S}}[X]$ to the semiring ${\mathbb{S}}^{\infty}[X]$ by admitting exponents in ${\mathbb{N}}^{\infty}$.

Definition 16**.**

Let $X$ be a finite set of provenance tokens. A monomial over $X$ with exponents from ${\mathbb{N}}^{\infty}$ is a function $m:X\rightarrow{\mathbb{N}}^{\infty}$. Informally, we write $m$ as $x_{1}^{m(x_{1})}\cdots x_{n}^{m(x_{n})}$. Monomial multiplication adds the exponents. Observe also that $x^{\infty}\cdot x^{n}=x^{\infty}$. For any two monomials, $m_{1},m_{2}$ we say that that $m_{2}$ absorbs $m_{1}$ if $m_{2}$ has smaller exponents than $m_{1}$. Formally, $m_{1}\preceq m_{2}$ if, and only if, $m_{1}(x)\geq m_{2}(x)$ for all $x\in X$. Since monomials are functions, this is the pointwise partial order given by the order on ${\mathbb{N}}^{\infty}$.

Because ${\mathbb{N}}^{\infty}$ is a lattice (with top and bottom) the monomials also inherit a lattice structure. The set of all monomials is, of course, infinite. However, it has some crucial finiteness properties.

Proposition 10.1**.**

Every ascending chain and every antichain of monomials is finite.

Proof 10.2**.**

Clearly $({\mathbb{N}}^{\infty},\leq)$ is a well-order. For any finite set $X$, the set of monomials $m:X\rightarrow{\mathbb{N}}^{\infty}$ with the reverse order of the absorption order is isomorphic to $({\mathbb{N}}^{\infty})^{k}$ with $k=|X|$ and with the component-wise order inherited from $({\mathbb{N}}^{\infty},\leq)$. This is a well-quasi-order and therefore has no infinite descending chains and no infinite antichains. This implies that in the set of monomials over $X$ with the absorption order, all ascending chains and all antichains are finite.

Definition 17**.**

We define ${\mathbb{S}}^{\infty}[X]$ as the set of antichains of monomials with indeterminates from $X$ and exponents in ${\mathbb{N}}^{\infty}$. Writing an antichain as a (formal) sum of its monomials we identify it with a polynomial with coefficients 0 or 1, and call these generalized absorptive polynomials. We define polynomial addition and multiplication as usual, except that for coefficients 1+1=1, and that we keep only the maximal monomials in the result. The empty antichain corresponds to the 0 polynomial. The 1 polynomial consists of just the monomial in which every indeterminate has exponent 0.

Proposition 10.3**.**

$({\mathbb{S}}^{\infty}[X],+,\cdot,0,1)$* is an absorptive commutative semiring. Further it is a complete lattice wrt. to the natural order, which is fully $\omega$-continuous and moreover completely distributive.*

As a consequence, we can compute not only least fixed point solutions for systems of polynomial equations but also greatest fixed points. In contrast to other semirings with such properties, such as for instance the Viterbi semiring, ${\mathbb{S}}^{\infty}[X]$ has one further crucial property. It is chain-positive which means that the infimum of every chain of non-zero elements is also non-zero. As in other semirings of polynomials and power series we can also here take pairs of positive and negative indeterminates, with a correspondence $X\leftrightarrow\overline{X}$ and build the quotient with respect to the congruence generated by the equation $x\cdot\overline{x}=0$. We thus obtain a new semiring ${\mathbb{S}}^{\infty}[X,\overline{X}]$ which provides a natural framework for a provenance analysis for full LFP and other fixed point calculi. We shall develop this in forthcoming work. Here we use the semiring ${\mathbb{S}}^{\infty}[T]$ to describe a provenance analysis for safety games where $T$ is the set of terminal positions of the given game graph.

11 Absorption among strategies

Definition 18**.**

Let ${\cal G}=(V,V_{0},V_{1},T,E)$ be a finite game graph, and $v\in V$. For two strategies ${\cal S},{\cal S}^{\prime}\in\mathrm{Strat}_{\sigma}(v)$, we say that ${\cal S}$ absorbs ${\cal S}^{\prime}$ (in symbols ${\cal S}\succeq_{a}{\cal S}^{\prime}$) if

• •

*for all $t\in T$, ${\cal S}$ admits at most as many plays with outcome $t$ as ${\cal S}^{\prime}$ does, and *

• •

if ${\cal S}$ admits an infinite play, then so does ${\cal S}^{\prime}$.

We call ${\cal S}$ absorption-dominant if it is maximal with respect to $\succeq_{a}$.

Absorption-dominant strategies are interesting both for games in general and for logic because they can win “with minimal effort”. As a simple example, consider a model checking game for a formula $\varphi\lor(\varphi\land\psi)$. The Verifier can either establish $\varphi$ or $\varphi\land\psi$, but any strategy that establishes the truth of $\varphi\land\psi$ will have more plays and more outcomes than one that proves just $\varphi$, and will thus be absorbed by it. The absorption-dominant strategies for $\varphi\lor(\varphi\land\psi)$ are thus precisely the absorption-dominant strategies for $\varphi$. Notice however that, despite this minimality, absorption dominant strategies need not be positional, not even in acyclic games.

Example 11.1**.**

Consider the game

u$$v$$w$$z$$s$$t

There are four strategies in $\mathrm{Strat}_{0}(u)$ with provenance values $s^{2}$, $st$, $st$, and $t^{2}$. The positional ones are those with values $s^{2}$ and $t^{2}$, but all four strategies are absorption-dominant.

However, absorption-dominant strategies are weakly positional in the sense that if a node is reached several times during the same play, then, without loss of strategic power, the player can always make the same choice at that node. Absorption among strategies makes sense for both acyclic and cyclic games. In acyclic games, absorption-dominant strategies are described by provenance polynomials in ${\mathbb{S}}[T]$ (with only finite exponents). But they are even more interesting for the analysis of reachability and safety games that admit infinite plays. The fundamental difference between valuations for reachability and safety strategies concerns the valuations of infinite plays. If, as we assume here, reachability and safety goals are defined for terminal nodes, then an infinite play is losing for every reachability objective but winning for every safety objective. As a consequence, the strategies ${\cal S}\in\mathrm{Strat}_{\sigma}(v)$ that enforce all plays to be non-terminating absorb all other strategies in $\mathrm{Strat}_{\sigma}(v)$ that admit at least one infinite play. We thus extend the valuations of plays in a game ${\cal G}$ (with finite game graph that may contain cycles) to two different valuation function $f_{\sigma}^{\mu}$ and $f_{\sigma}^{\nu}$. For simplicity, we assume trivial valuations on the edges, so for a finite play $x$ ending in $t$, we just put $f_{\sigma}^{\mu}(x)=f_{\sigma}^{\nu}(x)=f_{\sigma}(t)$ but if $x$ is an infinite play, we put $f_{\sigma}^{\mu}(x)=0$ and $f_{\sigma}^{\nu}(x)=1$. A strategy ${\cal S}\in\mathrm{Strat}_{\sigma}(v)$ may well admit an infinite set of plays. Taking the semiring ${\mathbb{S}}^{\infty}[T]$ with the basic valuation $f_{\sigma}(t):=t$ for the terminal nodes, strategies are described by monomials (or 0), and we put

[TABLE]

We extend the absorption order $\succeq$ on monomials by $m\succeq 0$ for all $m$.

Lemma 11.2**.**

Let ${\cal G}$ be any finite game graph, with valuations of strategies in ${\mathbb{S}}^{\infty}[T]$ induced by $f_{\sigma}(t)=t$ for all $t\in T$. For all strategies ${\cal S},{\cal S}^{\prime}\in\mathrm{Strat}_{\sigma}(v)$ we have,

• •

$0\neq F^{\nu}({\cal S})\succeq F^{\mu}({\cal S})\neq 1$.

• •

$F^{\mu}({\cal S})=0$* if, and only if, ${\cal S}$ admits an infinite play. Otherwise $F^{\mu}({\cal S})=F^{\nu}({\cal S})$.*

• •

$F^{\nu}({\cal S})=1$* if, and only if, ${\cal S}$ admits only infinite plays.*

• •

${\cal S}$* absorbs ${\cal S}^{\prime}$ if, and only if, both $F^{\nu}({\cal S})\succeq F^{\nu}({\cal S}^{\prime})$ and $F^{\mu}({\cal S})\succeq F^{\mu}({\cal S}^{\prime})$.*

Proof 11.3**.**

Only the last item requires proof. Suppose that ${\cal S}$ absorbs ${\cal S}^{\prime}$. If ${\cal S}$ admits only finite plays, then $F^{\mu}({\cal S})=F^{\nu}({\cal S})\succeq F^{\nu}({\cal S}^{\prime})\succeq F^{\mu}({\cal S}^{\prime})$. If ${\cal S}$ admits an infinite play, then so does ${\cal S}^{\prime}$ and $F^{\nu}({\cal S})\succeq F^{\nu}({\cal S}^{\prime})\succeq F^{\mu}({\cal S}^{\prime})=F^{\mu}({\cal S})=0$. In both cases, $F^{\nu}({\cal S})\succeq F^{\nu}({\cal S}^{\prime})$ and $F^{\mu}({\cal S})\succeq F^{\mu}({\cal S}^{\prime})$. Conversely, assume that ${\cal S}$ does not absorb ${\cal S}^{\prime}$. Then either there is a terminal $t$ such that ${\cal S}$ admits more plays with outcome $t$ than ${\cal S}^{\prime}$ does, or ${\cal S}$ admits an infinite play, but ${\cal S}^{\prime}$ does not. In the first case, $F^{\nu}({\cal S})\not\succeq F^{\nu}({\cal S}^{\prime})$ and in the second case $0=F^{\mu}({\cal S})\not\succeq F^{\mu}({\cal S}^{\prime})\neq 0$.

Example 11.4**.**

We return to the game described in Example 7.11

s$$v$$w$$t

with equation system $G_{0}$ consisting of $X_{v}=s+X_{w}$ and $X_{w}=t\cdot X_{v}$. In ${\mathbb{N}}^{\infty}[\![s,t]\!]$ the least fixed-point solution is $f(v)=s\cdot(1+t+t^{2}\dots)$ and $f(w)=s\cdot(t+t^{2}+\dots)$. In ${\mathbb{S}}^{\infty}[s,t]$ the least fixed-point solution $f^{\mu}=\operatorname{\mathbf{lfp}}G_{0}$ has values $f^{\mu}(v)=s$ and $f^{\mu}(w)=st$, which describes the possible outcomes of the unique absorption-dominant dominant strategy that enforces finite plays. The only other absorption-dominant strategy (moving from $v$ to $w$) has value 0 because it admits an infinite play. However, the greatest fixed-point solution $f^{\nu}=\operatorname{\mathbf{gfp}}G_{0}$ of this equation system in ${\mathbb{S}}^{\infty}[s,t]$ has values $f^{\nu}(v)=s+t^{\infty}$ and $f^{\nu}(w)=st+t^{\infty}$. Here this second strategy has value $t^{\infty}$ since it admits infinitely many plays ending in $t$ (and one infinite play with value 1).

Theorem 11.5**.**

Let ${\cal G}=(V,V_{0},V_{1},T,E)$ be a game graph and let $G_{\sigma}$ be the associated equation system for Player $\sigma$. In the semiring ${\mathbb{S}}^{\infty}[T]$ this system has least and greatest fixed point solutions $\operatorname{\mathbf{lfp}}G_{\sigma}$ and $\operatorname{\mathbf{gfp}}G_{\sigma}$ with

[TABLE]

The values of these sums do not change if we restrict them to the absorption-dominant strategies.

Proof 11.6**.**

Since ${\mathbb{S}}^{\infty}[T]$ is $\omega$-continuous, the claim for $(\operatorname{\mathbf{lfp}}G_{\sigma})$ follows from Theorem 7.7. For the greatest fixed-point solution we use that ${\mathbb{S}}^{\infty}[T]$ is also $\omega$-co-continuous and has the structure of a complete lattice. Thus, $(\operatorname{\mathbf{gfp}}G_{\sigma})$ is the limit of the descending chain $(G^{n})_{n<\omega}$ of approximants starting with $G^{0}=1$, and $G^{n+1}$ is defined by applying the equation system to $G^{n}:V\rightarrow{\mathbb{S}}^{\infty}[T]$. As in the proof of Theorem 7.7 we argue with the unfoldings ${\cal G}^{n}$ of ${\cal G}$ up to $n-1$ moves, but we now put $f^{n}_{\sigma}(\pi v)=1$ for the final node of an ‘unfinished’ play, i.e. with $|\pi|=n-1$ and $v\in V\setminus T$. The valuations $f^{n}_{\sigma}$ extend to all nodes of the (acyclic) game ${\cal G}^{n}$, and again, coincide with the Kleene approximants $G^{n}$: for every $n$ and every $v$ we have that $G^{n}(v)=f_{\sigma}^{n}(v)$. The different valuation of the terminal nodes in ${\cal G}^{n}$ also has the effect that any ${\cal T}\in\mathrm{Strat}^{(n)}_{\sigma}(v)$ we have that $F({\cal T})=\prod_{t\in T}t^{\#_{\cal T}(t)}$, which is a monomial with only finite exponents. Since ${\cal G}^{n}$ is acyclic

[TABLE]

Every strategy ${\cal S}\in\mathrm{Strat}_{\sigma}(v)$ for the original game ${\cal G}$ induces for each game ${\cal G}^{n}$ a strategy ${\cal S}^{(n)})$. Conversely, every strategy ${\cal T}\in\mathrm{Strat}^{(n)}_{\sigma}(v)$ is induced by at least one strategy ${\cal S}\in\mathrm{Strat}_{\sigma}(v)$. Since the semiring ${\mathbb{S}}^{\infty}[T]$ is idempotent, we have that, for every $n<\omega$,

[TABLE]

As graphs, the sequence $({\cal S}^{(n)})_{n\in\omega}$ of induced strategies is increasing, i.e. ${\cal S}^{(1)}\subseteq S^{(2)}\subseteq\cdots$, but their values in ${\mathbb{S}}^{\infty}[T]$ are decreasing, i.e., $F({\cal S}^{(1)})\succeq F(S^{(2)})\subseteq\cdots$. Further, $F^{\nu}({\cal S})=\prod_{t\in T}t^{\#_{\cal S}(t)}$ with exponents $\#_{\cal S}(t)\in{\mathbb{N}}^{\infty}$ and the corresponding exponents in the monomial $F({\cal S}^{(n)}$ tell us how often a terminal position $t\in T$ has been reached by ${\cal S}$ after $n-1$ moves. In particular,

[TABLE]

It is clear that these limits commute with summation over stratgies, so we have that

[TABLE]

Putting everything together we get that

[TABLE]

These least and greatest fixed points give precise descriptions of the absorption-dominant reachability and safety strategies of the players for each position of the game.

Example 11.7**.**

We return to the Example 9.1:

s$$w$$v$$z$$t

Recall that the associated equation system for Player 0 has the equations $X_{v}=X_{w}+X_{z}$, $X_{w}=f(s)\cdot X_{v}$, and $X_{z}=f(t)\cdot X_{v}$. The greatest fixed-point solution in ${\mathbb{S}}^{\infty}[s,t]$, computed by iterating from the top element $f=1$ results in $f^{\nu}(v)=s^{\infty}+t^{\infty}$, $f^{\nu}(w)=s^{\infty}+st^{\infty}$, and $f^{\nu}(z)=s^{\infty}t+t^{\infty}$. Notice that indeed, $f^{\nu}(v)=f^{\nu}(w)+f^{\nu}(z)$ because $st^{\infty}$ is absorbed by $t^{\infty}$, and $s^{\infty}t$ by $s^{\infty}$. The greatest fixed point solution indicates that Player 0 has two absorptive strategies (move always to $w$ or move always to $z$), and gives, for each of the terminal nodes $s$ and $t$ the number of plays ending in that node that the strategy admits. For instance, if the safety objective requires to avoid $t$, then $v$ and $w$ the strategy moving to $w$ has infinitely many winning plays ending in $s$ (and one nonterminating play with value 1), but since $f(z)[s,0]=0$, Player 0 has no safety strategy from $z$ that avoids $t$.

12 Outlook

*In this paper we have extended the semiring framework for provenance analysis by new elements, so that it can be applied to logics with negation, in particular first-order logic and fixed-point logics, and to an analysis of games that provides detailed information about the number and properties of the strategies of the players. Our treatment of negation is based on transformations to negation normal form and the use of newly introduced semirings of dual-indeterminate polynomials and dual-indeterminate power series. In particular, $\omega$-continuous semirings ${\mathbb{N}}^{\infty}[\![X,\overline{X}]$ of dual-indeterminate power series povide an adequate general framework for logics with least fixed points, such as ${\rm posLFP}$ (and Datalog) and the semiring of absorptive generalized dual-indeterminate polynomials ${\mathbb{S}}^{\infty}[\![X,\overline{X}]$ permits an adequate treatment of greatest fixed points. We have thus laid foundations for a provenance analysis of general fixed-point logics, and we are currently applying this also to modal, temporal, and dynamic logics. On the level of games, we have seen that provenance valuations in $\omega$-continuous and absorptive semirings give us very detailed information about strategies for possibly infinite games with reachability and safety objectives. We are currently expanding this to games with more complicated objectives, such as Büchi, Co-Büchi or parity games. Since these objectives do no longer depend on terminal nodes but on the data occurring in infinite plays, a somewhat different framework has to be used, depending for instance on basic valuations of the edges of the game graph. *