4 Approach: Equivalence Problems as Energy Games
Time to get real. This chapter will demonstrate my core approach by solving the spectroscopy problem in an easy instance.
It will be easy in two regards: Firstly, complexity-wise—we narrow our focus on equivalences of polynomial-time. Secondly, conceptually—we just use the bisimulation game of Chapter 2, almost directly!
We already know that winning attacker strategies in the bisimulation game correspond to distinguishing formulas, and that these can be computed quite straightforwardly. All we need on top of this is a way of quantifying the amount of syntactic expressiveness in these formulas during the game. For this, we employ the first core idea of this chapter:
Spectra of equivalence problems can be encoded as energy games.
Energy games are games in which players have limited resources that can be used up or recharged during moves. Players running out of a resource lose the game. After introducing such games in Section 4.1, we will prove in Section 4.2 that several core equivalences can be characterized as defender’s winning energy budgets by adding three-dimensional energies to the bisimulation game.
The second core idea is how to compute these winning budgets:
Attacker’s winning budgets in energy reachability games can be computed by a generalized shortest paths algorithm.
Section 4.3 will provide an algorithm to solve a range of energy-game-like quantitative problems as long as the energy updates can be undone through a Galois connection, which is a generalization of invertibility on monotonic functions.
By combining the two contributions, we arrive at a polynomial-time solution of the spectroscopy problem for the polynomial slice of the strong spectrum.
Effectively, we adapt the game framework of Figure 2.13 to not treat one equivalence, but a spectrum of equivalences. This approach is summarized in Figure 4.1.
4.1 Energy Games
Energy games extend games as discussed in Section 2.4 with resources of the players, called energies. We will focus on reachability games with an energy-bounded attacker. In most publications, energy games update vector-valued energy levels by vector addition or subtraction. We work with more general monotonic energy games (Subsection 4.1.1) and then zoom in on declining energy games (Subsection 4.3), which include updates that combine vector components by taking their minimum. The latter are exactly what we need for the following Section 4.2.
4.1.1 Monotonic Energy Games
To introduce energy games, we generalize the definitions on games (Definition 2.15 and the following) to include energy levels. We define how winning regions then become quantitative winning budgets, which can still be characterized inductively.
Definition 4.1 (Energy Reachability Game) Given a partially ordered set of energies (\mathcal{E}, \leq), an energy reachability game \mathcal{G}^🗲 is a reachability game (G, G_{\mathrm{d}}, \mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}) extended by an edge labeling of energy updates \mathcal{upd}\colon (\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}) \to (\mathcal{E}\to (\{⊥\} ∪ \mathcal{E})).
We demand the following for monotonic energy games:
- ⊥ \notin \mathcal{E} is final in the sense that \mathcal{upd}(m)(⊥) = ⊥.
- All update functions u =\mathcal{upd}(m) with m \in {\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}} are monotonic and upward-closed with respect to \leq. More formally, this means that for any energies e, e' \in \mathcal{E}, if e \in \operatorname{\mathrm{dom}}(u) and e \leq e', then e' \in \operatorname{\mathrm{dom}}(u) and u(e) \leq u(e'), where \operatorname{\mathrm{dom}}(u) := \{e ∈ \mathcal{E}\mid u(e) \neq \bot\}.
We denote by \mathcal{G}^🗲(g_0, e_0) the game played from starting position g_0 ∈ G with initial energy level e_0 ∈ \mathcal{E}.
Definition 4.2 (Energy Level) For a finite play ρ = {g_0}{g_1}…{g_{n-1}} ∈ G^{*} of \mathcal{G}^🗲(g_0, e_0), its energy level \operatorname{EL}(ρ) is computed recursively:
- \operatorname{EL}(g_0) ≔ e_0
- \operatorname{EL}(g_0…{g_{i+1}}) ≔ \mathcal{upd}({g_{i}},{g_{i+1}})(\operatorname{EL}(g_0…{g_{i}}))
For infinite plays ρ ∈ G^ω, we define energy levels to equal ⊥.
We consider the attacker to be energy-bounded and understand \operatorname{EL}(ρ) = ⊥ to mean that they have run out of energy. Thus, we declare plays with \operatorname{EL}(ρ) = ⊥ to be won by the defender (even if they are stuck).
Strategies and winning strategies work exactly as in the energy-less scenario. Additionally, we lift positional strategies of Definition 2.17 to be energy-positional in the sense that they pick next moves depending on the current energy level, i.e. \mathcal{f} \colon G_{\mathrm{a}}× \mathcal{E}\to G.
Instead of a winning region as in Definition 2.18, we define winning budgets for game positions:
Definition 4.3 (Winning Budgets) For each position g_0 ∈ G of energy game \mathcal{G}^🗲, the attacker winning energy budgets, \mathsf{Win}_\mathrm{a}(g_0) \subseteq \mathcal{E} are the energies e_0 where the attacker wins \mathcal{G}^🗲(g_0, e_0). The defender winning budgets \mathsf{Win}_\mathrm{d} are defined analogously.
Classical energy games use \mathbb{N}-vectors for energies and vector addition for updates as in the following example:
Example 4.1 Consider vector energies \mathcal{E}= \mathbb{N}^2 with point-wise order and the energy game with graph in Figure 4.2. Edges are labeled by update vectors \vec{u} ∈ \mathbb{Z}^2, each representing an update function e \mapsto \begin{cases} e + \vec{u} & \text{if } e + \vec{u} \geq \mathbf{0}\\ ⊥ & \text{otherwise.} \end{cases} Can the attacker win from \mathsf{g_1} with energy (0,0)?
No, as all outgoing paths would lead to ⊥-energy and thus to the defender winning.
But if the attacker starts with budget (0,2), they can take the upper path to \mathsf{g_4} with energy (2,1), from where both defender options lead to the defender being stuck in \mathsf{g_6}.
Also, if the attacker starts with (2,1), they win through the lower \mathsf{g_3}-path.
Moving to \mathsf{g_4} directly, would be more expensive than the \mathsf{g_2}/\mathsf{g_3}-alternatives—so we can disregard this option.
Starting with less energy means that the defender has an option of bankrupting the attacker at \mathsf{g_4}.
Summing up our observations, (0,2) and (2,1) define a Pareto front of minimal budgets where the attacker wins from \mathsf{g_4}, as depicted in Figure 4.3.
We can notice two things from the example:
- A purely positional strategy would not suffice for the defender to win reliably at \mathsf{g_4}. Say the game starts with energy (1,1), that is, with a budget where the defender should win. Then, the level with either be (0,1) or (3,0) at \mathsf{g_4}. The defender has to either move to \mathsf{g_5} or \mathsf{g_6}, depending on the play so far. So, either the defender must know the history, or at least the current energy level to make an ideal decision.
- Attacker’s winning budgets are upward-closed, and defender budgets are downward-closed.
Both are effects of Definition 4.1. More formally, the winning budgets are characterized by the following two propositions:
Proposition 4.1 Given an energy game \mathcal{G}, the attacker winning budgets \mathsf{Win}_\mathrm{a}^{\mathcal{G}} are point-wise upward-closed, that is, {}\uparrow\mathsf{Win}_\mathrm{a}^{\mathcal{G}}(g) = \mathsf{Win}_\mathrm{a}^{\mathcal{G}}(g) for all positions g \in G.1
1 This is formalized as Lemma 3.2 in Lemke (2024).
Proposition 4.2 Given an energy game \mathcal{G}, the attacker winning budgets \mathsf{Win}_\mathrm{a}^{\mathcal{G}} are characterized inductively by the following rules:2 \dfrac{ g_{\mathrm{a}}∈ G_{\mathrm{a}}\quad g_{\mathrm{a}}\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}g' \quad \mathcal{upd}(g_{\mathrm{a}}, g')(e) ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}}(g') } { e ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}}(g_{\mathrm{a}}) } \dfrac{ g_{\mathrm{d}}∈ G_{\mathrm{d}}\quad \forall u,g' \ldotp \; g_{\mathrm{d}}\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}g' \longrightarrow \mathcal{upd}(g_{\mathrm{d}}, g')(e) ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}}(g') } { e ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}}(g_{\mathrm{d}}) }
2 Proved as Theorem 3 in Lemke (2024).
The inductive definition is nice as it allows for local proves of how the attacker wins. Defender’s wins on the other hand would dually be a coinductive concept because the defender wins loops.3
3 By the way, to those wondering: It is intentional that this thesis aims to achieve all its constructions without recurring to coinduction. Therefore, coinduction is only mentioned in side remarks and is not required to understand what is going on.
Remark 4.1. Ordinary reachability games can be seen as a special case of energy games with trivial energies, e.g. \mathcal{E}= \{1\} and \mathcal{upd}(\cdot) = \mathrm{id}_{\mathcal{E}}.
Remark 4.2. We deviate in two important points from other work on energy games:
- In the literature, it is more common to consider the defender instead of the attacker to be energy-bounded (e.g. Fahrenberg et al., 2011). This choice follows the intuition that there is a party with scarce resources that wants to keep the system running. For our purposes, however we want to bound the resources of an attacker, which is no fundamental change. Still, one cannot have both at the same time: Kupferman & Shamash Halevy (2022), studying both-bounded energy games, establish that their winner is only decidable if both parties have only one-dimensional energies.
- We define energy-reachability games more abstractly than is common: In other publications, energy games work on numbers with component-wise updates as seen in Example 4.1. We do not demand this as, in the next sections, we will need updates that combine information from different components of the energy vector. Even prior generalizations on energy update functions such as Ésik et al. (2013) do not allow sufficient flexibility in this regard.
4.1.2 Declining Energy Games
We now turn to special kind of monotonic energy games with vector-valued energy levels where updates will never increase energy levels in any component. An N-dimensional declining energy game is played on energy vectors:
Definition 4.4 (Energies and Energy Updates) For dimensionality N, the set of energies, \mathbf{En}, is given by (\mathbb{N}∪ \{\infty\})^N.
The set of energy update labels, \mathbf{Up}, contains ({u}_1,\ldots,{u}_{N}) ∈ \mathbf{Up} where each component u_k is a symbol of the form
- u_k ∈ \{-1, 0\} (relative update), or
- u_k = \mathtt{min}_D where D \subseteq \{1, \ldots, N\} and k ∈ D (minimum selection update).
Applying an update to an energy, \mathsf{upd}(u, e), where e = ({e}_1,\ldots,{e}_{N}) ∈ \mathbf{En} and u = ({u}_1,\ldots,{u}_{N}) ∈ \mathbf{Up}, yields a new energy vector e' where kth components e'_k ≔ e_k + u_k for u_k ∈ \mathbb{Z} and e'_k ≔ \min_{d∈ D} e_d for u_k = \mathtt{min}_D. Updates that would cause any component to become negative yield \bot.
Example 4.2 Consider the update label (\mathtt{min}_{\{\!1,2\!\}},0,-1).
- \mathsf{upd}((\mathtt{min}_{\{\!1,2\!\}},0,-1), (1,1,0)) equals \bot because of the last component.
- \mathsf{upd}((\mathtt{min}_{\{\!1,2\!\}},0,-1), (2,1,1)) equals (1,1,0).
- \mathsf{upd}((\mathtt{min}_{\{\!1,2\!\}},0,-1), (1,1,1)) equals (1,1,0), as well.
- There is no e ∈ \mathbf{En} such that \mathsf{upd}((\mathtt{min}_{\{\!1,2\!\}},0,-1), e) = (1,0,0), because the second component would demand a lower first component.
In summary, \mathsf{upd}((\mathtt{min}_{\{\!1,2\!\}},0,-1), \cdot) is neither injective nor surjective with respect to \mathbf{En}. The same is true for most other u and \mathsf{upd}(u, \cdot) with a \mathtt{min}-update component.
Definition 4.5 (Declining Energy Game) Given a weight labeling w \colon (\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}) \to \mathbf{Up}, an N-dimensional declining energy game \mathcal{G}^🗲 is an energy reachability game with energies \mathcal{E}≔ \mathbf{En} and with edges labeled \mathcal{upd}(m) ≔ \mathsf{upd}(w(m), \cdot).
We write g \mathrel{\smash{›\!\!\frac{\;u\;}{}\!\!›}} g' for a move g \mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}g' labeled by weight w(g, g') = u.
Declining energy games differ from more common energy games with vector addition updates as seen in Example 4.1 due to the non-invertibility of updates we encountered in Example 4.2.
Proposition 4.3 In this model, energy levels can only decline.
- Updates may only decrease energies, \mathsf{upd}(u, e) \leq e.
- Updates are monotonic as demanded: If e_A \leq e_B, then \mathsf{upd}(u, e_A) \leq \mathsf{upd}(u, e_B).<
4.2 Characterizing the \textsf{P}-Time Part of the Spectrum
As hinted at in Subsection 3.3.3, parts of the strong equivalence spectrum can be decided in polynomial time, whereas others require polynomial space (and thus effectively exponential time). In this section, we will show how to adapt the standard bisimulation game of Definition 2.20 to decide not just bisimulation, but all polynomial-time equivalences of the strong spectrum at once.
4.2.1 The Polynomial Slice
First, let us make explicit which equivalences we include in the polynomial-time slice of the spectrum. (The fact that they indeed can be decided efficiently is mostly well-known, but also itself a corollary of this section.)
To define the polynomial slice, we only use three dimensions:
- modal depth
- depth of negative clauses, and
- nesting depth of negations (that is, the first, fifth and sixth dimension of the strong spectrum Definition 3.7).
Components for other dimensions of the strong spectrum of the previous chapter are effectively set to ∞.
Definition 4.6 (Polynomial-Time Strong Spectrum) We denote as polynomial-time strong spectrum the projection of the strong spectrum (Definition 3.7) to the first, fifth, and sixth dimension, thus by notions \mathbf{N}^\mathsf{poly-strong} ≔ \mathbb{N}_\infty^3, and the family of strong observation languages \mathcal{O}_{(N_1, N_2, N_3) ∈ \mathbf{N}^\mathsf{poly-strong}}^\mathsf{poly-strong} ≔ \mathcal{O}_{(N_1,∞,∞,∞,N_2,N_3)}^\mathsf{strong}.
In effect, \mathcal{O}_{N ∈ \mathbf{N}^\mathsf{poly-strong}} can be characterized by φ^N in the following grammar: \begin{array}{rcll} φ^N & \;::=\;& \top{} & \\ & \;\mid\;& \langle α \rangle φ^{N - \mathbf{\hat{e}}_{1}} & \\ & \;\mid\;& \textstyle\bigwedge \{ψ^N, ψ^N, ψ^N \ldots\} & \\ ψ^N & \;::=\;& \langle α \rangle φ^{N - \mathbf{\hat{e}}_{1}} & \\ & \;\mid\;& \neg\langle α \rangle φ^{(N \sqcap (N_2, \infty, \infty))- \mathbf{\hat{e}}_{1} - \mathbf{\hat{e}}_{3}} & \\ \end{array} Figure 4.4 gives names to coordinates that correspond to notions discussed previously.
Except for enabledness, \mathrm{E}, all coordinates after unfolding them for \mathbf{N}^\mathsf{strong} are identical to the ones used previously. When one unfolds the coordinate for enabledness (1,0,0) to the original strong system, (1,∞,∞,∞,0,0), it differs from the one previously used, namely, (1,0,0,0,0,0). The characterized language is strictly more expressive, as it contains conjunctions of enabled actions (e.g. \textstyle\bigwedge \{\langle \mathsf{a} \rangle, \langle \mathsf{b} \rangle\}), but it is equally distinctive.4
4.2.2 The Bisimulation Energy Game
Let us upgrade the bisimulation game of Definition 2.20 with energies. The claim is that the resulting game {\mathcal{G}}_\mathrm{B}^🗲 will characterize all equivalences of the polynomial-time strong spectrum in the sense that p \preceq_{\mathcal{O}_{e}} q for e ∈ \mathbf{N}^\mathsf{poly-strong} precisely if the defender wins {\mathcal{G}}_\mathrm{B}^🗲 from [p, q] with budget e.
As we have seen in Subsection 2.4.4, the game moves match the distinctive power of productions in the \mathcal{O}_\mathrm{\lfloor B \rfloor}-grammar of Example 2.11. Consequently, we can count the use of HML constructs in the game. As the game stands, we can meaningfully count the three dimensions used in Subsection 4.2.1.5
5 We cannot hope to count the other dimensions of Definition 3.7: the bisimulation game washes away the amount of necessary conjunctions as its HML has conjunctions under each observation, even though they might not be necessary for a distinguishing formula.
We add the computations that happen in the grammar of Definition 4.6 as energy updates to the bisimulation game and obtain:
Definition 4.7 (Bisimulation Energy Game) For a transition system \mathcal{S}, the bisimulation energy game {\mathcal{G}}_\mathrm{B}^{🗲\mathcal{S}} is played on the same graph as the bisimulation game {\mathcal{G}}_\mathrm{B}^{\mathcal{S}} (of Definition 2.20), but the moves are weighted by the following energy updates:
- Attacker swaps are counted as a negation and limit the further observations to the depth of negative clauses: [p, q] \quad \mathrel{\smash{›\!\!\frac{\mathtt{min}_{\{\!1,2\!\}},0,-1}{}\!\!›}}^🗲_\mathrm{B} \quad [q, p].
- Simulation challenges count as an observation (using up the budget for modal depth): [p, q] \quad \mathrel{\smash{›\!\!\frac{-1,0,0}{}\!\!›}}^🗲_\mathrm{B} \quad (α, p', q) \quad \text{if} \quad p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{α}$}}} p'.
- And defender answers come for free: (α, p', q) \quad \mathrel{\smash{›\!\!\frac{0,0,0}{}\!\!›}}^🗲_\mathrm{B} \quad [p', q'] \quad \text{if} \quad q \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{α}$}}} q'.
The first dimension thus bounds how often the attacker may challenge simulation down the road, the third limits how often they may swap sides, and the middle dimension bounds the amount of simulation moves after a swap.
Example 4.3 Let us label the bisimulation game of Example 2.18 (distinguishing the “trolled philosophers”) with energy updates. Figure 4.5 shows the game graph, also exhibiting the cheapest formulas with regards to the polynomial spectrum that correspond to attacker winning strategies.
The attacker wins {\mathcal{G}}^🗲_\mathrm{B} from [\mathsf{Q}, \mathsf{T}] if they start out with an energy budget of (2,2,2) or above. But if the budget does not dominate this bound, the attacker loses. For instance, neither (1,\infty,\infty) nor (\infty,\infty,1) is enough. The second bound implies that the budgets, (\infty,1,1) and (\infty,0,0) are won by the defender as well.
On the game-side, this tells us is that the attacker needs at least two simulation moves (after swaps) and two swaps to tell \mathsf{Q} apart from \mathsf{T}. Telling apart \mathsf{T} from \mathsf{Q} is slightly easier, only requiring one swap (and only one simulation move after the swap).
But, due to the correspondence of the game to modal formulas and of the energy updates to the pricing of formulas in the spectrum, the attacker winning budgets tell us more: They reveal that one needs two observations and two (or more) negations to distinguish \mathsf{Q} from \mathsf{T} using formulas from \mathcal{O}_\mathrm{\lfloor B \rfloor}.
Thus, \mathbf{N}^{\mathsf{poly-strong}}_{\mathsf{Q}, \mathsf{T}} = \{N ∈ \mathbf{N}^\mathsf{poly-strong} \mid N \nleq (2,2,2)\} is the solution for the (polynomial-time strong) spectroscopy problem. \mathsf{Q} is preordered to \mathsf{T} by 2-nested simulation, 1-step bisimulation, and all notions below; but distinguished by all above, in particular, 3-nested simulation and 2-step bisimulation.
This is in line with the solution we thought of for the original strong spectrum in Example 3.6.
4.2.3 Correctness of Characterization
We now prove that the bisimulation energy game indeed characterizes the equivalences of the polynomial-time strong spectrum. In following chapters, we will prove stronger results for more general games in more detail. The approach is to generalize the connection between winning attacks and distinguishing formulas that we have already explored in Lemma 2.10 and Lemma 2.11 to energies and spectrum.
Definition 4.8 (Strategy Formulas for {\mathcal{G}}_\mathrm{B}^{🗲}) The set of strategy formulas for a game position g and a budget e, \mathsf{Strat}_\mathrm{B}(g, e), in the context of a bisimulation energy game {\mathcal{G}}_\mathrm{B}^{🗲\mathcal{S}} is defined inductively by the following rules: \dfrac{ [p, q] \mathrel{\smash{›\!\!\frac{-1,0,0}{}\!\!›}}^🗲_\mathrm{B} (α, p', q) \quad e' = \mathsf{upd}((-1,0,0), e) ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_\mathrm{B}^🗲}((α, p', q)) \quad φ ∈ \mathsf{Strat}_\mathrm{B}((α, p', q), e') }{ (\langle α \rangle φ) ∈ \mathsf{Strat}_\mathrm{B}([p, q], e) } \dfrac{ \forall q' ∈ \operatorname{Der}(q, α) \ldotp \quad (α, p', q) \mathrel{\smash{›\!\!\frac{0,0,0}{}\!\!›}}^🗲_\mathrm{B} [p', q'] \; \land \; e ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_\mathrm{B}^🗲}([p', q']) \; \land \; ψ_{q'} ∈ \mathsf{Strat}_\mathrm{B}([p', q'], e) }{ (\textstyle\bigwedge_{q' \in \operatorname{Der}(q, α)} ψ_{q'}) ∈ \mathsf{Strat}_\mathrm{B}((α, p', q), e) } \dfrac{ [p, q] \mathrel{\smash{›\!\!\frac{\mathtt{min}_{\{\!1,2\!\}},0,-1}{}\!\!›}}^🗲_\mathrm{B} [q, p] \quad e' = \mathsf{upd}((\mathtt{min}_{\{\!1,2\!\}},0,-1), e) ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_\mathrm{B}^🗲}([q, p]) \quad \langle α \rangle φ ∈ \mathsf{Strat}_\mathrm{B}([q, p], e') }{ (\neg\langle α \rangle φ) ∈ \mathsf{Strat}_\mathrm{B}([p, q], e) }
Effectively, this definition generalizes the construction of distinguishing formulas on {\mathcal{G}}_\mathrm{B} we introduced in Lemma 2.10. So the formulas we encountered before also serve as examples of such strategy formulas.
Lemma 4.1 If e ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_\mathrm{B}^🗲}([p, q]), then there is φ ∈ \mathsf{Strat}_\mathrm{B}([p, q], e) with φ ∈ \mathcal{O}_{e}^\mathsf{poly-strong}, p ∈ \llbracket φ \rrbracket and q \notin \llbracket φ \rrbracket.
Proof. We prove the following, more general, property by induction.
- If e ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_\mathrm{B}^🗲}([p, q]), then there is ψ ∈ \mathsf{Strat}_\mathrm{B}([p, q], e) of form ψ = \langle α \rangle φ' or \neg\langle α \rangle φ' with \textstyle\bigwedge \{ψ\} ∈ \mathcal{O}_{e}^\mathsf{poly-strong}, p ∈ \llbracket ψ \rrbracket and q \notin \llbracket ψ \rrbracket.
- If e ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_\mathrm{B}^🗲}((α, p', q)), then there is φ ∈ \mathsf{Strat}_\mathrm{B}((α, p', q), e) of form φ = \textstyle\bigwedge Ψ with φ ∈ \mathcal{O}_{e}^\mathsf{poly-strong}, p' ∈ \llbracket φ \rrbracket and q \notin \llbracket \langle α \rangle φ \rrbracket.
Proof by induction on the inductive characterizations of attacker winning budgets Proposition 4.2.
- Assume e ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_\mathrm{B}^🗲}([p, q]). This must be due to one of the following moves:
- Case [p, q] \mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}^🗲_\mathrm{B} [q, p] with e' = \mathsf{upd}((\mathtt{min}_{\{\!1,2\!\}},0,-1), e) ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_\mathrm{B}^🗲}([q, p]). By induction hypothesis on [q, p], there is ψ ∈ \mathsf{Strat}_\mathrm{B}([q, p], e') with \textstyle\bigwedge \{ψ\} ∈ \mathcal{O}_{e'}^\mathsf{poly-strong}, q ∈ \llbracket ψ \rrbracket and p \notin \llbracket ψ \rrbracket. Consider the possible forms of ψ:
- ψ = \langle α \rangle φ'. By Definition 4.8 of \mathsf{Strat}_\mathrm{B}, we obtain \neg\langle α \rangle φ' ∈ \mathsf{Strat}_\mathrm{B}([p, q], e). Because of the semantics of \textsf{HML}, \neg\langle α \rangle φ' must distinguish p from q. Also, \textstyle\bigwedge \{\neg\langle α \rangle φ'\} ∈ \mathcal{O}_{e}^\mathsf{poly-strong}, by the calculations of the grammar in Definition 4.6.
- ψ = \neg\langle α \rangle φ'. This can only be in \mathsf{Strat}_\mathrm{B}([q, p], e') due to φ' being in \mathsf{Strat}_\mathrm{B}([p, q], \mathsf{upd}((\mathtt{min}_{\{\!1,2\!\}},0,-1), e')). Clearly, φ' must distinguish p from q and \textstyle\bigwedge \{φ'\} ∈ \mathcal{O}_{e}^\mathsf{poly-strong}.
- Case [p, q] \mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}^🗲_\mathrm{B} (α, p', q) with p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{α}$}}} p' and e' = \mathsf{upd}((-1,0,0), e) ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_\mathrm{B}^🗲}((α, p', q)). By induction hypothesis on (α, p', q), there is \textstyle\bigwedge Ψ ∈ \mathsf{Strat}_\mathrm{B}((α, p', q), e') and \textstyle\bigwedge Ψ ∈ \mathcal{O}_{e'}^\mathsf{poly-strong} with p' ∈ \llbracket \textstyle\bigwedge Ψ \rrbracket and q \notin \llbracket \langle α \rangle\textstyle\bigwedge Ψ \rrbracket. By Definition 4.8, we obtain \langle α \rangle\textstyle\bigwedge Ψ ∈ \mathsf{Strat}_\mathrm{B}([p, q], e). Due to the semantics of \textsf{HML} and p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{α}$}}} p', p ∈ \llbracket \langle α \rangle\textstyle\bigwedge Ψ \rrbracket, thus distinguishing p from q. Also, \langle α \rangle\textstyle\bigwedge Ψ ∈ \mathcal{O}_{e}^\mathsf{poly-strong} as \textstyle\bigwedge Ψ ∈ \mathcal{O}_{e - \mathbf{\hat{e}}_{1}}^\mathsf{poly-strong}.
- Case [p, q] \mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}^🗲_\mathrm{B} [q, p] with e' = \mathsf{upd}((\mathtt{min}_{\{\!1,2\!\}},0,-1), e) ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_\mathrm{B}^🗲}([q, p]). By induction hypothesis on [q, p], there is ψ ∈ \mathsf{Strat}_\mathrm{B}([q, p], e') with \textstyle\bigwedge \{ψ\} ∈ \mathcal{O}_{e'}^\mathsf{poly-strong}, q ∈ \llbracket ψ \rrbracket and p \notin \llbracket ψ \rrbracket. Consider the possible forms of ψ:
- Assume e ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_\mathrm{B}^🗲}((α, p', q)). This means that e suffices for the attacker to win every q'-move (α, p', q) \mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}^🗲_\mathrm{B} [p', q'] with q \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{α}$}}} q' that the defender might take, with e ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_\mathrm{B}^🗲}([p', q']). For each q', we employ the induction hypothesis to obtain ψ_{q'} ∈ \mathsf{Strat}_\mathrm{B}([p', q'], e) of form ψ_{q'} = \langle α \rangle φ' or \neg\langle α \rangle φ' with \textstyle\bigwedge \{ψ_{q'}\} ∈ \mathcal{O}_{e}^\mathsf{poly-strong}, p' ∈ \llbracket ψ_{q'} \rrbracket and q' \notin \llbracket ψ_{q'} \rrbracket. By Definition 4.8, (\textstyle\bigwedge_{q' \in \operatorname{Der}(q, α)} ψ_{q'}) ∈ \mathsf{Strat}_\mathrm{B}((α, p', q), e). By the \textsf{HML}-semantics, (\textstyle\bigwedge_{q' \in \operatorname{Der}(q, α)} ψ_{q'}) must be true for p', and also taking the semantics of observation, \langle α \rangle(\textstyle\bigwedge_{q' \in \operatorname{Der}(q, α)} ψ_{q'}) false for q. Moreover, (\textstyle\bigwedge_{q' \in \operatorname{Der}(q, α)} ψ_{q'}) ∈ \mathcal{O}_{e}^\mathsf{poly-strong} by the grammar.
Lemma 4.2 If there is φ ∈ \mathcal{O}_{e}^\mathsf{poly-strong} with p ∈ \llbracket φ \rrbracket and q \notin \llbracket φ \rrbracket, then e ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_\mathrm{B}^🗲}([p, q]).
Proof. By induction on the grammar of \mathcal{O}_{e}^{\mathsf{poly-strong}}.
Consider the cases of φ ∈ \mathcal{O}_{e}^\mathsf{poly-strong} with p ∈ \llbracket φ \rrbracket and q \notin \llbracket φ \rrbracket.
- φ = \top. This cannot be the case as q \notin \llbracket φ \rrbracket and \llbracket \top \rrbracket = \mathcal{P}.
- φ = \langle α \rangle φ' with φ' ∈ \mathcal{O}_{e - \mathbf{\hat{e}}_{1}}^\mathsf{poly-strong}. As φ distinguishes p from q, there must be a p' ∈ \llbracket φ' \rrbracket such that p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{α}$}}} p' and, for all q' ∈ \operatorname{Der}(q, α), q' \notin \llbracket φ' \rrbracket. Due to the induction hypothesis, e - \mathbf{\hat{e}}_{1} ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_\mathrm{B}^🗲}([p', q']) for all such q' ∈ \operatorname{Der}(q, α). Therefore, e - \mathbf{\hat{e}}_{1} ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_\mathrm{B}^🗲}((α, p', q)). As the attacker can move [p, q] \mathrel{\smash{›\!\!\frac{-\mathbf{\hat{e}}_{1}}{}\!\!›}} (α, p', q), this proves e ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_\mathrm{B}^🗲}([p, q]) by Proposition 4.2.
- φ = \textstyle\bigwedge \setΨ one of the ψ ∈ Ψ must be false for q. Consider the possible forms of ψ:
- Case ψ = \langle α \rangle φ' with φ' ∈ \mathcal{O}_{e - \mathbf{\hat{e}}_{1}}^\mathsf{poly-strong}. Then we can apply the same argument as in the case of φ = \langle α \rangle φ'.
- Case ψ = \neg\langle α \rangle φ' with φ' ∈ \mathcal{O}_{(e \sqcap (e_2, \infty, \infty)) - \mathbf{\hat{e}}_{1} - \mathbf{\hat{e}}_{3}}^\mathsf{poly-strong}. Therefore, \langle α \rangle φ' ∈ \mathcal{O}_{(e \sqcap (e_2, \infty, \infty)) - \mathbf{\hat{e}}_{3}}^\mathsf{poly-strong} distinguishes q from p. This time, we can employ the same argument as in the case of φ = \langle α \rangle φ' to obtain that (e \sqcap (e_2, \infty, \infty)) - \mathbf{\hat{e}}_{3} ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_\mathrm{B}^🗲}([q, p]). The move [p, q] \mathrel{\smash{›\!\!\frac{\mathtt{min}_{\{\!1,2\!\}},0,-1}{}\!\!›}}^🗲_\mathrm{B} [q, p] and \mathsf{upd}((\mathtt{min}_{\{\!1,2\!\}},0,-1), e) = (e \sqcap (e_2, \infty, \infty)) - \mathbf{\hat{e}}_{3} justify that e ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_\mathrm{B}^🗲}([p, q]).
Theorem 4.1 p \preceq_{\mathcal{O}_{e}} q for e ∈ \mathbf{N}^\mathsf{poly-strong} precisely if the defender wins {\mathcal{G}}_\mathrm{B}^🗲 from [p, q] with budget e.
Thus, we have established that the bisimulation energy game {\mathcal{G}}_\mathrm{B}^🗲 characterizes the equivalences of the polynomial-time strong spectrum \mathbf{N}^\mathsf{poly-strong}. To exploit this property to decide equivalences and solve the spectroscopy problem algorithmically, we need one more ingredient: A decision procedure for winning budgets in declining energy games.
4.3 Deciding Energy Games
This section is about how to compute which energy budgets are winning for the attacker (or the defender) at positions of an energy game:
Definition 4.9 (Monotonic Energy Game Winner Problem) In the context of an energy system (\mathcal{E}, \leq) and a finite energy game \mathcal{G}^🗲=(G,G_{\mathrm{d}},\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}, \mathcal{upd}), the energy game winner problem goes:
- Input
- Game position g ∈ G.
- Output
- \mathsf{Win}^{\mathrm{min}}_\mathrm{a}(g)—the Pareto front of minimal winning budgets for the attacker at g.
We will show how to solve the problem for energy games with monotonic updates. To this end, we will adapt the idea of back-propagating how the defender loses in reachability games from Algorithm 2.1.
The change is that we have to propagate not just attacker wins, but Pareto fronts of attacker-winning energy levels. For this, we have to “invert” the energy update functions. But, as we have seen in Example 4.2, our specific declining energy updates are neither injective nor surjective, and thus cannot be cleanly inverted.
We will see how to tackle these challenges using Galois connections. For details, readers are referred to Lemke (2024).
4.3.1 Galois Connections
Galois connections can be thought of as a pair of monotonic functions that invert each other up to their partial ordering relations. Another standard intuition is that Galois connections couple a concrete and a more abstract domain, and this is what the variable naming in the following definition alludes to.
Definition 4.10 A Galois connection between two partially ordered sets (C, \leq_C) and (A,\leq_A) is a pair of functions α \colon C \to A and \gamma \colon A \to C such that, for all a ∈ A and c ∈ C: α(c) \leq_A a \iff c \leq_C \gamma(a).
An illustration of the connection property can be seen in Figure 4.7. (The illustration also illuminates why the α-function is often referred to as “lower adjoint“ and \gamma as “upper adjoint” of a Galois connection.)
Example 4.4 Take the non-negative reals \mathbb{R}^{\geq 0} as concrete domain and the natural numbers \mathbb{N} as abstract domain. Then, as function α_{\mathbb{R}} \colon \mathbb{R}^{\geq 0} \to \mathbb{N}, take flooring, x \mapsto \lfloor x \rfloor, and for the other direction, the identity \mathrm{id}_{\mathbb{N}}, n \mapsto n. Clearly, \lfloor x \rfloor \leq n \iff x \leq n. Therefore, α_{\mathbb{R}} and \mathrm{id}_{\mathbb{N}} form a Galois connection.
Any monotonic function naturally induces a Galois-connected abstraction function.
Lemma 4.3 The following are equivalent:
- \gamma \colon A \to C is a monotonic function, and α(c) = \inf \{a \mid c \leq_C \gamma(a)\} for all c ∈ C.
- α and \gamma constitute a Galois connection between C and A.6
6 Proposition 4 of Erné et al. (1993).
We will refer to functions derived like α(c) in Lemma 4.3 as “undo” functions. We understand them to generalize inverse functions of monotonic functions as these will always be Galois connected.
Lemma 4.4 If a function f \colon A \to C is surjective and injective, it has a unique inverse function f^{-1} \colon C \to A such that f^{-1} \circ f = \mathrm{id}_{A} and f \circ f^{-1} = \mathrm{id}_{C}.
If f is monotonic with respect to some partial orders on C and A, then f^{-1} and f must form a Galois connection.
Proof. Because of injectivity and monotonicity, f and f^{-1}, must be (strictly) monotonic. Together with the definition of function inversion, we can reason f(c) \leq_A a \implies f^{-1}(f(c)) \leq_A f^{-1}(a) \implies c \leq_C f^{-1}(a) and c \leq_C f^{-1}(a) \implies f(c) \leq_A f(f^{-1}(a)) \implies f(c) \leq_A a.
In the following, we will use a ↺-symbol to label the adjoint functions that we use to undo energy updates.
Remark 4.3. Definition 3.5 demands monotonicity of our observation languages for a spectrum, \mathcal{O}_{N \in \mathbf{N}}. If we construct an abstraction function as in Lemma 4.3 to undo the language selection for a set of formulas \Phi, the result would read: \alpha_{\mathcal{O}_\mathrm{}}(\Phi) := \inf \{N \in \mathbf{N}\mid \Phi \subseteq \mathcal{O}_{N}\}. The singleton case of this function exactly matches our expressiveness prices of Definition 3.6: \mathsf{expr}(\varphi) := \inf \{N \in \mathbf{N}\mid \varphi \in \mathcal{O}_{N}\}.
4.3.2 The Algorithm
To implement a back-propagation algorithm, we have to assume that we know a function that undoes energy updates, \mathcal{upd}^{↺}\colon (\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}) \to \mathcal{E}\to \mathcal{E} with \mathcal{upd}^{↺}(g, g')(e') = \inf \{e \mid e' \leq \mathcal{upd}(g, g')(e)\}. That means, we assume that there is a Galois connection (\mathcal{upd}^{↺}, \mathcal{upd}) between energies \mathcal{E} and the domain of updates \{e ∈ \mathcal{E}\mid \mathcal{upd}(e) \neq \bot\}.
Algorithm 4.1 can be used to compute the minimal attacker winning budgets.
\begin{array}{rl} 1 & \operatorname{\mathbf{def}}\; \mathtt{compute\_winning\_budgets}(\mathcal{G}^🗲=(G,G_{\mathrm{d}},\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}, \mathcal{upd}), \mathcal{upd}^{↺}) \colon \\ 2 & \quad \mathtt{attacker\_win} := [ g \mapsto \varnothing \mid g ∈ G ] \\ 3 & \quad \mathtt{todo} := \{g ∈ G_{\mathrm{d}}\mid g \mathrel{\smash{{›/\!\!\!\!\frac{\quad}{\;}\!\!›}}}\} \\ 4 & \quad \operatorname{\mathbf{while}}\; \mathtt{todo} \neq \varnothing \colon \\ 5 & \quad \quad \mathtt{g} := \operatorname{\mathbf{some}}\; \mathtt{todo} \\ 6 & \quad \quad \mathtt{todo} := \mathtt{todo} \mathbin{\backslash}\{\mathtt{g}\} \\ 7 & \quad \quad \operatorname{\mathbf{if}}\; \mathtt{g} ∈ G_{\mathrm{a}}\colon \\ 8 & \quad \quad \quad \mathtt{new\_attacker\_win} := \operatorname{\mathrm{Min}}( \{\mathcal{upd}^{↺}(\mathtt{g}, g')(\mathit{e'}) \\ & \quad \quad \quad \quad \mid {\mathtt{g} \mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}g'} \land \mathit{e'} ∈ \mathtt{attacker\_win}[g']\}) \\ 9 & \quad \quad \operatorname{\mathbf{else \colon}}\; \\ 10 & \quad \quad \quad \mathtt{new\_attacker\_win} := \{\mathbf{0}\} \\ 11 & \quad \quad \quad \operatorname{\mathbf{for}}\; \mathtt{g'} ∈ (\mathtt{g} \mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}\cdot) \colon \\ 12 & \quad \quad \quad \quad \mathtt{new\_attacker\_win} := \operatorname{\mathrm{Min}}( \{ \sup(e_{\mathrm{a}}, \mathcal{upd}^{↺}(\mathtt{g}, g')(\mathit{e'})) \mid \\ & \quad \quad \quad \qquad e_{\mathrm{a}}∈ \mathtt{new\_attacker\_win} \land {\mathtt{g} \mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}g'} \land \mathit{e'} ∈ \mathtt{attacker\_win}[g']\} ) \\ 13 & \quad \quad \operatorname{\mathbf{if}}\; \mathtt{new\_attacker\_win} \neq \mathtt{attacker\_win}[\mathtt{g}] \colon \\ 14 & \quad \quad \quad \mathtt{todo} := \mathtt{todo} ∪ (\cdot \mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}\mathtt{g}) \\ 15 & \quad \mathsf{Win}^{\mathrm{min}}_\mathrm{a}:= \mathtt{attacker\_win} \\ 16 & \quad \operatorname{\mathbf{return}}\; \mathsf{Win}^{\mathrm{min}}_\mathrm{a}\\ \end{array}
The algorithm can be understood as a generalization of Algorithm 2.1, but as positions might need to be revisited more than once, we have to depart from the option counting trick. Whenever we learn about a new minimal energy for the attacker to win, we schedule a position to be (re-)visited. The chain-reaction starts at defender positions with no outgoing moves (lines 3 and 10). By \mathbf{0}, we denote the minimal element of the energy system \mathcal{E}.
We illustrate the algorithm by running it on the simple energy game of Example 4.1.
Example 4.5 Let us execute Algorithm 4.1 on the \mathbb{N}^2-game of Example 4.1. The game graph, labeled by the minimal attacker winning energies we find, is reproduced in Figure 4.9.
What we need for the algorithm to run, is some undo function \mathcal{upd}^{↺}\colon (\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}) \to \mathcal{E}\to \mathcal{E}. We define it as: \mathcal{upd}^{↺}(e') := \sup(e - \vec{u}, \mathbf{0}) We list the steps of the computation in Example 4.5, and the mechanics behind them below.
| step | \mathtt{g} | \mathtt{new\_attacker\_win} | \mathtt{todo} |
|---|---|---|---|
| 0 | – | \mathsf{g}_i \mapsto \varnothing | \mathsf{g_6} |
| 1 | \mathsf{g_6} | \{(0,0)\} | \mathsf{g_4}, \mathsf{g_5} |
| 2 | \mathsf{g_4} | \varnothing | \mathsf{g_5} |
| 3 | \mathsf{g_5} | \{(0,1)\} | \mathsf{g_4} |
| 4 | \mathsf{g_4} | \{(1,1)\} | \mathsf{g_1}, \mathsf{g_2}, \mathsf{g_3} |
| 5 | \mathsf{g_1} | \{(3,2)\} | \mathsf{g_2}, \mathsf{g_3} |
| 6 | \mathsf{g_2} | \{(0,2)\} | \mathsf{g_3}, \mathsf{g_1} |
| 7 | \mathsf{g_3} | \{(1,1)\} | \mathsf{g_1} |
| 8 | \mathsf{g_1} | \{(0,2), (2,1)\} | \varnothing |
- The algorithm begins with \mathsf{g_6} in the \mathtt{todo}-set as this is the only position where the defender is stuck.
- Updating the defender node \mathsf{g_6} ∈ G_{\mathrm{d}}, we set it its minimal attacker-winning budget to \mathbf{0}. This means that the attacker wins here with any budget. As there has been a change, both predecessors \mathsf{g_4} and \mathsf{g_5} are added to the \mathtt{todo}. (Their order is undefined; for the sake of the simulation we will always pick the first positions from the \mathtt{todo}.)
- Updating \mathsf{g_4} ∈ G_{\mathrm{d}} finds no attacker wins so far because one successor \mathtt{attacker\_win}[\mathsf{g_5}] = \varnothing.
- \mathsf{g_4} ∈ G_{\mathrm{a}} is updated with the \mathcal{upd}^{↺}((0, -1))((0,0)) = \sup((0,0) - (0,-1), \mathbf{0}) = (0,1). This places \mathsf{g_4} in \mathtt{todo} again.
- Now, we can find attacker winning budgets for \mathsf{g_4} ∈ G_{\mathrm{d}}: The two successor options (after undo-update) are (0,1) and (1,0), as depicted in Figure 4.10. The unless the attacker at least arrives with energy \sup((0,1), (1,0)) = (1,1), the defender has a way of winning. Effectively, this amounts to intersecting attacker winning budgets of possible successor positions.
- For \mathsf{g_1} ∈ G_{\mathrm{a}}, it suffices to know a winning budget for one successor. So we determine as a preliminary winning budget \mathcal{upd}^{↺}((-2, -1))((1,1)) = (3,2).
- \mathsf{g_2} ∈ G_{\mathrm{a}} also derives its winning budget from (1,1). But (1,1) - (2,-1) = (-1,2) would be outside the possible energy levels the attacker could carry here and is thus \sup-ed into \mathbb{N}^2, yielding new win (0,2).
- \mathsf{g_3} ∈ G_{\mathrm{a}} just propagates (1,1) from \mathsf{g_4}.
- Revisiting \mathsf{g_1} ∈ G_{\mathrm{a}}, we can now combine the three Pareto-fronts of its successors as illustrated in Figure 4.11 as \operatorname{\mathrm{Min}}\{(0,2), (2,1), (3,4)\} = \{(0,2), (2,1)\}. This operation corresponds to taking the union of the three sets of attacker winning budgets. The previous minimal budget (3,4) of step 5 is thus superseded. As \mathtt{todo} is empty, the algorithm terminates.
Theorem 4.2 Assume energies form a well-founded bounded \sqcup-semi-lattice (\mathcal{E}, \leq). Given a finite-state energy game \mathcal{G}^🗲=(G,G_{\mathrm{d}},\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}, \mathcal{upd}) with monotonic \mathcal{upd}^{↺}-functions for all moves and with computable undo function \mathcal{upd}^{↺}(g, g')(e') = \min \{e \mid e' \leq \mathcal{upd}(g, g')(e)\}, Algorithm 4.1 computes the Pareto front of minimal attacker winning budgets, solving the monotonic energy game winner problem (Definition 4.9).
Proof. Algorithm 4.1 is a work-list variant of a fixed-point iteration computing the least fixed point of attacker winning budgets \mathsf{Win}_\mathrm{a} according to the inductive characterization of Proposition 4.2.
The “least” here refers to the size of the \mathsf{Win}_\mathrm{a}-sets characterized by the \mathsf{Win}^{\mathrm{min}}_\mathrm{a}-Pareto front.
A detailed proof, employing Kleene’s fixed point theorem, can be found in Lemke (2024). Theorem 5 of Lemke (2024) refers to a variant of Algorithm 4.1, where all game positions are updated simultaneously in each iteration, which aligns more directly with the underlying functor. As is common for graph algorithms, Algorithm 4.1 with updates of single vertices whose neighborhood has changed computes the same result, and usually in a more efficient manner.
4.3.3 Complexity
Thanks to Lemke (2024), we can name quite precise bounds for the running time of the algorithm in terms of size of the game and shape of the energy lattice.
Definition 4.11 The width, \operatorname{wdh}_B(b), of a (semi-)lattice (B, \leq) below a point b is defined as the maximal size of anti-chains B' \subseteq {}\downarrow\{b\}. (Cf. Definition 3.4.)
The height, \operatorname{hgt}_B(b), below b is defined as the size of the maximal size of chains B' \subseteq {}\downarrow\{b\}.
Theorem 4.3 Consider the following parameters of an energy game problem on \mathcal{G}^🗲=(G,G_{\mathrm{d}},\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}, \mathcal{upd}) where the energies at least form a well-founded bounded \sqcup-semi-lattice (\mathcal{E}, \leq):
- t_{\sup}, time to calculate the supremum between two elements of \mathcal{E},
- t_\leq, time to compare two elements of \mathcal{E},
- t_{\mathcal{upd}^{↺}}, time to compute \mathcal{upd}^{↺} on an energy,
- e_{\mathcal{G}}, the highest energy that can be achieved by applying permutations of \mathcal{upd}^{↺}(\cdot) to \mathbf{0} for \left|G\right|-1 times.
- o_{\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}}, the out-degree of the game graph \mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}.
Then, Algorithm 4.1 computes the minimal attacker winning budgets in \mathit{O}( (\left|G\right| + \operatorname{hgt}_{\mathcal{E}}(e_{\mathcal{G}})) \cdot \left|G\right| \cdot o_{\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}} \cdot (\operatorname{wdh}_{\mathcal{E}}(e_{\mathcal{G}}))^2 \cdot (t_{\mathcal{upd}^{↺}} + t_{\sup} + \operatorname{wdh}_{\mathcal{E}}(e_{\mathcal{G}}) \cdot t_\leq) ).
If \mathcal{upd}^{↺} is strictly declining, then the following suffices: \mathit{O}( \left|G\right|^2 \cdot o_{\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}} \cdot (\operatorname{wdh}_{\mathcal{E}}(e_{\mathcal{G}}))^2 \cdot (t_{\mathcal{upd}^{↺}} + t_{\sup} + \operatorname{wdh}_{\mathcal{E}}(e_{\mathcal{G}}) \cdot t_\leq) ). In both cases, the algorithm needs \mathit{O}(\left|G\right| \cdot \operatorname{wdh}_{\mathcal{E}}(e_{\mathcal{G}}) \cdot N) space to store the Pareto fronts.
Proof. As in Theorem 4.2, we refer to Lemke (2024) for a very detailed proof, where the corresponding fact is proved as Theorem 7.
TODO: Add a proof sketch regardless.
4.3.4 Solving Declining Energy Games
Let us instantiate the previous two subsections to declining energy games. All we have to do is instantiate \mathcal{upd}^{↺} to obtain an algorithm and think about the structure of the energies to tell its complexity.
Definition 4.12 The undo-update function \mathsf{upd}^{↺} on an N-dimensional declining energy game is defined component-wise for k \in \{1 … N\} as: \begin{array}{rl} (\mathsf{upd}^{↺}(u, e'))_k := \max( & \{e'_k - u_k \mid u_k \in \{0,-1\}\} \\ \cup & \{e'_j \mid \exists D \ldotp u_j = \mathtt{min}_D \land k \in D\}). \end{array}
TODO: Example
Lemma 4.5 For all updates u \in \mathbf{Up}, \mathsf{upd}^{↺}(u, \cdot) and \mathsf{upd}(u, \cdot) form a Galois connection on the domain \operatorname{\mathrm{dom}}(u).
Proof. As \mathsf{upd}(u, \cdot) is monotonic, all that needs to be shown according to Lemma 4.3, is that \mathsf{upd}^{↺}(u, e') = \min \{e \mid e' \leq \mathsf{upd}(u, e)\}.
- Soundness: \mathsf{upd}^{↺}(u, e') \in \{e \mid e' \leq \mathsf{upd}(u, e)\}. This boils down to showing e'_k \leq (\mathsf{upd}(u, \mathsf{upd}^{↺}(u, e')))_k. Consider the cases of u_k.
- Case u_k \in \{0,-1\}. Then, we have to show e'_k \leq \mathsf{upd}^{↺}(u, e') + u_k. Due to \mathsf{upd}^{↺} being increasing, this must be the case as e'_k \leq e'_k + u_k.
- Case there is D such that u_k = \mathtt{min}_D and k \in D. Then, by definition of \mathtt{min}-updates, we have to show e'_k \leq \min\{(\mathsf{upd}^{↺}(u, e'))_j \mid j \in D\}, that is, e'_k \leq \mathsf{upd}^{↺}(u, e')_j for all j \in D. We do so by contradiction: Assume there were a j where this ordering does not hold, meaning e'_k > \mathsf{upd}^{↺}(u, e')_j. As k \in D, this is impossible due to the definition of \mathsf{upd}^{↺} in terms of \max.
- Minimality: For all e' \leq \mathsf{upd}(u, e), we show \mathsf{upd}^{↺}(u, e') \leq e. More specifically, (\mathsf{upd}^{↺}(u, e'))_k \leq e_k. Let us define d' := \max \{e'_j \mid \exists D \ldotp u_j = \mathtt{min}_D \land k \in D\}. Consider the cases of u_k \in \mathbf{Up}.
- Case u_k \in \{0,-1\} and e'_k - u_k \geq d'. Then e'_k \leq (\mathsf{upd}(u, e))_k = e_k + u_k, implying e'_k - u_k \leq (\mathsf{upd}(u, e))_k = e_k. By definition, (\mathsf{upd}^{↺}(u, e'))_k = \max(e'_k - u_k, d'). As e'_k - u_k \geq d', we can connect to the previous inequality, getting (\mathsf{upd}^{↺}(u, e'))_k = e'_k - u_k \leq e_k.
- Otherwise, (\mathsf{upd}^{↺}(u, e'))_k = d'. We show d' \leq e_k by contradiction. Assume it were the case that d' > e_k. For this to be true there would need to be j and D such that u_j = \mathtt{min}_D, k \in D, and e'_j \geq d' > e_k. By definition of \mathtt{min}-update at j, we calculate (\mathsf{upd}(u, e))_j \leq e_k < e'_j. But this would contradict the global assumption that e' \leq \mathsf{upd}(u, e).
Lemma 4.6 Algorithm 4.1 solves the energy game problem on an N-dimensional declining energy game \mathcal{G}^🗲=(G,G_{\mathrm{d}},\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}, w) in time \mathit{O}(o_{\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}} \cdot \left|G\right|^{2 \cdot N} \cdot (N^2 + \left|G\right|^{N-1} \cdot N)) and space \mathit{O}( \left|G\right|^{N} \cdot N ).
Proof. For declining updates, we instantiate the second case of Theorem 4.3: \mathit{O}( \left|G\right|^2 \cdot o_{\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}} \cdot (\operatorname{wdh}_{\mathcal{E}}(e_{\mathcal{G}}))^2 \cdot (t_{\mathcal{upd}^{↺}} + t_{\sup} + \operatorname{wdh}_{\mathcal{E}}(e_{\mathcal{G}}) \cdot t_\leq) ). For declining energy games as defined in Definition 4.5, we can fill in several blanks:
- t_{\sup}, the time to calculate the supremum between two elements of \mathbf{En} is in \mathit{O}(N),
- t_\leq, time to compare two elements of \mathbf{En} is in \mathit{O}(N),
- t_{\mathcal{upd}^{↺}}, time to compute \mathsf{upd}^{↺} on an energy is in \mathit{O}(N^2),
- e_{\mathcal{G}}, the highest energy that can be achieved by applying permutations of \mathsf{upd}^{↺} to \mathbf{0} for \left|G\right|-1 times, is the N-ary vector (\left|G\right|-1, …, \left|G\right|-1),
- \operatorname{wdh}_{\mathbf{En}}(e_{\mathcal{G}}), the widest anti-chain under e_{\mathcal{G}}, can be bounded \mathit{O}(\left|G\right|^{N-1}).
This yields: \begin{array}{rl} & \mathit{O}( \left|G\right|^2 \cdot o_{\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}} \cdot (\operatorname{wdh}_{\mathbf{En}}(e_{\mathcal{G}}))^2 \cdot (t_{\mathcal{upd}^{↺}} + t_{\sup} + \operatorname{wdh}_{\mathbf{En}}(e_{\mathcal{G}}) \cdot t_\leq) ) \\ = & \mathit{O}( \left|G\right|^2 \cdot o_{\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}} \cdot (\left|G\right|^{N-1})^2 \cdot (N^2 + N + \left|G\right|^{N-1} \cdot N) ) \\ = & \mathit{O}( o_{\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}} \cdot \left|G\right|^{2N+2-2} \cdot (N^2 + \left|G\right|^{N-1} \cdot N) ) \\ = & \mathit{O}( o_{\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}} \cdot \left|G\right|^{2N} \cdot (N^2 + \left|G\right|^{N-1} \cdot N) ) \\ \end{array} For space complexity, we obtain: \begin{array}{rl} & \mathit{O}( \left|G\right| \cdot \operatorname{wdh}_{\mathbf{En}}(e_{\mathcal{G}}) \cdot N ) \\ & \mathit{O}( \left|G\right| \cdot \left|G\right|^{N-1} \cdot N ) \\ & \mathit{O}( \left|G\right|^{N} \cdot N ) \end{array}
Definition 4.13 For N-dimensional energy games, we define the flattened energies as \widehat{\mathbf{En}}:= (\{0,1,\infty\})^N. A standard energy e \in \mathbf{En} is cast to \widehat{\mathbf{En}} by \widehat{e} where (\widehat{e})_k := \begin{cases} e_k & \text{if } e_k \leq 1 \\ \infty & \text{otherwise} \end{cases}. We denote as flattened monotonic energy game winner problem the variant of Definition 4.9 that outputs \widehat{\mathsf{Win}^{\mathrm{min}}_\mathrm{a}}(g) := \operatorname{\mathrm{Min}}(\mathsf{Win}_\mathrm{a}(g) \cap \widehat{\mathbf{En}}).
Clearly, Algorithm 4.1 can too be used to solve the flattened version of the problem by adapting \mathsf{upd}^{↺} to represent all components above 1 by \infty. Effectively, this decouples the size of Pareto fronts from the game size. In this instance, Lemma 4.6 becomes:
Lemma 4.7 Algorithm 4.1 solves the flattened energy game problem on an N-dimensional declining energy game \mathcal{G}^🗲=(G,G_{\mathrm{d}},\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}, w) in time \mathit{O}( o_{\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}} \cdot \left|G\right|^{2N} \cdot (N^2 + 3^{N-1} \cdot N) ) and in space \mathit{O}( \left|G\right| \cdot 3^{N-1} \cdot N ).
The bounds we have established are exponential with regard to the dimensionality N. But in our use case, we care for energy games of fixed dimensionality. The time bounds are polynomial with regard to game graph size. The space bounds behave similarly, but in the flattened variant fixed energy makes the space usage even drop to be linear in terms of game graph size.
4.3.5 Polynomial Spectroscopy Complexity
We have gathered enough material to have this section prove that the spectroscopy problem for the polynomial-time strong spectrum is indeed solvable in polynomial time, thus justifying the name we chose for the spectrum.
Theorem 4.4 Given a transition system \mathcal{S}, the spectroscopy problem for the \mathbf{N}^\mathsf{poly-strong}-spectrum can be solved in polynomial time with respect to the size of \mathcal{S}.
Proof. Theorem 4.1 has established that we can solve the spectroscopy problem for the \mathbf{N}^\mathsf{poly-strong}-spectrum by deciding the winning budgets of the bisimulation energy game {\mathcal{G}}_\mathrm{B}^🗲 on \mathcal{S}=(\mathcal{P},\mathit{Act},\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}). Thus, all that remains to be done is to instantiate the winning budget complexity of Lemma 4.6 for the case N=3 with the size of {\mathcal{G}}_\mathrm{B}^🗲 according to Definition 4.7.
The amount of attacker positions is bounded by \left|\mathcal{P}\right|^2. These positions can initiate up to \left|\mathcal{P}\right| \cdot \left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right| simulation challenges, leading to a similarly-bounded amount of defender positions, which again can be left by \left|\mathcal{P}\right| \cdot \left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right| moves.
In total, this amounts to o_{\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}_\mathrm{B}^🗲} in \mathit{O}(\left|\mathcal{P}\right| \cdot \left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right|) and to \left|G_\mathrm{B}^🗲\right| in \mathit{O}(\left|\mathcal{P}\right|^2).
Inserting the parameters in the time bounds of Lemma 4.6 yields: \begin{array}{rlccccccc} & O( & o_{\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}}} & \cdot & \left|G\right|^{2N} & \cdot & (N^2 + \left|G\right|^{N-1} \cdot N) & ) \\ = & O( & (\left|\mathcal{P}\right| \cdot \left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right|) & \cdot & (\left|\mathcal{P}\right|^2)^{2 \cdot 3} & \cdot & (3^2 + (\left|\mathcal{P}\right|^2)^{3-1} \cdot 3) & ) \\ = & O( & (\left|\mathcal{P}\right| \cdot \left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right|) & \cdot & \left|\mathcal{P}\right|^{12} & \cdot & \left|\mathcal{P}\right|^4 & )\\ = & O( & \left|\mathcal{P}\right|^{17} \cdot \left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right| & ). \end{array} For space complexity, the approach arrives at \mathit{O}( (\left|\mathcal{P}\right| \cdot \left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right|)^3). The bound drops to \mathit{O}( (\left|\mathcal{P}\right| \cdot \left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right|)) in the flattened variant of Lemma 4.7.
4.4 Discussion
This chapter has shown how to solve the spectroscopy problem for the \mathbf{N}^{\mathsf{poly-strong}} spectrum in polynomial time, thereby deciding all its preorders and equivalences at once.
The core ingredient has been to characterize the spectrum’s observation languages through an energy game (Note 4.1, Theorem 4.1) derived from the bisimulation game. The Pareto front view is slightly more general than other characteristic games, which Hüttel & Shukla (1996) for instance use to establish polynomial upper bounds individually for simulation-like notions.
To compute the Pareto fronts, we use a fixed point algorithm (Note 4.2, Algorithm 4.1). It can be thought of as a generalization of well-known ways to compute shortest distances in graphs:
Remark 4.4. The energy game problem of this chapter can be seen as a generalization of the shortest path problem on directed graphs to account for two players as well as for much more general distances and cost functions.
To see how, consider energy games on (\mathbb{Z}, \leq) where only deadlock positions belong to the defender and where all updates constitute one-dimensional integer addition. Then, e \in \mathsf{Win}^{\mathrm{min}}_\mathrm{a}(g) iff e is the length of a shortest path from g to some defender position (where negative (-z)-updates stand for what is usually written as a positive edge weight z for graphs). In this instance, Algorithm 4.1 behaves like the well-known Bellman–Ford algorithm for shortest paths.
Algorithm 4.1 contains relevant generalizations and practical improvements compared to the one originally used in Bisping (2023). Most importantly, the declining energy version loses a dimension of exponentiality. For the polynomial equivalences we arrive at a reasonably polynomial complexity for the spectroscopy instantiation, including reasonable space complexity for a flattened energy lattice.
Knowing that parts of the strong spectrum are \textsf{PSPACE}-hard, the algorithmic complexity indirectly proves that the bisimulation game cannot be used to characterize the whole spectrum. (Unless the polynomial hierarchy miraculously collapses to \textsf{PSPACE} = \textsf{P}.)
Thus, “we’re gonna need a bigger boat” game, at least exponentially-sized, to also cover \textsf{PSPACE}-hard notions.