# Semiring Provenance for Büchi Games:
Strategy Analysis with Absorptive Polynomials

Erich Grädel RWTH Aachen University
Aachen, Germany<EMAIL_ADDRESS>RWTH Aachen University
Aachen, GermanyRWTH Aachen University
Aachen, Germany Niels Lücking RWTH Aachen University
Aachen, Germany<EMAIL_ADDRESS>RWTH Aachen University
Aachen, Germany Matthias Naaf RWTH Aachen University
Aachen, Germany<EMAIL_ADDRESS>
###### Abstract

This paper presents a case study for the application of semiring semantics for
fixed-point formulae to the analysis of strategies in Büchi games. Semiring
semantics generalizes the classical Boolean semantics by permitting multiple
truth values from certain semirings. Evaluating the fixed-point formula that
defines the winning region in a given game in an appropriate semiring of
polynomials provides not only the Boolean information on _who_ wins, but also
tells us _how_ they win and _which strategies_ they might use. This is well-
understood for reachability games, where the winning region is definable as a
least fixed point. The case of Büchi games is of special interest, not only
due to their practical importance, but also because it is the simplest case
where the fixed-point definition involves a genuine alternation of a greatest
and a least fixed point.

We show that, in a precise sense, semiring semantics provide information about
all _absorption-dominant_ strategies – strategies that win with minimal
effort, and we discuss how these relate to positional and the more general
_persistent_ strategies. This information enables applications such as game
synthesis or determining minimal modifications to the game needed to change
its outcome.

Due to space reasons, several proofs have been omitted and can be found in the
full version [15].

##  1 Introduction

Two-player games on finite graphs which admit infinite plays are of
fundamental importance in many areas of logic and computer science, especially
in the formal analysis of reactive systems, where they model the non-
terminating interaction between a system and its environment. In such a game,
the _objective_ or _winning condition_ of the player who represents the system
specifies the desired set of behaviours of the system. The most basic classes
of such objectives are _reachability_ and _safety_ objectives defined by a set
of states (positions) that the player should reach, or avoid. We can assume,
without loss of generality, that even though infinite plays are possible in a
game with reachability or safety objectives, they are all won by the same
player.

Games with genuine and non-trivial winning conditions for infinite plays are
harder to analyse; they include games with arbitrary $\omega$-regular
objectives, such as liveness, Muller, Streett-Rabin, or parity objectives, and
many others. The goal of this paper is to provide a case study of a recent
method for strategy analysis, based on semiring semantics, and we would like
to explore its potential for providing detailed information about strategies
in genuinely infinite games. One of the simplest class of games with a non-
trivial winning condition for the infinite plays are games with Büchi
objectives, which require that a specific target set $F$ of states is reached
infinitely often during the play (see e.g. [18] for background). Büchi games,
as well as some of their straightforward generalisations, have many
applications in formal methods, and efficient algorithms for solving them have
been studied thoroughly (see e.g. [5, 6, 7]). They are also of interest from
the points of view of topology and logic, because they are among the simplest
games where the set of winning plays is neither open nor closed, and where
logical definition of the winning region requires a genuine alternation of a
greatest and a least fixed point (see Sect. 5).

Strategies in infinite games can be very complicated because, in principle,
they may depend on the entire history of a play. Thus, there exist uncountably
many different strategies, even on a finite game graph. Fortunately, in many
cases and in particular for Büchi games, simple strategies are sufficient to
win. A fundamental result in this context is the positional determinacy of
parity games (of which Büchi games are a special case), saying that from each
position, one of the two players has a _positional winning strategy_ , i.e. a
winning strategy that only depends on the current position and not on the
history of the play. A positional strategy can be viewed as a subgraph of the
game graph, and can therefore be represented in a compact way. As a
consequence, the algorithmic analysis of Büchi games has concentrated almost
exclusively on the positional strategies. Here we extend this point of view
somewhat and take also other kinds of simple strategies into account.
Specifically, we are interested in _absorption-dominant_ winning strategies
[17] which are strategies without redundant moves; this means that taking away
anything, in the sense of demanding that some specific move is played less
often, makes the strategy non-winning. Another way to distinguish positional
strategies from absorption-dominant ones concerns their minimisation
properties: while positional strategies minimize the _set_ of moves that they
use, absorption-dominant strategies take multiplicities into account and
minimize the _multiset_ of moves. A further interesting class are the
_persistent_ strategies [21], which are positional in each individual play but
not necessarily across distinct plays. We shall study the relationship between
these different classes of simple strategies, and prove that every positional
strategy is absorption-dominant and every absorption-dominant strategy is
persistent, and that these inclusions are strict.

The specific method for strategy analysis that we want to apply to Büchi games
in this paper is based on the logical definability of the winning positions by
a formula in the fixed-point logic LFP, and on the semiring semantics for LFP
developed in [10]. In the classical Boolean semantics, a model
${\mathfrak{A}}$ of a formula $\varphi$ assigns to each (instantiated) literal
a Boolean value. ${\mathbb{K}}$-interpretations $\pi$, for a suitable semiring
${\mathbb{K}}$, generalize this by assigning to each such literal a semiring
value from ${\mathbb{K}}$. We then interpret $0$ as _false_ and all other
semiring values as _nuances of true_ that provide additional information,
depending on the semiring: For example, the Boolean semiring
$\mathbb{B}=(\\{0,1\\},\lor,\land,0,1)$ corresponds to Boolean semantics, the
Viterbi-semiring $\mathbb{V}=([0,1],\max,\cdot,0,1)$ can model _confidence_
scores, the tropical semiring
$\mathbb{T}=(\mathbb{R}_{\\_}{+}^{\infty},\min,+,\infty,0)$ is used for cost
analysis, and min-max-semirings $(A,\max,\min,a,b)$ for a totally ordered set
$(A,<)$ can model different access levels. Most importantly, semirings of
polynomials, such as ${\mathbb{N}}[X]$, allow us to _track_ certain literals
by mapping them to different indeterminates. The overall value of the formula
is then a polynomial that describes precisely what combinations of literals
prove the truth of the formula. Semiring semantics has been studied for
various logics [2, 8, 9, 10, 16], following the successful development of
semiring provenance in database theory and related fields (see e.g.[11, 13,
19, 20, 24, 25, 26]). While semiring provenance analysis for database queries
had largely been confined to positive query languages such as conjunctive
queries, positive relational algebra, and Datalog, the generalisation to
logics such as first-order logic FO and least fixed-point logic LFP –
featuring full negation and unrestricted interaction between least and
greatest fixed points – poses non-trivial mathematical challenges and requires
new algebraic constructions. Specifically, it has turned out that appropriate
semirings for LFP should be absorptive and fully continuous. Fortunately, this
is the case for most of the important application semirings such as
$\mathbb{V},\mathbb{T}$ or min-max-semirings, but not for the natural semiring
${\mathbb{N}}$, or the general provenance semirings of polynomials or formal
power series, ${\mathbb{N}}[X]$ and ${\mathbb{N}}^{\infty}[\\![X]\\!]$.
Instead, we rely on semirings ${\mathbb{S}}^{\infty}[X]$ of _generalized
absorptive polynomials_ , which we explain in Sect. 4.1, and which are the
_universal_ absorptive, fully-continuous semirings, in the sense that every
mapping $h\colon X\to{\mathbb{K}}$ into an absorptive, fully-continuous
semiring ${\mathbb{K}}$ uniquely extends to a fully-continuous semiring
homomorphism $h\colon{\mathbb{S}}^{\infty}[X]\to{\mathbb{K}}$, see Theorem 17.
From valuations of fixed-point formulae in such semirings we thus can derive
detailed insights into why the formula holds – and by applying this to the
fixed-point definition of winning positions in Büchi games we obtain compact
descriptions of winning strategies, in particular of all positional strategies
and all absorption-dominant ones.

After an analysis of simple winning strategies in Büchi games, and a short
introduction to semiring semantics for fixed-point logic, we shall study the
semiring valuations of the particular LFP-formula $\mathsf{win}_{0}(x)$ that
defines the winning region for Player 0 in Büchi games. Given that the
objective of Player 0 is to ensure that the play hits the target set $F$
infinitely often, we may informally describe their winning region as the
_largest_ set $Y$ of positions from which they can enforce a (further) visit
to $Y\cap F$ after $k\geq 1$ moves. On the other side the set of positions
from which Player 0 can enforce a visit to a target set is the _smallest_ set
of positions that either are already in the target set, or from which Player 0
can enforce the play to come closer to it. Thus, the winning region of Player
0 can be described as a greatest fixed point inside of which there is a least
fixed point, and it is well-known that this fixed-point alternation in the
treatment of Büchi objectives cannot be avoided, see e.g. [3].

The theoretical underpinning of our method is a Sum-of-Strategies-Theorem,
saying that for any position $v$ in a Büchi game, the valuation of the LFP-
formula $\mathsf{win}_{0}(v)$ in an absorptive, fully-continuous semiring
coincides with the sum of the valuations of all absorption-dominant winning
strategies from $v$. The proof is somewhat involved and requires non-trivial
machinery; details are given in the full version of this paper [15]. Besides
being of theoretical interest, this result allows to study a number of
interesting questions concerning the available winning strategies in a given
Büchi game:

Strategy tracking. Introducing indeterminates for all edges in a fixed Büchi
game $\mathsf{G}$, the semiring value
$\pi_{\text{strat}}[\\![\mathsf{win}_{0}(v)]\\!]$ for a position $v$ is a
polynomial whose monomials are concise descriptions of all absorption-dominant
strategies. From these monomials we can derive whether Player 0 wins from $v$
(if there are any monomials) and which edges are used by each absorption-
dominant strategy, and how often they appear in the strategy tree. In
particular, we can immediately identify and count positional strategies from
the polynomial. Going further, we can answer questions such as: can Player 0
still win if we remove edge $e$, or several edges at once? Can they still win
if edge $e$ may only be used finitely often in each play?

Repairing a game. Instead of analysing strategies in a fixed game, we may also
reason about modifications or synthesis of (parts of) the game. For example,
assuming Player 0 loses from $v$, what are minimal modifications to the game
that would let Player 0 win from $v$? To answer such questions we have to take
into account also negative information (i.e., absent edges in the graph), so
as to find a minimal repair consisting of both moves to delete and moves to
add. Algebraically, this requires to extend our semirings by dual-
indeterminates, which leads to quotient semirings
${\mathbb{S}}^{\infty}[X,\overline{X}]$ by a construction that has been used
before in [16, 28, 10] to deal with semiring semantics for negation. We
illustrate with the example of minimal repairs that we can indeed derive the
desired information from valuations in such semirings.

##  2 Büchi Games and Strategies

A Büchi game is given by a tuple $\mathsf{G}=(V,V_{\\_}0,V_{\\_}1,E,F)$ where
$V$ is a set of positions (here assumed to be finite), with a disjoint
decomposition $V=V_{\\_}0\dot{\cup}V_{\\_}1$ into positions of Player 0 and
positions of Player 1. The relation $E\subseteq V\times V$ specifies the
possible moves, and the target set $F\subseteq V$ describes the winning
condition. We denote the set of immediate successors of a position $v$ by
$vE:=\\{w\mid vw\in E\\}$ and require that $vE\neq\varnothing$ for all $v$. A
play from an initial position $v_{\\_}0$ is an infinite path
$v_{\\_}0v_{\\_}1v_{\\_}2\dots$ through $\mathsf{G}$ where the successor
$v_{\\_}{i+1}\in v_{\\_}iE$ is chosen by Player 0 if $v_{\\_}i\in V_{\\_}0$
and by Player 1 if $v_{\\_}1\in V_{\\_}1$. A play
$v_{\\_}0v_{\\_}1v_{\\_}2\dots$ is won by Player 0 if $v_{\\_}i\in F$ for
infinitely many $i<\omega$, otherwise it is won by Player 1. The winning
region of Player $\sigma$ is the set of those positions $v\in V$ such that
Player $\sigma$ has a winning strategy from $v$, i.e. a strategy that
guarantees them a win, no matter what the opponent does.

A strategy for Player $\sigma$ in $\mathsf{G}=(V,V_{\\_}0,V_{\\_}1,E,F)$ can
be represented in different ways, for instance as a function $f\colon
V^{*}V_{\\_}\sigma\to V$ that assigns a next position to each partial play
ending in a position of Player $\sigma$, or simply $f\colon V_{\\_}\sigma\to
V$ if the strategy is positional. Here we follow an alternative approach and
represent strategies as trees, comprised of all plays that are consistent with
the strategy (see, e.g., [17]). For simplicity, we only consider strategies of
Player 0, so unless mentioned otherwise, “strategy” always refers to a
strategy for Player 0.

######  Definition 1.

Given a Büchi game $\mathsf{G}=(V,V_{\\_}0,V_{\\_}1,E,F)$, the _tree
unraveling_ from $v_{\\_}0$ is the tree ${\mathsf{T}}(\mathsf{G},v_{\\_}0)$
whose nodes are all finite paths $\rho$ from $v_{\\_}0$ in $\mathsf{G}$ and
whose edges are $\rho\to\rho v$ for $v\in V$. We often write a node of
${\mathsf{T}}(\mathsf{G},v_{\\_}0)$ as $\rho v$ to indicate a finite path
ending in $v\in V$. The length of $\rho$ is denoted by $|\rho|$ and we write
$\rho\rho^{\prime}$ if $\rho$ is a (not necessarily strict) prefix of
$\rho^{\prime}$.

Strategies can then be defined as subtrees of the tree unraveling, which
allows for a more visual way to reason about strategies. An important detail
is that the strategy tree only contains positions (and thus choices for these
positions) that are reachable when following the strategy. Moreover, we only
consider finite Büchi games and hence the tree unraveling and all strategies
are finitely branching.

######  Definition 2.

A _strategy_ $\mathsf{S}$ (of Player 0) from $v_{\\_}0$ in $\mathsf{G}$ is a
subtree of ${\mathsf{T}}(\mathsf{G},v_{\\_}0)$ induced by a node set $W$
satisfying the following conditions:
\- If $\rho v\in W$, then also $\rho\in W$ (prefix closure).
\- If $\rho v\in W$ and $v\in V_{\\_}0$, then there is a unique $v^{\prime}\in
vE$ with $\rho vv^{\prime}\in W$ (unique choice).
\- If $\rho v\in W$ and $v\in V_{\\_}1$, then $\rho vv^{\prime}\in W$ for all
$v^{\prime}\in vE$ (all moves of the opponent).
The strategy is winning if all plays contained in $\mathsf{S}$ are winning.

We commonly write $\rho\in\mathsf{S}$ instead of $\rho\in W$, and we often
refer to paths of the form $\rho v\in\mathsf{S}$ as _occurrences of $v$_ in
$\mathsf{S}$. When we depict strategies graphically, we represent finite paths
$\rho v$ just by their last position $v$ to ease readability (notice that in
the tree unravelling $\rho$ can be reconstructed from $v$ by following the
path to the root). See Figure 1b for an example. For $v\in V_{\\_}0$, we
further write $\mathsf{S}(\rho v)=w$ if $\rho vw$ is the (unique) successor of
$\rho v$ in $\mathsf{S}$. If $\mathsf{S}$ is positional, we may also write
$\mathsf{S}(v)$ to denote the unique successor of $v$ chosen by $\mathsf{S}$.
We write $\operatorname{\mathrm{Strat}}_{\\_}\mathsf{G}(v)$ and
$\operatorname{\mathrm{WinStrat}}_{\\_}\mathsf{G}(v)$ to denote the set of all
(winning) strategies of Player 0 from position $v\in\mathsf{G}$, and we drop
$\mathsf{G}$ if the game is clear from the context.

$v$$v^{\prime}$$u$$w$$a$$c$$b$$d$$e$$i$$f$$h$$g$$k$$m$$n$$p$$q$ (a)
Rectangular nodes belong to Player 1, round nodes to Player 0, dashed nodes
are in $F$.

$v$$v^{\prime}$$v^{\prime}$$a$$b$$e$$h$$c$$f$$g$$g$$k$$m$$m$$k$$m$$m$ (b)
Depiction of an infinite strategy tree of a winning strategy for Player 0 from
position $v$.

Figure 1: Running example of a Büchi game and a winning strategy.

######  Example 3.

An example of a Büchi game is depicted in Figure 1. Player 0 has essentially
three different positional winning strategies from $v$, by either choosing
edge $d$, or edges $e,h,m$ or $f,m$. Notice that for the first strategy, we
did not specify moves for all positions in $V_{\\_}0$ as these positions
cannot be reached when edge $d$ is played; this is the main reason why we
represent strategies as trees. Figure 1b depicts such a tree representation of
a strategy. This strategy is a typical example of a winning strategy that is
not positional, but still minimal if we take edge multiplicities into account.
$\lrcorner$

##  3 Strategies with Minimal Effort

> Perfection is achieved, not when there is nothing more to add, but when
> there is nothing left to take away — Antoine de Saint-Exupéry

As a measure for the complexity or effort of a strategy, we consider the set
of edges a strategy $\mathsf{S}$ uses and how often each of these edges
appears in the strategy tree. Under this measure, the simplest strategies are
the ones that do not play redundant edges – hence no moves are left to take
away.

######  Definition 4.

Given an edge $e=vw\in E$ in a Büchi game $\mathsf{G}$ and a strategy
$\mathsf{S}$ in $\mathsf{G}$, we denote by $\\#_{e}(\mathsf{S})=|\\{\rho
v\in\mathsf{S}\mid\rho v\to\rho vw\text{ is an edge in
}\mathsf{S}\\}|\in{\mathbb{N}}\cup\\{\infty\\}$ the number of times (possibly
infinite) the edge $e$ occurs in $\mathsf{S}$. With each strategy $\mathsf{S}$
we associate its _edge profile_ , the vector
$\\#_{E}(\mathsf{S})=(\\#_{e}(\mathsf{S}))_{\\_}{e\in E}$.

######  Example 5.

Consider the following Büchi game:

$v$$w$$a$$c$$b$

Player 0 wins by first looping $n$ times at position $v$ (for any fixed
$n\in{\mathbb{N}}$) and then moving to $w$, corresponding to the edge profile
$(n,1,\infty)$. Clearly, looping at $v$ is a redundant move, so we consider
the strategy with $n=0$ as the simplest strategy (that wins with the least
effort). $\lrcorner$

To formalize the intuition of redundant moves, we define an order $\succeq$ on
strategies called absorption. This is defined in such a way that the
$\succeq$-maximal strategies are the simplest ones that avoid redundant moves
whenever possible.

######  Definition 6.

Let $\mathsf{S}_{\\_}1,\mathsf{S}_{\\_}2$ be two strategies in a Büchi game
$\mathsf{G}=(V,V_{\\_}0,V_{\\_}1,E,F)$. We say that $\mathsf{S}_{\\_}1$
_absorbs_ $\mathsf{S}_{\\_}2$, denoted
$\mathsf{S}_{\\_}1\succeq\mathsf{S}_{\\_}2$, if
$\\#_{e}(\mathsf{S}_{\\_}1)\leq\\#_{e}(\mathsf{S}_{\\_}2)$ for all edges $e\in
E$. If additionally $\\#_{e}(\mathsf{S}_{\\_}1)<\\#_{e}(\mathsf{S}_{\\_}2)$
for some $e\in E$, we say that $\mathsf{S}_{\\_}1$ _strictly absorbs_
$\mathsf{S}_{\\_}2$, denoted $\mathsf{S}_{\\_}1\succ\mathsf{S}_{\\_}2$. They
are _absorption-equivalent_ , denoted
$\mathsf{S}_{\\_}1\equiv\mathsf{S}_{\\_}2$, if both
$\mathsf{S}_{\\_}1\succeq\mathsf{S}_{\\_}2$ and
$\mathsf{S}_{\\_}2\succeq\mathsf{S}_{\\_}1$. A strategy
$\mathsf{S}\in\operatorname{\mathrm{Strat}}(v)$ is _absorption-dominant from
position $v$_, if there is no strategy
$\mathsf{S}^{\prime}\in\operatorname{\mathrm{Strat}}(v)$ with
$\mathsf{S}^{\prime}\succ\mathsf{S}$. It is further _strictly_ absorption-
dominant, if there is no other strategy
$\mathsf{S}^{\prime}\in\operatorname{\mathrm{Strat}}(v)$ with
$\mathsf{S}^{\prime}\succeq\mathsf{S}$, so no other strategy is absorption-
equivalent to $\mathsf{S}$.

Notice that absorption is simply the inverse pointwise order on the edge
profiles. In particular, $\mathsf{S}_{\\_}1\equiv\mathsf{S}_{\\_}2$ if, and
only if, $\\#_{E}(\mathsf{S}_{\\_}1)=\\#_{E}(\mathsf{S}_{\\_}2)$. We next aim
at understanding the relation between (strictly) absorption-dominant
strategies and the standard notion of positional strategies. As a starter, we
show that absorption-dominant strategies are not necessarily positional (cf.
[17] for a similar example).

######  Example 7.

Consider the strategy $\mathsf{S}$ as depicted in Figure 1b. It is not
positional, as the choice for position $v^{\prime}$ is not unique (both $e$
and $f$ occur in $\mathsf{S}$). It is, however, absorption-dominant. As there
are two paths to $v^{\prime}$, every strategy must either use $e$ or $f$
twice, or use both edges. If $e$ (or $f$) is used twice, then the strategy
cannot absorb $\mathsf{S}$, and one can verify that $\mathsf{S}$ absorbs all
strategies using both $e$ and $f$.

It is not strictly absorption-dominant, as we obtain an absorption-equivalent
strategy by switching the two branches in the depiction of $\mathsf{S}$, so
that $e$ is used after $c$, and $f$ after $b$. $\lrcorner$

Strategies such as the one in Figure 1b are not positional, but satisfy the
weaker property that within each _play_ , the strategy makes a unique decision
for each position $v\in V_{\\_}0$. This notion of strategies has been
introduced as _persistent_ strategies in [21] in the context of LTL on game
graphs and has been further studied in [12]. Persistent strategies have also
been called _weakly positional_ in [17].

We say that a strategy _plays positionally_ from a position $v\in V_{\\_}0$ if
the strategy makes a unique choice at position $v$. A strategy that plays
positionally from all positions in $V_{\\_}0$ is positional. With this
notation, we now clarify the relation between the different notions of
strategies; a summary is shown in Figure 2. We first observe that if a
strategy $\mathsf{S}$ does not play positionally from $v$, we can always
obtain a strategy $\mathsf{S}^{\prime}$ with
$\mathsf{S}^{\prime}\succeq\mathsf{S}$ by swapping the choices at $v$. This
leads to the first result (see [15] for details):

absorption-dominantpositional = strictly abs.-dom.persistentWinning
strategiesEx. 7Ex. 11 Figure 2: Venn diagram depicting the relation of various
classes of winning strategies.

######  Proposition 8.

Strictly absorption-dominant strategies coincide with positional strategies.

Towards persistent strategies, we observe, by applying a simple combinatorial
fact known as Dickson’s Lemma to edge profiles, that there are only finitely
many absorption-dominant strategies from $v$ up to absorption-equivalence.
This leads to the following result:

######  Proposition 9.

Let $\mathsf{S}\in\operatorname{\mathrm{WinStrat}}_{\\_}\mathsf{G}(v)$ be
absorption-dominant from $v$, and let $w\in V_{\\_}0$ be a position. If $w$
occurs infinitely often in $\mathsf{S}$, then $\mathsf{S}$ plays positionally
from $w$.

###### Proof sketch.

Consider the infinitely many substrategies at occurrences of $w$ in
$\mathsf{S}$. By Dickson’s Lemma, there is one such substrategy
$\mathsf{S}_{\\_}w$ such that infinitely many of the substrategies are
absorption-equivalent to $\mathsf{S}_{\\_}w$. In particular,
$\mathsf{S}_{\\_}w$ only uses edges that occur infinitely often in
$\mathsf{S}$. By positional determinacy, there is thus a positional winning
strategy $\mathsf{S}_{\\_}{\text{pos}}$ from $w$ with the same property. If
$\mathsf{S}$ would not be positional, then modifying $\mathsf{S}$ to always
play $\mathsf{S}_{\\_}{\text{pos}}$ from $w$ would result in a strategy
$\mathsf{S}^{\prime}\succ\mathsf{S}$, a contradiction. ∎

With this important insight, we can deduce that the absorption-dominant
winning strategies (from some position $v$) are a (strict) subset of the
persistent strategies: An absorption-dominant strategy must play positionally
from positions that occur infinitely often by Proposition 9; positions that
occur finitely often cannot be visited twice in one play (this would be a
redundant repetition).

######  Corollary 10.

Every absorption-dominant winning strategy in $\mathsf{G}$ is persistent.

######  Example 11.

For strictness, consider the following game (a modified part of Figure 1a):

$v$$a$$b$

$\\#_{a,b}(\mathsf{S}_{\\_}1)=(2,0)$,

$\\#_{a,b}(\mathsf{S}_{\\_}2)=(0,\infty)$,

$\\#_{a,b}(\mathsf{S}_{\\_}3)=(1,\infty)$.

Due to the self-loop $b$, only the positional strategies $\mathsf{S}_{\\_}1$
(always take $a$) and $\mathsf{S}_{\\_}2$ (always take $b$) are absorption-
dominant from $v$. The strategy $\mathsf{S}_{\\_}3$ that, depending on Player
1’s choice, either takes edge $a$ or loops indefinitely using edge $b$ is
persistent, but not absorption-dominant: it is strictly absorbed by
$\mathsf{S}_{\\_}2$. $\lrcorner$

As a consequence of Corollary 10, all moves after the first repeated position
are determined by persistence and we can thus represent absorption-dominant
strategies in a compact way.

######  Corollary 12.

Let $\mathsf{G}$ be a game with $n=|V|$ positions. Every winning strategy
$\mathsf{S}\in\operatorname{\mathrm{WinStrat}}_{\\_}\mathsf{G}(v)$ that is
absorption-dominant from $v$ can be uniquely represented by a subtree of the
tree unraveling of height at most $n$. In particular, the number of
absorption-dominant winning strategies is finite.

##  4 A Whirlwind Tour of Semiring Semantics

This section gives an overview on semiring semantics for fixed-point logics,
with a focus on the semirings relevant for the case study. For a complete
account, we refer to [10].

###  4.1 Semirings

Semirings are algebraic structures with two binary operations, usually denoted
$+$ and $\boldsymbol{\cdot}$, which we use to interpret the logical
connectives $\lor$ and $\land$. While semirings are very general structures,
we make additional assumptions to ensure well-defined and meaningful semiring
semantics for logics with fixed-point operators, following the definitions in
[10].

######  Definition 13.

A _commutative semiring_ is an algebraic structure
$({\mathbb{K}},+,\boldsymbol{\cdot},0,1)$, with $0\neq 1$, such that
$({\mathbb{K}},+,0)$ and $({\mathbb{K}},\boldsymbol{\cdot},1)$ are commutative
monoids, $\boldsymbol{\cdot}$ distributes over $+$, and
$0\boldsymbol{\cdot}a=a\boldsymbol{\cdot}0=0$. It is _idempotent_ if $a+a=a$
for all $a\in{\mathbb{K}}$.

All semirings we consider are commutative, so we omit _commutative_ in the
following. Towards fixed-point logic, we compute least and greatest fixed
points with respect to the natural order $\leq_{\\_}{\mathbb{K}}$ (see below)
and to ensure that they exist, we require $\leq_{\\_}{\mathbb{K}}$ to be a
complete lattice (in fact, suprema and infima of chains would suffice, but in
idempotent semirings this is equivalent). We additionally impose a natural
_continuity_ requirement which is crucial to our proofs, but does not seem to
be a strong restriction in practice (we are not aware of any natural complete-
lattice semirings that are not continuous). Regarding notation, a _chain_ is a
totally ordered set $C\subseteq{\mathbb{K}}$ and we write $a\circ C=\\{a\circ
c\mid c\in C\\}$ for $a\in{\mathbb{K}}$.

######  Definition 14.

In an idempotent semiring $({\mathbb{K}},+,\boldsymbol{\cdot},0,1)$, the
_natural order_ $\leq_{\\_}{\mathbb{K}}$ is the partial order defined by
$a\leq_{\\_}{\mathbb{K}}b\Leftrightarrow a+b=b$. We say that ${\mathbb{K}}$ is
_fully continuous_ if $\leq_{\\_}{\mathbb{K}}$ is a complete lattice (with
supremum $\bigsqcup$ and infimum $\bigsqcap$) and for all non-empty chains
$C\subseteq{\mathbb{K}}$, elements $a\in{\mathbb{K}}$ and
$\circ\in\\{+,\boldsymbol{\cdot}\\}$,

$\bigsqcup(a\circ C)=a\circ\bigsqcup C,\quad\text{and}\quad\bigsqcap(a\circ
C)=a\circ\bigsqcap C.$

A semiring homomorphism $h\colon{\mathbb{K}}_{\\_}1\to{\mathbb{K}}_{\\_}2$ on
fully-continuous semirings is _fully continuous_ if $h(\bigsqcup C)=\bigsqcup
h(C)$ and $h(\bigsqcap C)=\bigsqcap h(C)$ for all non-empty chains
$C\subseteq{\mathbb{K}}_{\\_}1$.

By the Knaster-Tarski theorem, every $\leq_{\\_}{\mathbb{K}}$-monotone
function $f\colon{\mathbb{K}}\to{\mathbb{K}}$ on a fully-continuous semiring
has a least fixed point $\operatorname{\mathbf{lfp}}(f)$ and a greatest fixed
point $\operatorname{\mathbf{gfp}}(f)$ in ${\mathbb{K}}$, and this suffices to
guarantee well-defined semantics of fixed-point logics. However, from a
provenance perspective we further want this semantics to be meaningful in the
sense that the value of a formula provides insights into why the formula
holds. It turns out that this is the case if we additionally require the
semiring to be absorptive [10].

######  Definition 15.

A semiring ${\mathbb{K}}$ is _absorptive_ if $a+ab=a$ for all
$a,b\in{\mathbb{K}}$.

We remark that absorption is equivalent to ${\mathbb{K}}$ being _0-closed_ or
_bounded_ [22], that is, $1+a=1$. If ${\mathbb{K}}$ is idempotent, then
absorption is further equivalent to multiplication being decreasing, that is,
$a\boldsymbol{\cdot}b\leq_{\\_}{\mathbb{K}}a,b$. Clearly, every absorptive
semiring is idempotent and thus partially ordered by $\leq_{\\_}{\mathbb{K}}$,
with $1$ as top element. If we additionally assume full continuity, we can
extend any absorptive semiring by an infinitary power operation
$a^{\infty}=\bigsqcap_{\\_}{n\in{\mathbb{N}}}a^{n}$ with natural properties
such as $a\boldsymbol{\cdot}a^{\infty}=a^{\infty}$ and
$(a+b)^{\infty}=a^{\infty}+b^{\infty}$.

######  Example 16.

Examples of semirings used in provenance analysis of databases and logics [19,
20, 17] are:

  * •

The _Boolean semiring_
$\mathbb{B}=(\\{\mathbf{0},\mathbf{1}\\},\vee,\wedge,\mathbf{0},\mathbf{1})$
is the standard habitat of logical truth. It is absorptive and (trivially)
fully continuous.

  * •

$\mathbb{N}=(\mathbb{N},+,\cdot,0,1)$ is used for counting evaluation
strategies for a logical statement. It is not absorptive and hence not well
suited for fixed-point logics.

  * •

The _Viterbi_ semiring $\mathbb{V}=([0,1],\max,\cdot,0,1)$ is used to compute
_confidence scores_ for logical statements. It is isomorphic to the _tropical_
semiring $\mathbb{T}=(\mathbb{R}_{\\_}{+}^{\infty},\min,+,\infty,0)$ which is
used for measuring the cost of evaluation strategies. Both are absorptive and
fully continuous.

  * •

The _min-max_ semiring $(A,\max,\min,a,b)$ on a totally ordered set $(A,\leq)$
with least and greatest elements $a$ and $b$ can be used to model access
privileges. It is absorptive and fully continuous. $\lrcorner$

From now on, all semirings we consider are commutative, absorptive and fully
continuous. Besides the application semirings listed above, we are
particularly interested in universal semirings of polynomials to represent
abstract information. We can then use fully-continuous homomorphisms to
specialize the computed information to application semirings as needed, as
these homomorphisms preserve fixed points.

The common examples of semirings of polynomials ${\mathbb{N}}[X]$ and formal
power series ${\mathbb{N}}^{\infty}[\\![X]\\!]$, as used for provenance
analysis of FO and Datalog in [19, 16], are not absorptive and hence not well-
suited for fixed-point logic. Instead, we rely on semirings of
(generalized111The definition we use here generalizes the notion of absorptive
polynomials in [11] by allowing $\infty$ as exponent.) _absorptive
polynomials_. We summarize the definition and main properties given in [10].
Essentially, an absorptive polynomial such as $ab^{3}+c^{\infty}$ is a sum of
monomials over a finite set of variables $X$, but without coefficients and
with exponents from ${\mathbb{N}}\cup\\{\infty\\}$ (where $n<\infty$ for
$n\in{\mathbb{N}}$). Monomial multiplication is defined as usual (with
$n+\infty=\infty$).

The key ingredient is absorption among monomials. We say that a monomial
$m_{\\_}1$ _absorbs_ $m_{\\_}2$, if all its exponents are smaller (or equal).
Formally, $m_{\\_}1\succeq m_{\\_}2$ if $m_{\\_}1(x)\leq m_{\\_}2(x)$ for all
$x\in X$, where $m_{\\_}1(x)$ denotes the exponent of $x$ in $m_{\\_}1$. For
example, $ab^{2}\succeq a^{\infty}b^{2}$ and $a\succeq ab$, but $a^{2}b$ and
$ab^{2}$ are incomparable. In an absorptive polynomial, we omit all monomials
that would be absorbed, so absorptive polynomials are $\succeq$-_antichains_
of monomials. Consequently, addition and multiplication are defined as usual,
but afterwards we only keep the $\succeq$-maximal monomials. For example,
$(ab^{2}+a^{2}b)\boldsymbol{\cdot}a^{\infty}=a^{\infty}b^{2}+a^{\infty}b=a^{\infty}b$.

We write ${\mathbb{S}}^{\infty}[X]$ for the semiring of absorptive polynomials
over the finite variable set $X$. The $0$ and $1$-elements are the empty
polynomial and the single monomial $1$ (with all zero exponents). This defines
an absorptive, fully-continuous semiring [10]. In fact,
${\mathbb{S}}^{\infty}[X]$ is the most general such semiring:

######  Theorem 17 (Universal Property, [10]).

Every mapping $h\colon X\to{\mathbb{K}}$ into an absorptive, fully-continuous
semiring ${\mathbb{K}}$ uniquely extends to a fully-continuous semiring
homomorphism $h\colon{\mathbb{S}}^{\infty}[X]\to{\mathbb{K}}$.

###  4.2 Logic

We consider here the fixed-point logic LFP that extends first-order logic FO
by least and greatest fixed-point formulae of the form
$\psi(\mathbf{y})=[\operatorname{\mathbf{lfp}}R\mathbf{x}.\
\varphi(R,\mathbf{x})](\mathbf{y})$ and
$\psi(\mathbf{y})=[\operatorname{\mathbf{gfp}}R\mathbf{x}.\
\varphi(R,\mathbf{x})](\mathbf{y})$. Here, $R$ is a relation symbol occurring
only positively in $\varphi$ and $\mathbf{x},\mathbf{y}$ are variable tuples
of matching arity. Given a (Boolean) model ${\mathfrak{A}}$ and a tuple
$\mathbf{a}$ of elements of ${\mathfrak{A}}$, the formula $\psi(\mathbf{a})$
holds in ${\mathfrak{A}}$, denoted ${\mathfrak{A}}\models\psi(\mathbf{a})$, if
$\mathbf{a}$ is contained in the least (or greatest) fixed point of the
operator $F_{\\_}\varphi\colon
R\mapsto\\{\mathbf{a}\mid{\mathfrak{A}}\models\varphi(R,\mathbf{a})\\}$ that
maps a relation $R$ to the relation consisting of those tuples for which
$\varphi$ holds. For more background and a precise definition, we refer to
[14].

In order to generalize Boolean semantics to semiring semantics, we first adapt
the notion of a model ${\mathfrak{A}}$. Instead of determining for each
literal whether it is true or false in ${\mathfrak{A}}$, we assign to each
literal a semiring value, interpreting $0$ as _false_ and all other values as
_nuances of true_. Special care is required to ensure that the assignment is
consistent with respect to opposing literals (this is not always necessary,
but often desirable). In the following, let ${\mathbb{K}}$ be a semiring, $A$
a finite universe and $\tau$ a relational signature (we drop $A$ and $\tau$ if
clear from the context). We denote the set of (instantiated) literals as

$\displaystyle\operatorname{\mathrm{Lit}}_{\\_}{A,\tau}={}$
$\displaystyle\\{R\mathbf{a},\neg R\mathbf{a}\mid R\in\tau\text{ of arity
$k$},\mathbf{a}\in
A^{k}\\}\,\cup\,\\{\mathbf{a}=\mathbf{b},\mathbf{a}\neq\mathbf{b}\mid\mathbf{a},\mathbf{b}\in
A^{k}\\}.$

Given a literal $L$, we write $\neg L$ for the opposing literal (identifying
$\neg\neg L$ and $L$). The role of the Boolean model ${\mathfrak{A}}$ is then
replaced by a semiring interpretation $\pi$ that assigns semiring values to
all literals.

######  Definition 18.

Let ${\mathbb{K}}$ be a semiring. A _${\mathbb{K}}$ -interpretation_ (over
finite $A$ and $\tau$) is an assignment
$\pi\colon\operatorname{\mathrm{Lit}}_{\\_}{A,\tau}\to{\mathbb{K}}$ that maps
true (in)equalities to $1$ and false (in)equalities to $0$. We say that
${\mathbb{K}}$ is _model-defining_ , if for each literal $L$, exactly one of
$\pi(L)$ and $\pi(\neg L)$ is $0$.

We lift $\pi$ to LFP-formulae in negation normal form, resulting in a semiring
value $\pi[\\![\psi]\\!]$, by interpreting $\land$ and $\lor$ as semiring
operations $\boldsymbol{\cdot}$ and $+$, and similarly quantifiers as products
or sums over the (finite) universe. For fixed-point formulae, we consider the
induced operator $F_{\\_}\varphi$ analogous to the Boolean case (but acting on
mappings $A^{k}\to{\mathbb{K}}$ instead of relations $R\subseteq A^{k}$) and
compute its fixed point in the semiring ${\mathbb{K}}$. We refer to [10] for a
formal definition; the details are not relevant for this paper, as we will
only consider a fixed formula $\psi$ (see Section 5). An important property of
the resulting semantics is that they are preserved by fully-continuous
semiring homomorphisms, in particular by polynomial evaluation in
${\mathbb{S}}^{\infty}[X]$ due to Theorem 17 (but not by polynomial evaluation
of $\mathbb{N}[X]$ or formal power series!).

##  5 Case Study: Computing Strategies with Semiring Semantics

This section connects the previous sections on semiring semantics and
absorption-dominant strategies. We focus on the formula for the winning region
in a Büchi game and show that its value under semiring semantics can be
understood in terms of (absorption-dominant) winning strategies.

###  5.1 The Semiring Interpretation

We want to use semiring semantics to analyze moves in winning strategies. For
this reason, we label edges with indeterminates $X$ (cf. Figure 1a) and use an
${\mathbb{S}}^{\infty}[X]$-interpretation $\pi_{\text{strat}}$ to track moves
(i.e., edge literals $Euv$) via their indeterminates. We assume the game graph
to be fixed and do not wish to track information about the winning set $F$ or
the active player at a certain node, hence we simply map all other literals
over $\tau=\\{E,F,V_{\\_}0,V_{\\_}1\\}$ (e.g., $Fv$, $V_{\\_}0v$, $\neg Euv$)
to $0$ or $1$, depending on whether they are true or false in the game. The
resulting interpretation is almost Boolean and hence behaves very similar to
the original game, except that we remember which edges are used in the
evaluation of a formula.

######  Definition 19.

Let $G=(V,V_{\\_}0,V_{\\_}1,E,F)$ be a Büchi game and let
$X=\\{X_{\\_}{vw}\mid vw\in E\\}$ be a set of indeterminates for all edges. We
define the ${\mathbb{S}}^{\infty}[X]$-interpretation $\pi_{\text{strat}}$ as
follows (depending on $G$):

$\pi_{\text{strat}}(Evw)=X_{\\_}{vw}\text{ for all }vw\in
E,\quad\pi_{\text{strat}}(L)=\begin{cases}1,&\text{ if }G\models L,\\\
0,&\text{ if }G\not\models L,\end{cases}\;\text{ for all other literals
$L\in\operatorname{\mathrm{Lit}}_{\\_}{V,\tau}$.}$

###  5.2 The Formula

It is well known that the winning region (of Player 0) in a Büchi game is
definable in fixed-point logic. Intuitively, the winning region is the largest
set $Y$ such that from each position in $Y$, Player 0 can enforce a visit to
$Y\cap F$ (after at least one move). In LFP, we can express the winning region
by the following formula (see, e.g., [4, 27]):

$\displaystyle\mathsf{win}_{0}(x)\coloneqq{}$
$\displaystyle\big{[}\operatorname{\mathbf{gfp}}Yy.\
[\operatorname{\mathbf{lfp}}Zz.\ \varphi(Y,Z,z)](y)\big{]}(x),$
$\displaystyle\varphi(Y,Z,z)\coloneqq{}$
$\displaystyle\Big{(}Fz\;\land\;((V_{\\_}0z\land\exists u(Ezu\land
Yu))\lor(V_{\\_}1z\land\forall u(Ezu\to Yu)))\Big{)}$ $\displaystyle{}\lor{}$
$\displaystyle\Big{(}\neg Fz\;\land\;((V_{\\_}0z\land\exists u(Ezu\land
Zu))\lor(V_{\\_}1z\land\forall u(Ezu\to Zu)))\Big{)}.$

Given a ${\mathbb{K}}$-interpretation $\pi$ for a Büchi game
$\mathsf{G}=(V,V_{\\_}0,V_{\\_}1,E,F)$, semiring semantics of the above
formula induce222Here we first translate $Ezu\to Yu$ to the formula $\neg
Ezu\lor(Ezu\land Yu)$ in negation normal form. the following fixed-point
computation. To simplify the presentation, we introduce two families of
variables, $\mathbf{Y}=(Y_{\\_}v)_{\\_}{v\in V}$ and
$\mathbf{Z}=(Z_{\\_}v)_{\\_}{v\in V}$ that take values in ${\mathbb{K}}$. We
can then express the semiring semantics as
$\pi[\\![\mathsf{win}_{0}(v)]\\!]=Y^{*}_{\\_}v$ where
$\mathbf{Y}^{*}=(Y_{\\_}v^{*})_{\\_}{v\in V}$ is the _greatest_ solution to
the equation system

$\mathbf{Y}=\mathbf{Z}^{*}(\mathbf{Y})$

where, in turn, $\mathbf{Z}^{*}(\mathbf{Y})$ is the _least_ solution, given
values $\mathbf{Y}=(Y_{\\_}v)_{\\_}{v\in V}$, to the equation system
consisting of the following equation for all $v\in V$:

$\displaystyle Z_{\\_}v={}$
$\displaystyle\pi(Fv)\boldsymbol{\cdot}\Big{(}(\pi(V_{\\_}0v)\boldsymbol{\cdot}\sum_{\\_}{w\in
V}(\pi(Evw)\boldsymbol{\cdot}Y_{\\_}w))+(\pi(V_{\\_}1v)\boldsymbol{\cdot}\prod_{\\_}{w\in
V}(\pi(\neg Evw)+\pi(Evw)\boldsymbol{\cdot}Y_{\\_}w))\Big{)}$
$\displaystyle{}+{}$ $\displaystyle\pi(\neg
Fv)\boldsymbol{\cdot}\Big{(}(\pi(V_{\\_}0v)\boldsymbol{\cdot}\sum_{\\_}{w\in
V}(\pi(Evw)\boldsymbol{\cdot}Z_{\\_}w))+(\pi(V_{\\_}1v)\boldsymbol{\cdot}\prod_{\\_}{w\in
V}(\pi(\neg Evw)+\pi(Evw)\boldsymbol{\cdot}Z_{\\_}w))\Big{)}$

For most of this paper, we use the interpretation $\pi_{\text{strat}}$ to
track only _moves_ of winning strategies. As $\pi_{\text{strat}}$ maps most of
the literals to $0$ or $1$, we can simplify the equations depending on $v$:

| $v\in F$ | $v\notin F$
---|---|---
$v\in V_{\\_}0$ | $\displaystyle Z_{\\_}v=\sum_{\\_}{w\in vE}\pi(Evw)\boldsymbol{\cdot}Y_{\\_}w$ | $\displaystyle Z_{\\_}v=\sum_{\\_}{w\in vE}\pi(Evw)\boldsymbol{\cdot}Z_{\\_}w$
$v\in V_{\\_}1$ | $\displaystyle Z_{\\_}v=\prod_{\\_}{w\in vE}\pi(Evw)\boldsymbol{\cdot}Y_{\\_}w$ | $\displaystyle Z_{\\_}v=\prod_{\\_}{w\in vE}\pi(Evw)\boldsymbol{\cdot}Z_{\\_}w$

A good way to think about (and compute) the least and greatest solutions is
the fixed-point iteration. The idea is to start with each $Z_{\\_}v$ set to
the least element of the semiring, then apply the above equations (i.e., the
induced operator $F_{\\_}\varphi$) to compute a next, larger semiring value
and repeat this process until a fixed-point is reached (notice that the
iteration can also be infinite, we then continue with the supremum/infimum).

######  Example 20.

Recall the simple game from Example 5 $\big{(}$ $v$$w$$a$$c$$b$
$\\!\\!\big{)}$.

Using the interpretation $\pi_{\text{strat}}$ corresponding to the edge
labels, we obtain the following fixed-point iteration. We write the tuples
$\mathbf{Y}$ and $\mathbf{Z}$ as vectors $({Y_{\\_}v}\;{Y_{\\_}w})^{T}$ and
$({Z_{\\_}v}\;{Z_{\\_}w})^{T}$.

$\mathbf{Y}:$$\mathbf{Z}:$$\begin{pmatrix}1\\\
1\end{pmatrix}$$\begin{pmatrix}0\\\ 0\end{pmatrix}$$\begin{pmatrix}0\\\
c\end{pmatrix}$$\begin{pmatrix}bc\\\ c\end{pmatrix}$$\begin{pmatrix}bc\\\
c\end{pmatrix}$$\begin{pmatrix}0\\\ 0\end{pmatrix}$$\begin{pmatrix}0\\\
c^{2}\end{pmatrix}$$\begin{pmatrix}bc^{2}\\\
c^{2}\end{pmatrix}$$\begin{pmatrix}bc^{2}\\\
c^{2}\end{pmatrix}$$\dots\vphantom{\begin{pmatrix}x\\\
x\end{pmatrix}}$$\mathbf{Y}^{*}=\begin{pmatrix}bc^{\infty}\\\
c^{\infty}\end{pmatrix}$$F_{\\_}\varphi$$F_{\\_}\varphi$$F_{\\_}\varphi$$F_{\\_}\varphi$

We obtain the overall result
$\pi_{\text{strat}}[\\![\mathsf{win}_{0}(v)]\\!]=Y_{\\_}v^{*}=\bigsqcap_{\\_}nbc^{n}=bc^{\infty}$
corresponding to the unique absorption-dominant strategy using edge $b$ once
and $c$ infinitely often (cf. Example 5). $\lrcorner$

###  5.3 Connection to Strategies

By mapping edges to semiring values, we can track edges through the fixed-
point computation. In Example 20, the resulting semiring value revealed how
often each edge is used in the unique absorption-dominant winning strategy. We
now generalize this observation. For simplicity, we only consider
${\mathbb{K}}$-interpretations $\pi$ that are _edge tracking_ for a given game
$\mathsf{G}$. That is, they may assign arbitrary values to positive edge
literals $Evw$, but all other literals are mapped to $0$ or $1$ in accordance
with $\mathsf{G}$. To make the connection to strategies explicit, we first
define semiring values for strategies based on their edges.

######  Definition 21.

Let $\mathsf{S}$ be a strategy in a Büchi game
$\mathsf{G}=(V,V_{\\_}0,V_{\\_}1,E,F)$. Let ${\mathbb{K}}$ be an absorptive,
fully-continuous semiring and $\pi$ an edge-tracking
${\mathbb{K}}$-interpretation on $\mathsf{G}$. The _${\mathbb{K}}$ -value_ of
$\mathsf{S}$ is the product of the values for all edges appearing in
$\mathsf{S}$. Formally,

$\pi[\\![\mathsf{S}]\\!]\coloneqq\prod_{\\_}{vw\in
E}\pi(Evw)^{\\#_{vw}(\mathsf{S})}.$

The semiring value of $\mathsf{win}_{0}$ can then be expressed as the sum over
the values of all winning strategies. The proof of this result (see [15]) is
based on a similar result for LFP model-checking games in [10] which is rather
involved due to both infinite strategy trees and infinite fixed-point
iterations.

######  Theorem 22 (Sum of Strategies).

Let $\mathsf{G}$ be a Büchi game and $v$ a position in $\mathsf{G}$. Let
${\mathbb{K}}$ be an absorptive, fully-continuous semiring and $\pi$ an edge-
tracking ${\mathbb{K}}$-interpretation. Then,

$\pi[\\![\mathsf{win}_{0}(v)]\\!]=\sum\big{\\{}\pi[\\![\mathsf{S}]\\!]\;\big{|}\;\text{$\mathsf{S}\in\operatorname{\mathrm{WinStrat}}_{\\_}\mathsf{G}(v)$
is absorption-dominant from $v$}\big{\\}}.$

It is in fact this central result that motivated the notion of _absorption-
dominant_ strategies. However, as we have already discussed, these may also be
interesting in their own right if one is interested in minimal winning
strategies.

######  Example 23.

For the edge-tracking interpretation $\pi_{\text{strat}}$ induced by the edge
labels in Figure 1a, we obtain

$\displaystyle\pi_{\text{strat}}[\\![\mathsf{win}_{0}(v)]\\!]={}$
$\displaystyle(abcd)^{\infty}+abc\,e^{2}h^{2}(gkm)^{\infty}+abc\,f^{2}(gkm)^{\infty}+abc\,efh(gkm)^{\infty}.$

There are four monomials, corresponding to four equivalence classes of
absorption-dominant strategies. Each monomial reveals the edges that appear in
the corresponding strategies, so we see that the first three monomials belong
to positional (and hence uniquely defined) strategies. The last monomial
belongs to the non-positional strategy shown in Figure 1b (and its switched
version, see Example 7). The values of all other strategies are strictly
absorbed by one of these monomials. $\lrcorner$

###  5.4 Strategy Analysis

For the general case, we fix a Büchi game $\mathsf{G}$ and focus on the
${\mathbb{S}}^{\infty}[X]$-interpretation $\pi_{\text{strat}}$ with
$X=\\{X_{\\_}{uv}\mid u,v\in\mathsf{G}\\}$. The values
$\pi_{\text{strat}}[\\![\mathsf{S}]\\!]$ are monomials and we can read off the
number of occurrences of each edge in $\mathsf{S}$ from the exponents, i.e.,
the monomial is a representation of the edge profile $\\#_{E}(\mathsf{S})$. In
particular,
$\pi_{\text{strat}}[\\![\mathsf{S}_{\\_}1]\\!]\succeq\pi_{\text{strat}}[\\![\mathsf{S}_{\\_}2]\\!]$
if, and only if, $\mathsf{S}_{\\_}1\succeq\mathsf{S}_{\\_}2$. The fact that
absorptive polynomials are always finite [10] is thus another way to see that
the number of absorption-dominant strategies is finite.

What can we learn from the polynomial
$\pi_{\text{strat}}[\\![\mathsf{win}_{0}(v)]\\!]$? First,
$\pi_{\text{strat}}[\\![\mathsf{win}_{0}(v)]\\!]\neq 0$ holds if, and only if,
Player 0 has a winning strategy from $v$. By Theorem 22, we can further derive
information about all absorption-dominant strategies. More precisely, we learn
which edges each absorption-dominant strategy uses and how often they appear
in the strategy tree. Knowing the edge profile immediately reveals whether the
strategy is positional and what the positional choices are. By counting
monomials, we can thus count the positional strategies, as well as the
absorption-dominant strategies up to absorption-equivalence.

We can further answer questions such as: can Player 0 still win if we remove
edge $e$? This is the case if, and only if, the polynomial
$\pi_{\text{strat}}[\\![\mathsf{win}_{0}(v)]\\!]$ contains a monomial without
the variable $X_{\\_}e$ (if there is a winning strategy without $e$, then
there is also an absorption-dominant strategy and hence a monomial without
$X_{\\_}e$). Going further, a more interesting question is: can Player 0 still
win if edge $e$ may only be used finitely often in each play? The answer is
not immediately obvious. Consider for example the strategy $\mathsf{S}$ in
Figure 1b. The edge $k$ occurs infinitely often in the strategy tree and we
get
$\pi_{\text{strat}}[\\![\mathsf{S}]\\!]=abcefhg^{\infty}k^{\infty}m^{\infty}$.
However, $k$ is clearly played only once in each play consistent with
$\mathsf{S}$, whereas edge $m$ is played infinitely often. We cannot
distinguish edges $k$ and $m$ just from
$\pi_{\text{strat}}[\\![\mathsf{S}]\\!]$, but we can do so if we compute
$\pi_{\text{strat}}[\\![\mathsf{win}_{0}(w)]\\!]$ for all positions $w\in V$,
by the following criterion.

######  Proposition 24.

Let $\mathsf{S}\in\operatorname{\mathrm{WinStrat}}_{\\_}\mathsf{G}(v)$ be
absorption-dominant from $v$, and let $e=uw\in E$ be an edge with
$\\#_{e}(\mathsf{S})=\infty$. Then there is a unique positional strategy
$\mathsf{S}_{\\_}w\in\operatorname{\mathrm{WinStrat}}_{\\_}\mathsf{G}(w)$ such
that
$\pi_{\text{strat}}[\\![\mathsf{S}_{\\_}w]\\!]\succeq\pi_{\text{strat}}[\\![\mathsf{S}]\\!]$.
Moreover, $\mathsf{S}$ admits a play in which $e$ occurs infinitely often if,
and only if, $e$ occurs in $\mathsf{S}_{\\_}w$.

######  Example 25.

Consider the strategy $\mathsf{S}$ in Figure 1b with
$\pi_{\text{strat}}[\\![\mathsf{S}]\\!]=abcefhg^{\infty}k^{\infty}m^{\infty}$
and the edge $k$ from $u$ to $w$. Since edge $n$ does not occur in
$\pi_{\text{strat}}[\\![\mathsf{S}]\\!]$, the only winning strategy
$\mathsf{S}_{\\_}w$ from $w$ we need to consider is the strategy that always
stays at $w$, with
$\pi_{\text{strat}}[\\![\mathsf{S}_{\\_}w]\\!]=m^{\infty}\succeq\pi_{\text{strat}}[\\![\mathsf{S}]\\!]$.
As $k$ does not occur in $\mathsf{S}_{\\_}w$, we conclude that it occurs only
finitely often (and hence at most once) in each play consistent with
$\mathsf{S}$.

If, on the other hand, we consider edge $m$ (which also leads to position
$w$), we see that $m$ occurs in $S_{\\_}w$ and we can thus conclude that
$\mathsf{S}$ contains a play visiting $m$ infinitely often. $\lrcorner$

Summarizing the results of this section, we see that semiring semantics in
${\mathbb{S}}^{\infty}[X]$ is very informative and allows us to derive
important information about the winning strategies.

######  Corollary 26.

From the polynomial $\pi_{\text{strat}}[\\![\mathsf{win}_{0}(v)]\\!]$, we can
efficiently (in the size of the polynomial) derive the following information:
\- whether Player $0$ wins from $v$,
\- the edge profiles of all absorption-dominant winning strategies from $v$,
\- the number and precise shape of all positional winning strategies from $v$,
\- whether Player $0$ can still win from $v$ if only a subset of the edges is
allowed.

From the polynomials $\pi_{\text{strat}}[\\![\mathsf{win}_{0}(v)]\\!]$, for
all positions $v$, we can further derive for each absorption-dominant strategy
and each edge, how often the edge can occur in a play consistent with the
strategy.

Regarding the complexity, we remark that it is not obvious how to compute
$\pi_{\text{strat}}[\\![\mathsf{win}_{0}(v)]\\!]$, as depending on the
semiring, the fixed-point iteration may be infinite (even if the game is
finite). However, it has been shown in [23] that in absorptive, fully-
continuous semirings, fixed points of polynomial systems, such as the ones
induced by $\mathsf{win}_{0}(v)$, can be computed using a number of semiring
operations (including the infinitary power operation) that is polynomial in
the size of the game.

Notice, however, that for $\pi_{\text{strat}}[\\![\mathsf{win}_{0}(v)]\\!]$,
the number of monomials and hence the cost to compute semiring operations can
become exponentially large. This is not avoidable, as the number of
(positional) winning strategies can be exponential. More efficient algorithms
can be obtained by modifying $\pi_{\text{strat}}$ to track only some of the
edges (mapping the rest to $1$). The resulting interpretation remains edge-
tracking, so the Sum-of-Strategies Theorem still applies and we can see which
sets of tracked edges (if any) are required for a winning strategy. Even then,
some of the questions in Corollary 26 can also be solved by direct methods
which may be more efficient. Thus, the main benefit of semiring semantics in
${\mathbb{S}}^{\infty}[X]$ does not lie in a more efficient method to compute
some specific winning strategy, but rather in providing a general and compact
description of all important strategies at once, from which we can directly
derive the answers to many different questions concerning the strategy
analysis of a Büchi game.

###  5.5 Reverse Analysis

Instead of tracking strategies in a fixed game, we may also ask questions such
as: assuming Player 1 wins from $v$, what are minimal modification to
$\mathsf{G}$ such that instead Player 0 wins? The generality of semiring
semantics enables us to answer such questions by choosing appropriate
semirings and interpretations.

More precisely, let $\mathsf{G}=(V,V_{\\_}0,V_{\\_}1,E,F)$ be a Büchi game and
$v\in\mathsf{G}$ a position from which Player 1 wins. Let $E^{-}\subseteq E$
and $E^{+}\subseteq V^{2}\setminus E$ be sets of edges we are allowed to
delete or add, respectively. We call a set of edges in $E^{\pm}\coloneqq
E^{-}\cup E^{+}$ a _repair_ if Player 0 wins when these edges are deleted or
added. Our goal is to determine all (preferably minimal) repairs. We achieve
this by evaluating $\mathsf{win}_{0}(v)$ in a modified polynomial semiring,
similar to the computation of repairs for database queries in [28], except
that here we need absorptive polynomials to deal with fixed points.

Dual-Indeterminates. To track negative information, such as the absence of an
edge, we follow the approach in [16, 28, 10] and extend our semiring by dual-
indeterminates $\overline{X}=\\{\overline{x}\mid x\in X\\}$. The idea is to
label a literal and its negation by corresponding indeterminates $x$ and
$\overline{x}$. We must then avoid monomials such as $x\overline{x}$, as they
represent contradictory information. To this end, we consider the quotient of
${\mathbb{S}}^{\infty}[X\cup\overline{X}]$ with respect to the congruence
generated by $x\cdot\overline{x}=0$ for $x\in X$ and refer to the resulting
quotient semiring as dual-indeterminate absorptive polynomials
${\mathbb{S}}^{\infty}[X,\overline{X}]$. This semiring inherits most of the
properties of ${\mathbb{S}}^{\infty}[X]$. Most importantly, any assignment
$h\colon X\cup\overline{X}$ that respects dual-indeterminates, i.e.,
$h(x)\cdot h(\overline{x})=0$, lifts to a fully-continuous homomorphism
analogous to Theorem 17.

We then replace $\pi_{\text{strat}}$ with an
${\mathbb{S}}^{\infty}[X,\overline{X}]$-interpretation
$\pi_{\text{rep}}^{\pm}$ for $X=\\{X_{\\_}e\mid e\in E^{\pm}\\}$: if $vw\in
E^{\pm}$, we set $\pi_{\text{rep}}^{\pm}(Evw)=X_{\\_}{vw}$ and
$\pi_{\text{rep}}^{\pm}(\neg Evw)=\overline{X_{\\_}{vw}}$, all other literals
are mapped to $0$ or $1$ according to $\mathsf{G}$. Notice that
$\pi_{\text{rep}}^{\pm}$ is not model-defining, but still satisfies
$\pi_{\text{rep}}^{\pm}(L)\boldsymbol{\cdot}\pi_{\text{rep}}^{\pm}(\neg L)=0$
for all literals $L$.

Back and Forth between Monomials and Models. Let $X^{\pm}=\\{X_{\\_}e\mid e\in
E^{+}\\}\cup\\{\overline{X_{\\_}e}\mid e\in E^{-}\\}$. Given $Y\subseteq
X^{\pm}$, we further write $E(Y)=\\{e\mid X_{\\_}e\in Y\text{ or
}\overline{X_{\\_}e}\in Y\\}$ for the set of edges mentioned in $Y$. We denote
the set of all (dual-)indeterminates occurring in a monomial $m$ by
$\mathsf{var}(m)=\\{x\in X\cup\overline{X}\mid m(x)>0\\}$. By examining what
combination of indeterminates from $X^{\pm}$ occur in the monomials of
$\pi_{\text{rep}}^{\pm}[\\![\mathsf{win}_{0}(v)]\\!]$, we can read off all
minimal repairs as follows.

######  Proposition 27.

In the above setting, the following holds:

  1. 1.

Let $m\in\pi_{\text{rep}}^{\pm}[\\![\mathsf{win}_{0}(v)]\\!]$ be a monomial.
Then the set $E(\mathsf{var}(m)\cap X^{\pm})$ is a repair.

  2. 2.

Let $R\subseteq E^{\pm}$ be a repair. Then there is a monomial
$m\in\pi_{\text{rep}}^{\pm}[\\![\mathsf{win}_{0}(v)]\\!]$ such that
$E(\mathsf{var}(m)\cap X^{\pm})\subseteq R$. If $R$ is minimal, then
$E(\mathsf{var}(m)\cap X^{\pm})=R$.

Before proving Proposition 27, we illustrate the computation of minimal
repairs in a small example.

######  Example 28.

In the following game, Player 1 wins from $v$. We are interested in the
minimal repairs with $E^{+}=\\{c\\}$ and $E^{-}=\\{a,b\\}$.

$v$$b$$c$$a$

$\displaystyle\pi_{\text{rep}}^{\pm}[\\![\mathsf{win}_{0}(v)]\\!]=\overline{X_{\\_}a}X_{\\_}c^{\infty}+\overline{X_{\\_}a}^{\infty}X_{\\_}b^{\infty}$

Evaluating $\mathsf{win}_{0}(v)$ in the
${\mathbb{S}}^{\infty}[X,\overline{X}]$-interpretation
$\pi_{\text{rep}}^{\pm}$ described above results in two monomials. The first
yields the repair $\\{a,c\\}$, the second yields the minimal repair $\\{a\\}$
(notice that $X_{\\_}b\notin X^{\pm}$, as edge $b$ is already present). The
reason why we get two monomials is that we track also positive usage of edge
$b$ by $X_{\\_}b$, but are only interested in the negative indeterminate
$\overline{X_{\\_}b}$ for the repairs. $\lrcorner$

###### Proof of Proposition 27.

We prove both statements by considering homomorphisms into the Boolean
semiring $\mathbb{B}$. For the first statement, let
$m\in\pi_{\text{rep}}^{\pm}[\\![\mathsf{win}_{0}(v)]\\!]$ be a monomial and
let $h\colon X\cup\overline{X}\to\mathbb{B}$ be the unique function that
respects dual-indeterminates and satisfies

  * •

$h(x)=\mathbf{1}$, for all $x\in\mathsf{var}(m)$

  * •

$h(X_{\\_}e)=\mathbf{0}$, if
$X_{\\_}e,\overline{X_{\\_}e}\notin\mathsf{var}(m)$ and $e\in E^{+}$ (do not
add $e$ without reason),

  * •

$h(X_{\\_}e)=\mathbf{1}$, if
$X_{\\_}e,\overline{X_{\\_}e}\notin\mathsf{var}(m)$ and $e\in E^{-}$ (do not
remove $e$ without reason).

Then, $h$ lifts to a fully-continuous semiring homomorphism
$h\colon{\mathbb{S}}^{\infty}[X,\overline{X}]\to\mathbb{B}$ with
$h(m)=\mathbf{1}$. Moreover, $h\circ\pi_{\text{rep}}^{\pm}$ is a Boolean
interpretation which corresponds to a Boolean model $\mathsf{G}^{\prime}$.
Since semiring semantics are preserved by fully-continuous homomorphisms, we
have
$h\circ\pi_{\text{rep}}^{\pm}[\\![\mathsf{win}_{0}(v)]\\!]=h(\pi_{\text{rep}}^{\pm}[\\![\mathsf{win}_{0}(v)]\\!])\geq
h(m)=\mathbf{1}$ and hence $\mathsf{G}^{\prime}\models\mathsf{win}_{0}(v)$. By
the choice of $h$, the model $\mathsf{G}^{\prime}$ is equal to $\mathsf{G}$
except that we add all edges $e\in X^{+}$ with $X_{\\_}e\in\mathsf{var}(m)$,
and remove all $e\in X^{-}$ with $\overline{X_{\\_}e}\in\mathsf{var}(m)$.
Hence $\mathsf{G}^{\prime}$ results from $\mathsf{G}$ by adding or deleting
the edges $E(\mathsf{var}(m)\cap X^{\pm})$, and since
$\mathsf{G}^{\prime}\models\mathsf{win}_{0}(v)$, this set is a repair as
claimed.

For the second statement, let $R\subseteq E^{\pm}$ be a repair and consider
the repaired game $\mathsf{G}^{\prime}\models\mathsf{win}_{0}(v)$. As
$\mathsf{G}^{\prime}$ differs from $\mathsf{G}$ only by edges in $E^{\pm}$,
there is a unique assignment $h\colon X\cup\overline{X}\to\mathbb{B}$ such
that $h\circ\pi_{\text{rep}}^{\pm}$ corresponds to $\mathsf{G}^{\prime}$.
Again, $h$ lifts to a fully-continuous homomorphisms and we thus get
$\mathbf{1}=h\circ\pi_{\text{rep}}^{\pm}[\\![\mathsf{win}_{0}(v)]\\!]=h(\pi_{\text{rep}}^{\pm}[\\![\mathsf{win}_{0}(v)]\\!])$.
So there must be a monomial
$m\in\pi_{\text{rep}}^{\pm}[\\![\mathsf{win}_{0}(v)]\\!]$ with
$h(m)=\mathbf{1}$. Consider the set $\mathsf{var}(m)\cap X^{\pm}$. If
$X_{\\_}e\in\mathsf{var}(m)\cap X^{\pm}$, then $h(X_{\\_}e)=\mathbf{1}$ and
hence $e\in R$ by construction of $h$. Further,
$\overline{X_{\\_}e}\in\mathsf{var}(m)\cap X^{\pm}$ implies
$h(\overline{X_{\\_}e})=\mathbf{1}$ and thus again $e\in R$ by construction of
$h$. This proves $E(\mathsf{var}(m)\cap X^{\pm})\subseteq R$. If $R$ is
minimal, we have equality: otherwise $E(\mathsf{var}(m)\cap X^{\pm})$ would be
a smaller repair by the first statement, contradicting minimality. ∎

We remark that these results ignore the exponents of the monomials, so we
could drop exponents from ${\mathbb{S}}^{\infty}[X,\overline{X}]$ and work in
the resulting, simpler semiring $\mathsf{PosBool}[X,\overline{X}]$ (but again,
the number of minimal repairs can be exponential in the size of the game).
Further, the reverse analysis approach is not limited to questions about
edges. We can also work with interpretations that track the target set $F$ and
thus answer questions such as how to choose or modify the target set so that
Player $0$ wins?

##  6 Conclusion

Based on a recent line of research on semiring provenance analysis that lead
from database theory to semiring semantics for LFP, we reported here on a case
study that puts semiring semantics to use for a strategy analysis in Büchi
games. The choice of Büchi games has been motivated on one side by their
relevance for applications in the synthesis and verification of reactive
systems, on the other side because they provide one of the simplest non-
trivial cases of infinite games for which the definability of winning
positions requires an alternation between least and greatest fixed points –
and can thus not be treated by simpler classes of semirings such as the
$\omega$-continuous ones used for Datalog and reachability games.

The aim of the case study was to illustrate how semiring semantics can be
applied to more complex games, featuring infinite plays and complicated
winning conditions, and what kind of insights it provides (or fails to
provide) about the winning strategies in the game. This is captured in the
central Sum-of-Strategies Theorem and its applications. This non-trivial
result can be seen as a simpler version of the general Sum-of-Strategies
characterization in terms of model-checking games in [10] and it essentially
identifies the value of the statement that Player 0 wins with the sum of the
valuations of all (absorption-dominant) winning strategies. While this applies
to the class of all absorptive, fully-continuous semirings, the most important
semirings for our analysis are generalized absorptive polynomials
${\mathbb{S}}^{\infty}[X]$. Due to their universal property, these provide the
most general information, allowing us to read off the edge profiles of all
absorption-dominant strategies.

With this information, we can count positional strategies, we can determine
whether a particular move is needed (once or even infinitely often) for
winning the game, and we can compute minimal “repairs” for a game. The method
of semiring valuations is rather flexible; we can use different semirings than
${\mathbb{S}}^{\infty}[X]$, and we can tailor the set of moves that we track
to make the resulting polynomial smaller and its computation more efficient.
We remark that, of course, there are also limitations to this method and not
all relevant questions about strategies can be answered directly by semiring
valuations. As an example we show in the full version of this paper [15] that
minimal cost computations provide serious obstacles to a semiring treatment.

The Sum-of-Strategies result motivates the general notion of absorption-
dominant strategies which captures strategies that are minimal with respect to
the multiplicities of the edges they use. To understand these strategies, we
discussed how they relate to other classes of simple strategies, namely to
positional and persistent strategies, and we have shown that these form a
strict hierarchy.

Finally, we remark that although Büchi games have been chosen as the topic of
our case study, the method of semiring valuations in absorptive semirings is
not confined to this case. In principle, it can be applied to different
formulae and generalizes in particular to other games such as parity games, as
long as the winning positions are definable in fixed-point logic. The win-
formula for parity games is more complicated, and is parametrised by the
number of priorities, and so the Sum-of-Strategies Theorem requires different
technical details, but can be established along the same lines.

## References

  * [1]
  * [2] C. Bourgaux, A. Ozaki, R. Peñaloza & L. Predoiu (2020): _Provenance for the Description Logic ELHr_.  In: Proceedings of IJCAI 2020, pp. 1862–1869, 10.24963/ijcai.2020/258.
  * [3] J. Bradfield & I. Walukiewicz (2018): _The mu-calculus and model checking_.  In E. Clarke, T. Henzinger, H. Veith & R. Bloem, editors: Handbook of Model Checking, Springer, pp. 871–919, 10.1007/978-3-319-10575-826.
  * [4] F. Canavoi, E Grädel, S. Lessenich & W. Pakusa (2015): _Defining winning strategies in fixed-point logic_.  In: 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 366–377, 10.1109/LICS.2015.42.
  * [5] K. Chatterjee, W. Dvorák, M. Henzinger & V. Loitzenbauer (2016): _Conditionally Optimal Algorithms for Generalized Büchi Games_.  arXiv:1607.05850 [cs.DS].  Available at http://arxiv.org/abs/1607.05850.
  * [6] K. Chatterjee & M. Henzinger (2014): _Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition_.  J. ACM 61(3), pp. 15:1–15:40, 10.1145/2597631.
  * [7] K. Chatterjee, T. Henzinger & N. Piterman (2008): _Algorithms for Büchi Games_.  arXiv:0805.2620 [cs.GT].  Available at http://arxiv.org/abs/0805.2620.
  * [8] K. Dannert & E. Grädel (2019): _Provenance Analysis: A Perspective for Description Logics?_ In C. Lutz et al., editor: Description Logic, Theory Combination, and All That, Lecture Notes in Computer Science 11560, Springer, pp. 266–285, 10.1007/978-3-030-22102-712.
  * [9] K. Dannert & E. Grädel (2020): _Semiring Provenance for guarded logics_.  In: Hajnal Andréka and István Németi on Unity of Science: From Computing to Relativity Theory through Algebraic Logic, Outstanding Contributions to Logic, Springer, pp. 53–79, 10.1007/978-3-030-64187-03.
  * [10] K. Dannert, E. Grädel, M. Naaf & V. Tannen (2021): _Semiring Provenance for Fixed-Point Logic_.  In C. Baier & J. Goubault-Larrecq, editors: 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), Leibniz International Proceedings in Informatics (LIPIcs) 183, Dagstuhl, pp. 17:1–17:22, 10.4230/LIPIcs.CSL.2021.17.
  * [11] D. Deutch, T. Milo, S. Roy & V. Tannen (2014): _Circuits for Datalog Provenance_.  In: Proc. 17th International Conference on Database Theory ICDT, OpenProceedings.org, pp. 201–212, 10.5441/002/icdt.2014.22.
  * [12] J. Duparc (2003): _Positive games and persistent strategies_.  In: International Workshop on Computer Science Logic, Springer, pp. 183–196, 10.1007/978-3-540-45220-117.
  * [13] F. Geerts & A. Poggi (2010): _On database query languages for K-relations_.  Journal of Applied Logic 8(2), pp. 173–185, 10.1016/j.jal.2009.09.001.
  * [14] E. Grädel, P. G. Kolaitis, L. Libkin, M. Marx, J. Spencer, M. Y. Vardi, Y. Venema & S. Weinstein (2007): _Finite Model Theory and Its Applications_.  Texts in Theoretical Computer Science. An EATCS Series, Springer, 10.1007/3-540-68804-8.
  * [15] E. Grädel, N. Lücking & M. Naaf (2021): _Semiring Provenance for Büchi Games: Strategy Analysis with Absorptive Polynomials_.  arXiv:2106.12892 [cs.LO].  Available at https://arxiv.org/abs/2106.12892.
  * [16] E. Grädel & V. Tannen (2017): _Semiring Provenance for First-Order Model Checking_.  arXiv:1712.01980 [cs.LO].  Available at https://arxiv.org/abs/1712.01980.
  * [17] E. Grädel & V. Tannen (2020): _Provenance analysis for logic and games_.  Moscow Journal of Combinatorics and Number Theory 9(3), pp. 203–228, 10.2140/moscow.2020.9.203.  Preprint available at https://arxiv.org/abs/1907.08470.
  * [18] E. Grädel, W. Thomas & T. Wilke, editors (2002): _Automata, Logics, and Infinite Games_.  Lecture Notes in Compter Science 2500, Springer, 10.1007/3-540-36387-4.
  * [19] T. Green, G. Karvounarakis & V. Tannen (2007): _Provenance semirings_.  In: Principles of Database Systems PODS, pp. 31–40, 10.1145/1265530.1265535.
  * [20] T. Green & V. Tannen (2017): _The Semiring Framework for Database Provenance_.  In: Proceedings of PODS, ACM, pp. 93–99, 10.1145/3034786.3056125.
  * [21] J. Marcinkowski & T. Truderung (2002): _Optimal complexity bounds for positive LTL games_.  In: International Workshop on Computer Science Logic, Springer, pp. 262–275, 10.1007/3-540-45793-318.
  * [22] M. Mohri (2002): _Semiring frameworks and algorithms for shortest-distance problems_.  Journal of Automata, Languages and Combinatorics 7(3), pp. 321–350, 10.25596/jalc-2002-321.
  * [23] M. Naaf (2021): _Computing Least and Greatest Fixed Points in Absorptive Semirings_.  arXiv:2106.00399 [cs.LO].  Available at https://arxiv.org/abs/2106.00399.
  * [24] A. Ozaki & R. Peñaloza (2018): _Provenance in Ontology-based Data Access_.  In: Description Logics 2018, CEUR Workshop Proceedings 2211\.  Available at http://ceur-ws.org/Vol-2211/paper-28.pdf.
  * [25] M. Raghothaman, J. Mendelson, D. Zhao, M. Naik & B. Scholz (2020): _Provenance-guided synthesis of Datalog programs_.  Proc. ACM Program. Lang. 4, pp. 62:1–62:27, 10.1145/3371130.
  * [26] P. Senellart (2017): _Provenance and Probabilities in Relational Databases: From Theory to Practice_.  SIGMOD Record 46(4), pp. 5–15, 10.1145/3186549.3186551.
  * [27] I. Walukiewicz (2002): _Monadic second-order logic on tree-like structures_.  Theoretical Computer Science 275, pp. 311–346, 10.1016/S0304-3975(01)00185-2.
  * [28] J. Xu, W. Zhang, A. Alawini & V. Tannen (2018): _Provenance Analysis for Missing Answers and Integrity Repairs_.  IEEE Data Eng. Bull. 41(1), pp. 39–50.  Available at http://sites.computer.org/debull/A18mar/p39.pdf.


# Symmetry of surfaces for linear fractional group

Lokenath Kundu, Kaustav Mukherjee<EMAIL_ADDRESS><EMAIL_ADDRESS>SRM University, A.P.  Indian Institute of
Science Education and Research Bhopal, Madhya Pradesh 462066

(Date: 24/11/21)

###### Abstract.

We will compute the stable upper genus for the family of finite non-abelian
simple groups $PSL_{2}(\mathbb{F}_{p})$ for $p\equiv 3~{}(mod~{}4)$. This
classification is well-grounded in the other branches of Mathematics like
topology, smooth, and conformal geometry, algebraic categories.

###### Key words and phrases:

Riemann surface, finite group, stable upper genus.

##  1\. Introduction

Let $\Sigma_{g}$ be a Riemann surface of genus $g\geq 0$. We will imply by the
action of a finite group $G$ on $\Sigma_{g}$, a properly discontinuous,
orientation preserving, faithful action. The collection $\\{g\geq
0|G~{}\text{acts on}~{}\Sigma_{g}\\}$ is known as spectrum of $G$ denoted by
$Sp(G)$. The least element of $Sp(G)$ is denoted by $\mu(G)$ familiar as the
minimum genus of the group $G$. An element $g\in Sp(G)$ is said to be the
stable upper genus of a given group $G$, if $g+i\in Sp(G)$ for all
$i\in\mathbb{N}$. The necessary and sufficient condition for an effective
action of a group $G$ preserving the orientation on compact, connected,
orientable surface $\Sigma_{g}$ of genus $g$ except for finitely many
exceptional values of $g$ was proved by Kulkarni in [6]. In particular the
group $PSL_{2}(\mathbb{F}_{p})$ has the above mentioned property for
$p\geq~{}5$, and $p$ is odd. The authors determined the minimum genus for the
family of finite groups in [3, 4].
Any action of a finite group $G$ on a Riemann surface $\Sigma_{g}$ of genus
$g$ gives an orbit space $\Sigma_{h}~{}:=\Sigma_{g}/G$ also known as orbifold.
We can take this action as conformal action, that means the action is analytic
in some complex structure on $\Sigma_{g}$, as the positive solution of Nielson
Realization problem [1, 2] implies that if any group $G$ acts topologically on
$\Sigma_{g}$ then it can also act conformally with respect to some complex
structure.
The orbit space $\Sigma_{h}$ is again a Riemann surface possibly with some
marked points and the quotient map
$p~{}:~{}\Sigma_{g}~{}\rightarrow~{}\Sigma_{h}$ is a branched covering map.
Let $B=~{}\\{c_{1},c_{2},\dots,c_{r}~{}\\}$ be the set of all branch points in
$\Sigma_{h}$ and $A:=p^{-1}(B)$. Then $p:~{}\Sigma_{g}\setminus
A~{}\rightarrow~{}\Sigma_{h}\setminus B$ is a proper covering. The tuple
$(h;m_{1},m_{2},\dots,m_{r})$ is known as signature of the finite group $G$,
where $m_{1},m_{2},\dots,m_{r}$ are the order of stabilizer of the preimages
of the branch points $c_{1},c_{2},\dots,c_{r}$ respectively. By Riemann-
Hurwitz formula we have

$(g-1)=~{}|G|(h-1)+\frac{|G|}{2}\sum_{i=1}^{r}(1-\frac{1}{m_{i}}).$

The signature of a group encodes the information of the group action of a
Riemann surface and about $Sp(G)$. For more details about signature of
Fuchsian group and Riemann surfaces refer to [11], and [12] respectively. In
[15, 16], with accurate use of Frobenius theorem and explicit formation of
surface kernel epimorphisms, the author able to prove the following theorems:

######  Theorem 1.1.

[15] $(h;2^{[a_{2}]},3^{[a_{3}]},4^{[a_{4}]},7^{[a_{7}]})$ is a signature of
$PSL_{2}(\mathbb{F}_{7})$ if and only if

$1+168(h-1)+42a_{2}+56a_{3}+63a_{4}+72a_{7}\geq 3$

except when the signature is $(1;2)$.

######  Theorem 1.2.

[15] $(h;2^{[a_{2}]},3^{[a_{3}]},5^{[a_{5}]},6^{[a_{6}]}11^{[a_{11}]})$ is a
signature of $PSL_{2}(\mathbb{F}_{11})$ if and only if

$1+660(h-1)+165a_{2}+220a_{3}+264a_{5}+275a_{6}+300a_{11}\geq 26.$

and the following lemma;

######  Lemma 1.3.

[16]
$(h_{\geq~{}0};~{}2^{[a_{2}]},~{}3^{[a_{3}]},~{}4^{[a_{4}]},~{}5^{[a_{5}]},~{}d^{[a_{d}]},~{}\frac{p-1}{2}^{[a_{\frac{p-1}{2}}]},~{}\frac{p+1}{2}^{[a_{\frac{p+1}{2}}]},~{}p^{[a_{p}]})$
is a signature for $PSL_{2}(\mathbb{F}_{p})$ for $p~{}\equiv~{}3~{}(mod~{}4)$
if and only if

$2(h-1)+~{}\frac{a_{2}-1}{2}~{}+\frac{2a_{3}-1}{3}+~{}\frac{3a_{4}}{4}+~{}\frac{4a_{5}}{5}+~{}\frac{(d-1)a_{d}+1}{d}~{}+\frac{a_{\frac{p-1}{2}}(p-3)}{p-1}~{}+\frac{a_{\frac{p+1}{2}}(p-1)}{p+1}$
$+\frac{(p-1)a_{p}}{p}~{}\geq 0\text{ or }$
$20(h-1)~{}+10[\frac{a_{2}}{2}~{}+\frac{2.a_{3}}{3}~{}+\frac{3.a_{4}}{4}~{}+\frac{4.a_{5}}{5}~{}+\frac{(d-1)a_{d}}{d}~{}+\frac{(p-3)a_{\frac{p-1}{2}}}{p-1}~{}+$
$\frac{(p-1)a_{\frac{p+1}{2}}}{p+1}~{}+\frac{(p-1)a_{p}}{p}]~{}\geq~{}1$

when $p~{}\geq~{}13,~{}p\equiv\pm
1~{}(\mod~{}5~{}),~{}p~{}\not\equiv~{}\pm~{}1(\mod~{}8),~{}\text{and}~{}d\geq
15$. Here

$d:=min\\{e|e\geq 7\text{ and either }e|\frac{p-1}{2}\text{ or
}e|\frac{p+1}{2}\\}.$

Having the details knowledge of the spectrum of the group
$PSL_{2}(\mathbb{F}_{p})$ one would like to address the following question:
What is the stable upper genus for each of the group $PSL_{2}(\mathbb{F}_{p})$
for $p\equiv 3~{}(mod~{}4)$? In [15], we find out the stable upper genus for
the group $PSL_{2}(\mathbb{F}_{7})$ is 399 and the stable upper genus for the
group $PSL_{2}(\mathbb{F}_{11})$ is 3508 using generic programming techniques
[7, 8, 9, 10]. Following a similar approach described in [15], here we will
largely extend the scenario for higher prime numbers and determine the stable
upper genus value for the each of the members of the family of finite groups
$PSL_{2}(\mathbb{F}_{p})$ for $p\equiv 3~{}(mod~{}4)$. Interestingly, the
novelty of this work is the observance of the exponential curve fitting for
the stable upper genus values of $PSL_{2}(\mathbb{F}_{p})$ for $p\equiv
3~{}(mod~{}4)$ which has not been seen in earlier cases [6, 15].
Here we have stated the main result of this paper as follows:

######  Theorem 1.4.

The stable upper genus value of the group $PSL_{2}(\mathbb{F}_{p})$ can be
written in the form

(1.1) $g=ap^{b}e^{c\times p},$

where $a$, $b$ and $c$ are constants discussed in the proof and $g$ represents
the upper stable genus of the group $PSL_{2}(\mathbb{F}_{p})$ while $p$ is the
respective prime for $p\equiv 3~{}(mod~{}4)$.

Implementing computations with loops over large variations of $h$ and $a_{i}$
[1.1,1.2,1.3] by means of Python coding [7, 8, 10], we find a set of stable
upper genus values of $PSL_{2}(\mathbb{F}_{p})$ for $p\in\\{7,11,19,23\\}$
which we discuss in the following sections. Based on the set of stable upper
genus values, we construct a mathematical function described in Eq. 1.1, which
follows the variation in the stable upper genus values of
$PSL_{2}(\mathbb{F}_{p})$ with the respect to $p$. We discuss the detailed
comparison of the expression in Eq. 1.1 with the dependency of the stable
upper genus on $p$ in the proof. To explore the possibility of obtaining a
mathematical function describing the stable upper genus as a function of $p$
for the group $PSL_{2}(\mathbb{F}_{p})$, we make use of the curve-fitting
technique on Mathematica [19] following from Fit and Manipulate tool, which
provides us with the best fit on the data set of the stable upper genus
corresponding to respective prime $p\in\\{7,11,19,23\\}$. We have specifically
considered the function type for the stable upper genus as

(1.2) $g=ap^{b}\exp[cp],$

where $a$, $b$ and $c$ are constants that are obtained based on the best fit
on the data-set and $p$ is the prime following $p\equiv 3~{}(mod~{}4)$. This
expression subsequently provides us an estimate along with upper bound of
stable upper genus of the group $PSL_{2}(\mathbb{F}_{p})$ for general $p\equiv
3~{}(mod~{}4)$. We have organized our paper in the following way. In chapter 2
we will study the necessary preliminary results. In most cases, we will state
the theorems without proof. In chapter 3, we will prove our main Theorem
[1.4].

##  2\. preliminaries

In this section, we will collect the knowledge about the properly
discontinuous actions of a group $G$ on any Riemann surface $\Sigma_{g}$,
signature of a finite group, the family of groups $PSL_{2}(\mathbb{F}_{p})$
for a prime $p$, curve fitting, exponential fitting.

We start with the definition of properly discontinuous action of a finite
group on a Riemann surface.

######  Definition 2.1.

[12] Let $G$ be a finite group is said to act on a Riemann surface
$\Sigma_{g}$ properly discontinuously if for any $x\in\Sigma_{g}$ there exists
a neighbouhood $U$ of $x$ in $X$ such that $g(U)\cap U=\emptyset$ for only
finitely many $g\in G$.

###  2.1. Fuchsian group

A discrete subgroup of the Fuchsian group is known as Fuchsian group [12].

######  Theorem 2.2.

[12] A group $\Gamma$ is a Fuchsian group if and only if $\Gamma$ acts on the
upper half plane $\mathbb{H}$ properly discontinuously.

######  Definition 2.3.

A Fuchsian group $\Gamma$ is said to be co-compact Fuchsian group if
$\mathbb{H}/\Gamma$ is compact.

###  2.2. Dirichlet Region

Let $\Gamma$ be a Fuchsian group acts on the upper half plane $\mathbb{H}$.
Let $p\in\mathbb{H}$ be a point which is not fixed by any non identity element
of $\Gamma\setminus\\{id\\}.$ The Dirichlet region center at $p$ for $\Gamma$
is defined as

$D_{p}(\Gamma)=\\{z\in\mathbb{H}|\rho(z,p)\leq\rho(z,T(p))~{}\forall
T\in\Gamma\setminus\\{id\\}\\}$

Here $\rho$ is the usual hyperbolic metric.

######  Theorem 2.4.

The Dirichlet region $D_{p}(\Gamma)$is a connected region of $\Gamma$ if $p$
is not fixed by any element of $\Gamma\setminus\\{id\\}.$

###### Proof.

[12]. ∎

######  Theorem 2.5.

Any two distinct points that lie inside the Dirichlet region will belong to
two different $\Gamma$ orbits.

###### Proof.

[12]. ∎

Two points $w_{1},w_{2}\in\mathbb{H}$ are said to be congruent if they lie to
the same $\Gamma$ orbit. Any two pints in a fundamental region $F$ may be
congruent only if the points lie in the boundary of $F$. Let $F$ be a
Dirichlet region for a Fuchsian group $\Gamma$. We will consider all congruent
vertices of $F$. The congruence is an equivalence relation on the vertices of
$F$, the equivalence classes are called the cycles. Let $w\in\mathbb{H}$ be
fixed by an elliptic element $T$ of $\Gamma$, then $Sw$ is fixed by
$STS^{-1}$. So if one vertex of the cycle is fixed by an elliptic element then
all the vertices of the cycle are fixed by the conjugate of the elliptic
cycles. Those cycles are called elliptic cycles, and the vertices of the
cycles are known as elliptic vertics. The cardinality of the collection of
distinct elliptical cycles is same as the of non-congruent elliptic points in
the Dirichlet region $F$.
Every non trivial stabilizer of any point in $\mathbb{H}$ is a maximal finite
cyclic subgroup of the group $\Gamma$. In this context we have the following
theorem.

######  Theorem 2.6.

Let $\Gamma$ be a Fuchsian group, and $F$ be a Dirichlet region for $\Gamma$.
Let $\alpha_{1},\alpha_{2},\dots,\alpha_{n}$ be the internal angles at all
congruent vertices of $F$. Let $k$ be the order of the stabilizer in $\Gamma$
of one of the vertices. Then
$\alpha_{1}+\alpha_{2}+\dots+\alpha_{n}=\frac{2\pi}{k}$.

###### Proof.

[12]. ∎

######  Definition 2.7.

The orders of non-conjugate maximal finite cyclic subgroups of the Fuchsian
group $\Gamma$ are known as the period of $\Gamma$.

###  2.3. Signature of Fuchsian group

Let a Fuchsian group $\Gamma$ acts on $\mathbb{H}$. Let the area of the orbit
space $\mathbb{H}/\Gamma$ has the finite area
$i.e.~{}\mu(\mathbb{H}/\Gamma)<\infty.$ The restriction of the natural
projevtion map $\mathbb{H}\rightarrow\mathbb{H}/\Gamma$ to the Dirichlet
region $F$, identifies the congruent points of $F$. So $F/\Gamma$ is an
oriented surface possibly with some marked points as the congruent points are
lying on the boundary of $F$. The marked points are correspond to the elliptic
cycles and the cusps are corresponding to the non-congruent vertices at
infinity. As a space $\mathbb{H}/\Gamma$ is known as orbifold. The number of
cusps and the genus of the orbifold decisive the topology type of the
orbifold. The area of $\mathbb{H}/\Gamma$ is defined as the area of the
fundamental region $F$. If one Dirichlet region is compact then all the other
Dirichlet regions are compact. If a Fuchsin group has a compact Dirichlet
region then the Dirichlet region has finitely many sides and the orbifold is
also compact.
If a convex fundamental region for a Fuchsian group $\Gamma$ has finitely many
sides then the Fuchsian group is known as geometrically finite group.

######  Theorem 2.8.

Let $\Gamma$ be a Fuchsian group. If the orbifold $\mathbb{H}/\Gamma$ has
finite area then the $\Gamma$ is geometrically finite.

###### Proof.

[12]. ∎

######  Definition 2.9.

(Co-compact Fuchsian group) A Fuchsian group is said to be co-compact if the
orbifold $\mathbb{H}/\Gamma$ is compact topological space.

Let $\Gamma$ be a Fuchsian group and $F$ be a compact Dirichlet region for
$\Gamma$. So the number of sides, vertices, and elliptic cycles of $F$ are
finitely many. Let $m_{1},m_{2},\dots,m_{r}$ be the finite number of periods
of $\Gamma$. Hence the orbifold $\mathbb{H}/\Gamma$ is a compact oriented
surface of genus $g$ with $r$-many marked points. The tuple
$(g;m_{1},m_{2},\dots,m_{r})$ is known as the signature of the Fuchsian group
$\Gamma$.

###  2.4. Signature of finite group

Now we define the signature of a finite group in the sense of Harvey [13].

######  Lemma 2.10 (Harvey condition).

A finite group $G$ acts faithfully on $\Sigma_{g}$ with signature
$\sigma:=(h;m_{1},\dots,m_{r})$ if and only if it satisfies the following two
conditions:

  1. (1)

The _Riemann-Hurwitz formula for orbit space_ i.e.

$\displaystyle\frac{2g-2}{|G|}=2h-2+\sum_{i=1}^{r}\left(1-\frac{1}{m_{i}}\right),\text{
and }$

  2. (2)

There exists a surjective homomorphism $\phi_{G}:\Gamma(\sigma)\to G$ that
preserves the orders of all torsion elements of $\Gamma$. The map $\phi_{G}$
is also known as surface-kernel epimorphism.

######  Corollary 2.11.

Let $Sig(G)$ denote the set of all possible signatures of a finite group $G$,
then $Sig(G)$ and $Sp(G)$ have bijective correspondence via the Harvey
condition.

###  2.5. The family of finite groups $PSL_{2}(\mathbb{F}_{p})$

Let $p$ be a prime number. The set

$PSL_{2}(\mathbb{F}_{p}):=\large\\{\begin{pmatrix}a&b\\\
c&d\end{pmatrix}|~{}ad-bc=1,~{}a,b,c,d\in\mathbb{F}_{p}\large\\}/\pm I$

forms a group under matrix multiplication. It is a simple linear group
generated by two elements, $A=\begin{pmatrix}0&1\\\ -1&0\end{pmatrix}$ of
order $2$, and $B=\begin{pmatrix}0&1\\\ -1&-1\end{pmatrix}$ of order $3.$ The
order of $AB=\begin{pmatrix}1&1\\\ 0&1\end{pmatrix}$ is $7,i.e.$

$PSL_{2}(\mathbb{F}_{p})=\langle A,B|A^{2}=B^{3}=(AB)^{P}\rangle.$

######  Theorem 2.12.

Let $p$ be an odd prime. Let $G:=\langle
x,y|x^{p}=y^{p}=(x^{a}y^{b})^{2}=1,ab\equiv 1(mod~{}p)\rangle$ be a two
generator group. Then $G$ is isomorphic $PSL_{2}(\mathbb{F}_{p}).$

###### Proof.

[18]. ∎

####  2.5.1. Maximal subgroups of $PSL_{2}(\mathbb{F}_{p})$

The group $PSL_{2}(\mathbb{F}_{p})$ has $\frac{p(p^{2}-1)}{2}$ many elements.
The elements of the group $PSL_{2}(\mathbb{F}_{p})$ have one of the following
order $p,~{}2,~{}3,~{}4,~{}\text{or}~{}5,~{}d$ and a divisor of either
$\frac{p-1}{2}$ or $\frac{p+1}{2}$ where $d$ is defined as

$d=min\\{~{}e|~{}e\geq 7\text{ and either }e|\frac{p-1}{2}\text{ or
}~{}e|\frac{p+1}{2}\\}.$

A subgroup $H$ of $G$ is said to be a maximal subgroup of $G$ if there exists
a subgroup $K$ such that $H\subset K\subset G,$ then either $H=K$ or $K=G.$
The maximal proper subgroups of $PSL_{2}(\mathbb{F}_{p})$ are the followings
[17];

  * 1.

dihedral group of order $p-1$ or $p+1$.

  * 2.

solvable group of order $\frac{p.(p-1)}{2}$.

  * 3.

$A_{4}$ if $p\equiv 3,13,27,37~{}(mod~{}40)$.

  * 4.

$S_{4}$ if $p\equiv\pm 1~{}(mod~{}8)$.

  * 5.

$A_{5}$ if $p\equiv\pm 1~{}(mod~{}5)$.

###  2.6. Exponential Regression

######  Definition 2.13.

Exponential regression is defined as the process of obtaining a mathematical
expression for the exponential curve that best fits a set of data. In
[exponentialregression], an exponential regression model has been discussed.
As an example, we know a data is fit into a linear regression, if it can be
explained using $y=mx+c$ where the data is represented as $\\{x,y\\}$ with $m$
as the slope and $c$ is the intercept on $y$-axis. Similarly, if the set of
data can be best explained using

(2.1) $\displaystyle Log[y]$ $\displaystyle=mLog[x]+c$ (2.2) $\displaystyle Y$
$\displaystyle=mX+c$

where $Y=Log[y]$ and $X=Log[x]$ with slope $m$ and intercept $c$ then it can
be called as exponential regression. The above example is the simplest form of
exponential regression, with possibilities of significant extension in more
complex scenario.

##  3\. Stable upper genus of $PSL_{2}(\mathbb{F}_{p})$ for $p\equiv
3~{}(mod~{}4)$

In this section we will prove our main theorem [1.4] using python coding.

######  Theorem 3.1.

The stable upper genus of the group $PSL_{2}(\mathbb{F}_{19})$ is 33112.

###### Proof.

We will prove the theorem in two steps.

  1. Step 1:

We will first prove that $33111\notin Sp(PSL_{2}(\mathbb{F}_{19})).$
From [1.3] we know that
$(h;2^{[a_{2}]},3^{[a_{3}]},5^{[a_{5}]},9^{[a_{9}]},10^{[a_{10}]},19^{[a_{19}]})$
is a signature of $PSL_{2}(\mathbb{F}_{19})$ if and only if

$3420h-3419+855a_{2}+1140a_{3}+1368a_{5}+1520a_{9}+1539a_{10}+1620a_{19}\geq
96.$

If possible let

$33111=3420h-3419+855a_{2}+1140a_{3}+1368a_{5}+1520a_{9}+1539a_{10}+1620a_{19}.$

Then the value of $h$ could be at most $11$. Similarly the values of $a_{i}$
could be at most $43,~{}33,~{}27,~{}25,~{}24,~{}23$ for
$i=~{}2,~{}3,~{}5,~{}9,~{}10,~{}19$ respectively. So We will consider

$0~{}\leq~{}h~{}\leq~{}11$ $0~{}\leq~{}a_{2}~{}\leq~{}43$
$0~{}\leq~{}a_{3}~{}\leq~{}33$ $0~{}\leq~{}a_{5}~{}\leq~{}27$
$0~{}\leq~{}a_{9}~{}\leq~{}25$ $0~{}\leq~{}a_{10}~{}\leq~{}24$
$0~{}\leq~{}a_{19}~{}\leq~{}23.$

We execute the following python code to conclude that
$PSL_{2}(\mathbb{F}_{19})$ can not act on a compact, connected, orientable
surface of genus $33111$ preserving the orientation.

Listing 1: $33111$ is not an admissable signature of
$PSL_{2}(\mathbb{F}_{19})$

⬇

def func2(h,a2,a3,a5,a9,a10,a19):

return 1+3420*(h-1) + 855*a2 + 1140*a3 + 1368*a5 + 1520*a9 +

1539*a10 + 1620*a19

for h in range(11):

for a2 in range(43):

for a3 in range(33):

for a5 in range(27):

for a9 in range(25):

for a10 in range(24):

for a19 in range(23):

sol = func2(h,a2,a3,a5,a9,a10,a19)

if sol >33111:

if sol < 33111:

if sol == 33111:

print(”wrong”)

  2. Step 2:

To complete the proof of our claim, we have to find out signatures
corresponding to the genus values $33112-33967$ of $PSL_{2}(\mathbb{F}_{19})$.
We execute the following python code to compute all the signature values of
$PSL_{2}(\mathbb{F}_{19})$ corresponding to the genus values $33112-33967$.

Listing 2: Signatures of $PSL_{2}(\mathbb{F}_{19})$ corresponding to the genus
value $33112-33967$

⬇

def func2(h,a2,a3,a5,a9,a10,a19):

return 1+3420*(h-1) + 855*a2 + 1140*a3 + 1368*a5 + 1520*a9 +

1539*a10 + 1620*a19

sol_arr = []

const_arr = []

for h in range(11):

for a2 in range(44):

for a3 in range(33):

for a5 in range(27):

for a9 in range(25):

for a10 in range(25):

for a19 in range(24):

sol = func2(h,a2,a3,a5,a6,a11)

if sol >33112:

if sol < 33967:

#print(sol)

sol_arr += [sol]

const_arr += [[h,a2,a3,a5,a9,a10,a19]]

color_dictionary = dict(zip(sol_arr, const_arr))

sort_orders = sorted(color_dictionary.items(), key=lambda x: x[0])

for i in sort_orders:

print(i[0], i[1])

Now we have to prove that $PSL_{2}(\mathbb{F}_{19})$ can act on all compact,
connected, orientable surface of genus $g~{}\geq~{}33967$ preserving the
orientation. Let $g~{}\geq 33967$, and $\Sigma_{g}$ be a compact, connected,
orientable surface of genus $g$. So we have

$g-33112~{}\equiv~{}s~{}(mod~{}855)~{}\text{ where }~{}1~{}\leq~{}s~{}\leq
854.$

Then $g~{}=~{}l+n.855$ where $l~{}=33112+s$. We know the signature
corresponding to the genus $l$ as $333112~{}\leq l~{}\leq 33967$ and let it be
$(h;m_{2},~{}m_{3},~{}m_{5},~{}m_{9},m_{10},m_{19})$. Then the signature
corresponding to the genus $g$ is
$(h;m_{2}+n,~{}m_{3},~{}m_{5},~{}m_{9},m_{10},m_{19})$. In this way we can
find signature corresponding to genus $g~{}\geq 33967$. This completes the
proof of our claim.

∎

######  Theorem 3.2.

The stable upper genus of the group $PSL_{2}(\mathbb{F}_{23})$ is 297084.

###### Proof.

Similar to Theorem3.1. ∎

######  Theorem 3.3.

The stable upper genus of the group $PSL_{2}(\mathbb{F}_{31})$ is 20275804.

###### Proof.

Similar to Theorem3.1. ∎

Proof of the main theorem 1.4.

###### Proof.

In the previous Theorems 3.1,3.2,3.3, we have obtained the upper stable genus
for $p\in\\{19,23,31\\}$. Combining with the previously obtained results
described in [15], we now posses a data-set of stable upper genus
$g\in\\{399,3508,33112,297084,20275804\\}$ corresponding to prime
$p\in\\{7,11,19,23,31\\}$ for the group $PSL_{2}(\mathbb{F}_{p})$, shown as
blue dots in Fig.1. We next investigate the dependencies of the stable upper
genus values $g$ with respect to prime number $p\equiv 3~{}(mod~{}4)$,
subsequently constructing a mathematical function described in Eq.1.1, which
can be visualized in Fig.1 [19].

Figure 1.  Upper stable genus values (blue dot) given by
$PSL_{2}(\mathbb{F}_{p})$ for $p$ ranging from $7$ to $31$. Black line
indicates the fitting on the upper stable genus values.

In Fig. 1 (b), we show the Log scaled plot of (a), which provides an
indication of exponential dependence of $g$ on $p$. For the next step, we
consider an ansatz in the form Eq. 1.1. Additionally, Fig. 1 indicates two
linear Log scaled lines, separating the cases $p\in\\{7,11\\}$ and
$p\in\\{19,23,31\\}$. Based on the exponential fitting, using the following
Mathematica code

Listing 3: Exponential fitting of $g$ with respect to $p$ for the group
$PSL_{2}(\mathbb{F}_{p})$

⬇

data = {{7, 399}, {11, 3508}, {19, 33112}, {23, 297084}, {31,

20275804}}

lineardata = ListPlot[data, Frame -> True,

PlotMarkers -> {\\[FilledCircle], 10},

PlotStyle -> Blue,

FrameLabel -> {Style[”Prime␣p”, Black, 14],

Style[”Upper␣stable␣genus␣g”, Black, 14]},

FrameTicksStyle -> Directive[FontSize -> 14],

ImageSize -> Medium,

PlotRange -> All]

logdata = ListPlot[data, Frame -> True,

PlotMarkers -> {\\[FilledCircle], 10},

PlotStyle -> Blue,

FrameLabel -> {Style[”Prime␣p”, Black, 14],

Style[”Upper␣stable␣genus␣g”, Black, 14]},

FrameTicksStyle -> Directive[FontSize -> 14],

ImageSize -> Medium,

PlotRange -> All]

Manipulate[

Show[{logdata, LogPlot[a*p^b*Exp[c*x], {p, 7, 31}]}],

{b, 0.0, 2, 0.5}, {a, 0.5, 4.5, 0.1}, {c, 0.5, 1, 0.01}]

Linearplot =

Show[{lineardata,

Plot[0.5*x^0.5*Exp[0.51*x], {x, 7, 31},

PlotRange -> All,

PlotStyle -> Black],

Plot[4.5*x^0.5*Exp[0.5*x], {x, 7, 31},

PlotRange -> All,

PlotStyle -> {Blue, Dashed}]}, ImageSize -> Large]

Logplot =

Show[{logdata,

LogPlot[0.5*x^0.5*Exp[0.51*x], {x, 7, 31},

PlotRange -> All,

PlotStyle -> Black],

LogPlot[4.5*x^0.5*Exp[0.5*x], {x, 7, 31},

PlotRange -> All,

PlotStyle -> {Blue, Dashed}]}, ImageSize -> Large]

which leads us to the values of constants $\\{a\rightarrow 4.5,b\rightarrow
0.5,c\rightarrow 0.5\\}$ for $p\in\\{7,11\\}$ and $\\{a\rightarrow
0.5,b\rightarrow 0.5,c\rightarrow 0.51\\}$ for $p\in\\{19,23,31\\}$. This
provides a general expression for $g$ as function of $p$ for higher range of
primes $p\equiv 3~{}(mod~{}4)$ following the second category, given as

(3.1) $g=0.5p^{0.5}\exp[0.51p].$

This expressions essentially captures the variation of upper stable genus $g$
with respect to $p$, and provides us with a rough estimate for general case
scenario of $p\equiv 3~{}(mod~{}4)$ as shown in the Table1. In order to
validate the fitting, we predict for arbitrary prime $p=59$, which should have
stable upper genus close to $g=44907302712962$.

Prime p | Stable upper genus g | Exponential fitting g
---|---|---
7 | 399 | 394
11 | 3508 | 3651
19 | 33112 | 35209
23 | 297084 | 297926
31 | 20275804 | 20457219
Table 1. Comparison of Stable upper genus obtained computationally with the
exponential fitting described in 1.1 for primes $p\in\\{7,11,19,23,31\\}$.

∎

##  4\. Acknowledgement

We acknowledge fruitful discussions with Dr. Manish Kumar Pandey. Author
Mukherjee acknowledges financial support from Ministry of Education, India for
the Prime Minister’s Research Fellowship (PMRF) for pursuing Ph.D. Author
Kundu is grateful to Council of Scientific and Industrial Research (CSIR),
India for the partial financial support.

## References

  * [1] Kerckhoff, S. The Nielsen realization problem, Ann. Math. 117 (1983), 235—265.
  * [2] Eckmann, B., Müller, H. Plane motion groups and virtual Poincare duality of dimension two, Invent. Math. 69 (1982), 293—310.
  * [3] Glover, H., Sjerve, D. The genus of $PSL_{2}(q).$ Journal für die renie und angewandte Mathematik. J.renie angew. Math. $380(1987),59-86.$
  * [4] Glover, H., and Sjerve, D. Representing $PSl_{2}(p)$ on a Riemann surface of least genus, L’Enseignement Mathematique 31 (1985), 305—325.
  * [5] Özaydin, M., Simmons, C., and Taback, J. Surface Symmetries and $PSL_{2}(p),$ American Mathematical Society, Volume 359, Number 5, May 2007, Pages 2243–2268. S 0002-9947(06)04011-6.
  * [6] Kulkarni, R.S. Symmetries of Surfaces, Topology, 26, No. 2(1987), 195-203.
  * [7] Pérez. F., and Granger. B. E. IPython: A System for Interactive Scientific Computing, Computing in Science & Engineering, (2007) 9, 21-29.
  * [8] McKinney. W. Data Structures for Statistical Computing in Python, Proceedings of the 9th Python in Science Conference, (2010), 51-56.
  * [9] Hunter. J. D. Matplotlib: A 2D Graphics Environment, Computing in Science & Engineering, (2007), 9, 90-95.
  * [10] Harris. C. R. et al., Array programming with NumPy, Nature, 585, (2020), 357–362.
  * [11] Foster, O. Lectures on Riemann surfaces. Springer Verlag New york INC.
  * [12] Katok, S. Fuchsian groups. Chicago Lectures in Mathematics. University of Chicago Press, Chicago, IL, $1992.$
  * [13] Harvey, W.J. Cyclic groups of automorphisms of a compact Riemann surface. Quart. J. Math. Oxford Ser. $(2),$ $1966$, $17:86-97.$
  * [14] Lando, S.K., Zvonkin, A. K., Graphs on surfaces and their applications. Springer-Verlag Berlin Heidelberg New York: 2004.
  * [15] Kundu, L. (2021). Linear Fractional group as Galois group. Journal of Topology and Analysis. DOI: 10.1142/S1793525321500722.
  * [16] Kundu, L. Growth of a family of finite simple groups. arXiv:2110.11429v1. (submitted)
  * [17] Glover, H., Sjerve; D. (1985). Representing $PSL_{2}(\mathbb{F}_{p})$ on a Riemann surface of least genus. L’Enseignement Mathematique. t.31(p.305-325.). http://doi.org/10.5169/seals-54572.
  * [18] M.J. Beetham; A set of generators and relations for the group $PSL(2,q),$ q odd. Journal of London Mathematical society, s2-3(3), 554-557.
  * [19] Wolfram Research, Inc., Mathematica, Version 13.0.0, Champaign, IL (2021).