3  Context: The Spectrum of Equivalences

We will now take a deeper dive into the question how groups of behavioral equivalences and preorders can be ranked in equivalence spectra.

For the following chapters, we will focus on the main “linear-time–branching-time spectrum” for the semantics of concrete processes treated by van Glabbeek (1990), the so-called “strong spectrum.” However, we will order the equivalences using the approach of parameterized notions of observability from the later “weak spectrum” by van Glabbeek (1993).

Section 3.1 provides the background on observability hierarchies, which motivate the chapter’s first core idea:

Idea 3.1: Notions of observability bring order

Groups of equivalences can be defined and ranked in lattices of notions of observability.

In particular, Section 3.2 will introduce such a spectrum, forming a hierarchy of modal logics for the strong spectrum. From there, we quickly run into our core question:

Idea 3.2: We have a spectroscopy problem

We can ask what notions of equivalence from a spectrum are the most fitting to relate two states.

Section 3.3 will define the spectroscopy problem formally and give lower bounds for its complexity on the strong spectrum.

3.1 Observability Hierarchies

Let us begin to pick up the idea from Section 2.3.3 that modal logics can nicely rank equivalences. The intuition is that \mathsf{HML} sublogics capture what we consider to be observable. The more we mark as observable, the finer the resulting equivalence relations become.

3.1.1 Understanding the Equivalence Hierarchy through Modal Logics

As promised, we revisit the hierarchy between bisimilarity, similarity, and trace equivalence of Section 2.2.3, modally. So far, we have only looked into the characterization of bisimilarity through the whole of \mathsf{HML} in Theorem 2.1 or through \mathcal{O}^{}_{\mathrm{\lfloor B \rfloor}} in Lemma 2.7. From now on, we will be working with hierarchies of Hennessy–Milner theorems.

Definition 3.1 (Logics of simulation and traces) We define the two \mathsf{HML} sublogics \mathcal{O}^{}_{\mathrm{T}}, the linear positive fragment+, and \mathcal{O}^{}_{\mathrm{S}}, the positive fragment*, by the grammars starting at φ^\mathrm{T} and φ^\mathrm{S}.

\begin{array}{rclll} φ^\mathrm{T} & \;::=\;& \langle α \rangle φ^\mathrm{T} & \;\mid\;& \top\\ φ^\mathrm{S} & \;::=\;& \langle α \rangle φ^\mathrm{S} & \;\mid\;& \textstyle\bigwedge_{i \in I}\langle α_i \rangle φ^\mathrm{S}_i \end{array}

The logics characterize trace and simulation preorder (and equivalence):

Lemma 3.1 (Trace characterizations) p \preceq_\mathrm{T} q precisely if p \preceq_{\mathcal{O}^{}_{\mathrm{T}}} q.1

Lemma 3.2 (Simulation characterization) p \preceq_\mathrm{S} q precisely if p \preceq_{\mathcal{O}^{}_{\mathrm{S}}} q.2

Clearly, \mathcal{O}^{}_{\mathrm{T}} \subset \mathcal{O}^{}_{\mathrm{S}} \subset \mathsf{HML}. So, Proposition 2.6 that sublogics will equate at least as much as their parent logic, yields another way of establishing the entailment hierarchy between bisimilarity, similarity, and trace equivalence of Section 2.2.3.3

3 Taking the two preceding lemmas together with Theorem 2.1 for \sim_\mathrm{B} and \mathsf{HML}.

In the modal realm, equivalences become naturally comparable. Contrast this with preceding definitions that live in different worlds: relational definition for (bi-)similarity of Definition 2.7 and denotational definition for trace equivalence of Definition 2.5. Heterogenous definitions lead to complicated proofs.

The modal view also reveals an intuitive hierarchy of “testing scenarios” for the equivalences, framed as black box tests in van Glabbeek (1990):

Trace equivalence
matches an observer that can see sequences of events. They just watch repeated executions of the program, but are oblivious to possibilities and decisions.
Similarity
matters to an experimenter that can also explore different branches of possibilities. This is valid if the experimenter can somehow copy the system state during the execution.
Bisimilarity
captures that the experimenter can moreover determine if a future course of events is impossible at some point. This means that the experimenter can not only copy the execution state but also exhaustively test every possibility of how the system may continue.

But such levels of observability do not need to be linear, as we will see in the next subsection …

3.1.2 Incomparabilities

Often, things we compare are comparable with respect to different dimensions. For instance, one can compare smartphone sizes with respect to width and height, as seen in Figure 3.1. This phenomenon of orthogonal dimensions also occurs for behavioral equivalences.

A well-known and natural notion of equivalence is that of failure equivalence. Intuitively, a failure says that the experimenter may follow a trace and see which actions are impossible at its end. Its standard definition is based on failure denotations:

Definition 3.2 (Failures) The set of failures of a process \mathsf{Failures}(p) \subseteq \mathit{Act}^* \times 2^{\mathit{Act}} is recursively defined as

  • (\texttt{()}, X) ∈ \mathsf{Failures}(p) if X \cap \operatorname{Ini}(p) = \varnothing,
  • (α \vec{w}, X) ∈ \mathsf{Failures}(p) if there is p' with p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{α}$}}} p' and (\vec w, X) ∈ \mathsf{Failures}(p').

For instance, the failure (\tau, \{\mathsf{a}\}) is in \mathsf{Failures}(\mathsf{P}) but not in \mathsf{Failures}(\mathsf{Q}) on Figure 2.3.

But would it not be nice if we could prevent the invention of new mathematical objects as denotations for each new notions of observability we consider? Fortunately, we can save the work, by directly employing modal logics:

Definition 3.3 (Failure logic) We define failure observations \mathcal{O}^{}_{\mathrm{F}} by the grammar: φ^\mathrm{F} \;::=\; \langle α \rangle φ^\mathrm{F} \quad\;\mid\;\quad \textstyle\bigwedge_{i \in I} \neg\langle α_i \rangle\top

Clearly, this encompasses what we may observe via traces, but is something that we cannot observe using simulation observations. We consider \preceq_\mathrm{F} given by \preceq_{\mathcal{O}^{}_{\mathrm{F}}}.

The distinguishing failure (\tau, \{\mathsf{a}\}) can be expressed as \langle τ \rangle\textstyle\bigwedge \{\neg\langle \mathsf{a} \rangle\top\} \in \mathcal{O}^{}_{\mathrm{F}} in HML. The formula distinguishes \mathsf{P} from \mathsf{Q} on Figure 2.3, \mathsf{P} \not\preceq_\mathrm{F} \mathsf{Q}. This sets failures apart from simulation, as \mathsf{P} \preceq_\mathrm{S} \mathsf{Q} (cf. Example 2.6). On the other hand, no failure from \mathcal{O}^{}_{\mathrm{F}}, distinguishes \mathsf{Q} from \mathsf{P}, implying \mathsf{Q} \preceq_\mathrm{F} \mathsf{P}, but \mathsf{Q} \not\preceq_\mathrm{S} \mathsf{P}.

Figure 3.2: Equivalence hierarchy including failure equivalence.

As a consequence, simulation preorder and failure preorder are incomparable, that is, neither one implies the other. The same is true of the corresponding equivalences: similarity and failure equivalence. The situation is summed up by the non-linear hierarchy in Figure 3.2. After a quick glance at the diamond-like figure, it probably comes as no surprise what kind of mathematical structure we employ to handle the hierarchy: lattices.

3.1.3 Lattices

To handle non-linearity, we will work with lattices of notions of behavioral equivalence. The following definition gives the preliminaries to talk about this kind of partial orders.

Definition 3.4 (Lattices, bounds, chains) A lattice is a partially ordered set (B, \leq), where there are greatest lower bounds \inf\{b_1, b_2\} and least upper bounds \sup\{b_1, b_2\} between each pair of elements b_1, b_2 \in B.

  • The greatest lower bound of a set B' \subseteq B is called its infimum, \inf B'. It refers to the greatest element b \in B such that b \leq b' for all b' \in B'.4
  • Dually, the least upper bound of a set B' \subseteq B is called its supremum, \sup B'. It refers to the least element b \in B such that b \geq b' for all b' \in B'.
  • For the pair-wise infimum we also use infix notation b_1 \sqcap b_2 = \inf \{b_1, b_2\}, and analogously b_1 \sqcup b_2 = \sup \{b_1, b_2\}.
  • If a lattice (B, \leq) not only allows infima and suprema for pairs but for any set B' \subseteq B, it is called complete. We say \inf-complete or \sup-complete if only one of the two is true.
  • We call a totally ordered subset B' \subseteq B a chain.
  • Dually, some B' \subseteq B with no two elements b_1, b_2 \in B' such that b_1 \leq b_2 is called an anti-chain.
  • The upward closure {{}\uparrow\! B'} of a B' \subseteq B is defined as \{b \in B \mid \exists b' \in B' \ldotp b' \leq b\}. Analogously, the downward closure is given by {{}\downarrow\! B'} \mathrel{≔}\{b \in B \mid \exists b' \in B' \ldotp b \leq b'\}.

4  Note that not necessarily b \in B'! Moreover, some sets do not have lower/upper bounds.

Figure 3.3: Lattice of subsets from Example 3.1. Solid lines stand for inclusion from bottom to top, transitive lines are left out.

Example 3.1 (Subset lattice) Given any set B, its subsets ordered by set inclusion (2^{B}, {\subseteq}) form a complete lattice.

The greatest lower bound is given by set intersection \bigcap B' with B' \subseteq B. The least upper bound is set union \bigcup B' with B' \subseteq B. The empty set \varnothing \in 2^{B} is the least element, B \in 2^{B} is itself the greatest element.

Consider the subset lattice over B = \{1,2,3\}. It is “cube-like,” as can be seen in its Hasse diagram in Figure 3.3. An example of a (maximal) chain would be \{\varnothing, \{1\}, \{1,2\}, B\} (the nodes connected by a blue dotted line in the figure), because its members are ordered linearly \varnothing \subset \{1\} \subset \{1,2\} \subset B. The set \{\{1\}, \{2\}, \{3\}\} forms a (maximal) anti-chain (the nodes connected by a red dashed line in the figure), because its members do not include each other. Their respective subsets are chains / anti-chains as well.

Figure 3.4: Visualization of the infinitary grid of \mathbb{N}^2 (and in gray, \mathbb{N}_\infty^2) in Example 3.2.

Example 3.2 (Vector lattice) Given a linearly ordered set (B, \leq_B), its d-ary Cartesian product with pointwise order (B^d, \leq) forms a lattice, where b \leq b' iff b_k \leq b'_k for all k \in \{1, …, d\}. Greatest lower bounds and least upper bounds can be transferred pointwise from B.

For instance, pairs of natural numbers, (\mathbb{N}^2, \leq), form a lattice, as visualized in Figure 3.4. It is \inf-complete, that is, for any set from \mathbb{N}^2, one can pick a greatest lower bound. However, the lattice is not \sup-complete: For instance, the set \mathbb{N}\times \{0\} has no upper bound. If we take the natural numbers extended with an upper bound \infty, \mathbb{N}_\infty, as basis, then (\mathbb{N}_\infty^2, \leq) forms a complete lattice.

When working with vectors, we assume standard notation, in particular, for d-dimensional vector addition b + c ≔ (b_1 + c_1, …, b_d + c_d). By \hat{\mathbf{e}}_{k}, we denote the unit vector where the k-th component is 1 and all other components equal 0. For example, \hat{\mathbf{e}}_{2} in a 3-dimensional context equals (0,1,0). The zero vector (0,…,0) is denoted by \mathbf{0}.

3.2 The Linear-Time–Branching-Time Spectrum

Van Glabbeek’s two papers on the “linear-time–branching-time spectrum” (1990, 1993) show how all common equivalences can be understood to form a lattice of sublanguages of \mathsf{HML} (and a variant of \mathsf{HML} for equivalences with silent steps). His hierarchy of equivalences derives from a hierarchy of notions of observability.5 We will introduce a similar construction: at first, in a generic form, then for the strong spectrum of van Glabbeek (1990).

5  In particular, the weak spectrum (van Glabbeek, 1993) makes this concept of notions really formal. Also, we usually implicitly refer to the full version of the strong spectrum (van Glabbeek, 2001).

3.2.1 Spectra as Observability Lattices

We will discuss various equivalence spectra. Van Glabbeek (1990, 1993) already gives two different ones. Let us first introduce an abstract description of such spectra.

Definition 3.5 (Equivalence spectrum) An equivalence spectrum (\mathbf{N}, \leq,\allowbreak \mathcal{O}^{}_{N \in \mathbf{N}}) consists of

  • a lattice of notions of observability, \mathbf{N}, partially ordered by {\leq} \subseteq \mathbf{N}\times \mathbf{N}, and
  • corresponding logics \mathcal{O}^{}_{N} \colon 2^{\mathsf{HML}} for N \in \mathbf{N}.

\mathcal{O}^{}_{N \in \mathbf{N}} must be monotonic, that is: for any two notions N,M \in \mathbf{N}, it holds that N \leq M \text{ implies } \mathcal{O}^{}_{N} \subseteq \mathcal{O}^{}_{M}.

Let us use our new definition to construct a subset lattice as in Example 3.1 to recreate the hierarchy of Figure 3.2.

Example 3.3 (Diamond spectrum) Consider the notions \mathbf{N}^\mathsf{simple} ≔ 2^{\{\mathsf{⊕}, \mathsf{⊗} \}}, ordered by subset inclusion, and the family of observation languages \mathcal{O}^{\mathsf{simple}}_{N \in \mathbf{N}} given by the family of grammars with some conditional productions: \begin{array}{rcll} φ^N & \;::=\;& \top{} & \\ & \;\mid\;& \langle α \rangle φ^N & \\ & \;\mid\;& \textstyle\bigwedge_{i \in I}φ^N_i & \text{ if $\mathsf{⊕} \in N$} \\ & \;\mid\;& \textstyle\bigwedge_{i \in I} \neg\langle α_i \rangle\top& \text{ if $\mathsf{⊗} \in N$} \\ & \;\mid\;& \neg φ^N & \text{ if $\{\mathsf{⊕}, \mathsf{⊗} \} = N$.} \end{array} Clearly, N \subseteq M implies \mathcal{O}^{}_{N} \subseteq \mathcal{O}^{}_{M} for N, M \in \mathbf{N}^\mathsf{simple}. We obtain the diamond hierarchy of Figure 3.5. It matches the diamond of Figure 3.2, but this time, the hierarchy is an effect of the ordered notions.

Figure 3.5: Hierarchy of simple notions of equivalence. (From now on, there are no arrows of implication: The lines stand for \leq or \subseteq relationships in the lattice!)

While the incomparable languages of Section 3.1 form no lattice, e.g. \mathcal{O}^{}_{\mathrm{S}} \cup \mathcal{O}^{}_{\mathrm{F}} \neq \mathsf{HML}, the notions of the present Example 3.3 do form a lattice, as \{\mathsf{⊕}\} \cup \{\mathsf{⊗}\} = \{\mathsf{⊕}, \mathsf{⊗}\}. This is one of the reasons why it is convenient to add notions of observability as an abstraction layer.

We can also ask what the least notion is to include a specific formula:

Definition 3.6 (Syntactic expressiveness price) In the context of a spectrum (\mathbf{N}, \leq, \mathcal{O}^{}_{N \in \mathbf{N}}), the syntactic expressiveness price of a formula \varphi that appears in one of the logics (i.e. \varphi \in \bigcup_{N \in \mathbf{N}} \mathcal{O}^{}_{N}) is defined as \mathsf{expr}^{}(\varphi) ≔ \min \{N \in \mathbf{N}\mid \varphi \in \mathcal{O}^{}_{N}\}.

Note that, given our definition of spectra, the minimum of Definition 3.6 does not need to exists—but it does for the spectra we will be working with.

Thinking of the lattice of notions as a hierarchy of how difficult it is to tell processes apart, we consider this as a kind of “price tag” to put on formulas depending on their syntactic complexity. Higher syntactic complexity allows formula sets of higher expressiveness.

In this view, a trace formula is cheaper than a failure formula. Using Example 3.3: The prices differ \mathsf{expr}^{}(\langle \tau \rangle\langle \mathsf{a} \rangle) = \varnothing \subset \{⊗\} = \mathsf{expr}^{}(\langle \tau \rangle \textstyle\bigwedge \{\neg\langle \mathsf{a} \rangle\}), which captures that we need a strictly smaller part of the grammar to construct the trace formula.

The concept of notions of equivalence will allow us to conveniently handle big equivalence hierarchies.

3.2.2 Strong Notions of Observability

Now we can approach the strong spectrum by van Glabbeek (1990).6 We will encode its notions as a \mathbb{N}_\infty-vector lattice as in Example 3.2. To cover all common behavioral preorders, we use six dimensions, counting certain syntactic features of \mathsf{HML} formulas:

6  “Strong” means that we treat \tau like any other action. This traditional naming alludes to the fact that weak notions, which wash away certain differences of internal \tau-behavior, are implied by their strong counterparts.

  1. Modal depth of observations (\langle \alpha \rangle\dots).
  2. Nesting depth of conjunctions (\textstyle\bigwedge \{\dots\}).
  3. Maximal modal depth of deepest positive conjuncts in conjunctions.
  4. Maximal modal depth of the other positive conjuncts in conjunctions.
  5. Maximal modal depth of negative conjuncts in conjunctions.
  6. Nesting depth of negations (\neg\dots).

Definition 3.7 (Strong spectrum) We define the strong notions of observability using vectors of extended naturals \mathbf{N}^\mathsf{strong} ≔ \mathbb{N}_\infty^6, ordered by pointwise comparison of vector components. The family of strong observation languages \mathcal{O}^{\mathsf{strong}}_{N \in \mathbf{N}^\mathsf{strong}} is given by the parameterized grammar starting from φ^N:7 \begin{array}{rcll} φ^N & \;::=\;& \top{} & \\ & \;\mid\;& \langle α \rangle φ^{N - \textcolor{obsColor}{\hat{\mathbf{e}}_{1}}} & \\ & \;\mid\;& \textstyle\bigwedge \{\varphi^{(N-\textcolor{conjColor}{\hat{\mathbf{e}}_{2}}) \sqcap (N_3, \infty, \infty, \infty, \infty, \infty)}, \\ & & \quad\; ψ^{(N-\textcolor{conjColor}{\hat{\mathbf{e}}_{2}}) \sqcap (\infty, \infty, \infty, \textcolor{mainPosColor}{N_3}, \infty, \infty)}, ψ^{(N-\textcolor{conjColor}{\hat{\mathbf{e}}_{2}}) \sqcap (\infty, \infty, \infty, \textcolor{mainPosColor}{N_3}, \infty, \infty)}, \ldots\} & \\ ψ^N & \;::=\;& φ^{(N \sqcap (\textcolor{otherPosColor}{N_4}, \infty, \infty, \infty, \infty, \infty))} & \\ & \;\mid\;& \neg φ^{(N \sqcap (\textcolor{negObsColor}{N_5}, \infty, \infty, \infty, \infty, \infty)) - \textcolor{negsColor}{\hat{\mathbf{e}}_{6}}} & \\ \end{array} The productions only exist if the respective recursive invocations are defined on the domain of notions. For instance, φ^N \leadsto \langle α \rangle φ^{N - \hat{\mathbf{e}}_{1}} is no valid production for N=(0,1,0,0,0,0) because (-1,1,0,0,0,0) \notin \mathbf{N}^\mathsf{strong}.

The number of \psi-conjuncts in \textstyle\bigwedge \{\dots\} is free–in particular, there might be none or infinitely many.

Example 3.4 (Formula language) The smallest notion to cover the failure formula of Section 3.1.2 would be (2,1,0,0,1,1), that is, \langle τ \rangle\textstyle\bigwedge \{\neg\langle \mathsf{a} \rangle\top\} \in \mathcal{O}^{\mathsf{strong}}_{(2,1,0,0,1,1)}. This is because the formula has two levels of modal observations, where the inner one is negated. The negation is wrapped in a conjunction with no positive conjuncts. A visualization for how \mathsf{expr}^{\mathsf{strong}}(\langle τ \rangle\textstyle\bigwedge \{\neg\langle \mathsf{a} \rangle\top\}) = (2,1,0,0,1,1) (according to Definition 3.6) comes together is given in Figure 3.6. Formally, the reason is that the following derivation is optimal: \begin{array}{rcl} \varphi^{(2,1,0,0,1,1)} & \leadsto & \langle τ \rangle\varphi^{(1,1,0,0,1,1)} \\ & \leadsto & \langle τ \rangle\textstyle\bigwedge \{\psi^{(1,0,0,0,1,1)}\} \\ & \leadsto & \langle τ \rangle\textstyle\bigwedge \{\neg\varphi^{(1,0,0,0,1,0)}\} \\ & \leadsto & \langle τ \rangle\textstyle\bigwedge \{\neg\langle \mathsf{a} \rangle\varphi^{(0,0,0,0,1,0)}\} \\ & \leadsto & \langle τ \rangle\textstyle\bigwedge \{\neg\langle \mathsf{a} \rangle\top\}. \end{array}

Figure 3.6: Pricing formula \langle τ \rangle\textstyle\bigwedge \{\neg\langle \mathsf{a} \rangle\top\} with syntactic expressiveness of (2,1,0,0,1,1).

If we reexamine the grammar of \mathcal{O}^{}_{\mathrm{F}} in Definition 3.3, we notice that the formulas it can produce almost match those of \mathcal{O}^{\mathsf{strong}}_{(\infty,1,0,0,1,1)} of the strong spectrum in Definition 3.7. The latter generates the \varphi_\mathrm{F}-grammar in Figure 3.9. As Lemma 3.3 will show, both languages are equally distinctive (Definition 2.15).

An example for the pricing of a more complex tree-like formula is given in Figure 3.7.

Figure 3.7: Pricing formula \langle \tau \rangle\textstyle\bigwedge \{\langle ec_A \rangle\langle lc_A \rangle\top, \langle \tau \rangle\top, \neg\langle ec_B \rangle\top\} with syntactic expressiveness (3,1,2,1,1,1).

Remark 3.1 (Explicit formula prices). In my papers (Bisping et al., 2022; Bisping, 2023; Bisping & Jansen, 2024), the syntactic expressiveness price of formulas \mathsf{expr}^{} is explicitly defined, instead of using a family of grammars. In this thesis, \mathsf{expr}^{} is indirectly defined through Definition 3.6.

The expressiveness price \mathsf{expr}^{\mathsf{strong}} of formulas in the strong spectrum (Definition 3.7) can be recursively characterized as described in Bisping (2023) (we will drop the “\mathsf{strong}” for readability):

\begin{array}{rl} \mathsf{expr}^{}(\top) \hspace{-3mm} &= \mathbf{0}\\ \mathsf{expr}^{}(\langle \alpha \rangle\varphi) \hspace{-3mm} &= \textcolor{obsColor}{\hat{\mathbf{e}}_{1}} + \mathsf{expr}^{}(\varphi) \\ \mathsf{expr}^{}(\neg\varphi) \hspace{-3mm} &= \textcolor{negsColor}{\hat{\mathbf{e}}_{6}} + \mathsf{expr}^{}(\varphi) \\ \textstyle\mathsf{expr}^{}(\bigwedge\limits_{i \in I}\psi_i) \hspace{-3mm} &= \textcolor{conjColor}{\hat{\mathbf{e}}_{2}} + \sup\Biggl(\big\{\! \begin{pmatrix} 0\\ 0\\ \textcolor{mainPosColor}{\sup_{i \in \mathit{Pos}}}\, (\mathsf{expr}^{}(\psi_i))_{\textcolor{obsColor}{1}}\\ \textcolor{otherPosColor}{\sup_{i \in \mathit{Pos} \mathbin{\backslash}\mathit{R}}}\, (\mathsf{expr}^{}(\psi_i))_{\textcolor{obsColor}{1}}\\ \textcolor{negObsColor}{\sup_{i \in \mathit{Neg}}}\, (\mathsf{expr}^{}(\psi_i))_{\textcolor{obsColor}{1}}\\ 0 \end{pmatrix} \!\big\} \cup \{ \mathsf{expr}^{}(\psi_i) \mid i \in I \} \Biggr) \\ & \begin{array}{rl} \mathit{Neg} \hspace{-2mm} & \mathrel{≔}\{i \in I \mid \exists \varphi'_i \ldotp \psi_i = \neg\varphi'_i \}\\ \mathit{Pos} \hspace{-2mm} & \mathrel{≔}I \mathbin{\backslash}\mathit{Neg}\\ \mathit{R} \hspace{-2mm} & \mathrel{≔} \begin{cases} \varnothing & \text{if } \mathit{Pos} = \varnothing\\ \{ r \} & \text{for some $r \in \mathit{Pos}$ with $(\mathsf{expr}^{}(\psi_r))_{\textcolor{obsColor}{1}}$ max.\ for $\mathit{Pos}$.}\! \end{cases} \end{array} \end{array}

Note that there is a minor divergence from Bisping (2023) in that the present thesis prices \mathsf{expr}^{}(\top) at \mathbf{0} instead of \hat{\mathbf{e}}_{2}. This change is done to align the pricing to the one we will need for the weak spectrum in later chapters.

Clearly, the explicit pricing of formulas is more versatile for the implementation direction we are aiming at. The grammar view, on the other hand, is particularly nice to see how our \mathsf{HML} sublanguages will align to games.

The strong spectrum of Definition 3.7 covers the notions of behavioral equivalence we have discussed so far. (What grammars due to the coordinates look like is listed in Figure 3.9 and Figure 3.10.)

Lemma 3.3 (Spectrum characterization) Traces, simulation, bisimulation and failures are covered as follows:

  1. The observation language \mathcal{O}^{\mathsf{strong}}_{(\infty, 0, 0, 0, 0, 0)} exactly matches the characterization of traces \mathcal{O}^{}_{\mathrm{T}} from Definition 3.1 and thus characterizes trace preorder.8
  2. The observation language \mathcal{O}^{\mathsf{strong}}_{(\infty, \infty, \infty, \infty, 0, 0)} exactly matches the characterization of simulation observations \mathcal{O}^{}_{\mathrm{S}} from Definition 3.1 and thus characterizes simulation.9
  3. The observation language \mathcal{O}^{\mathsf{strong}}_{(\infty, \infty, \infty, \infty, \infty, \infty)} matches \mathsf{HML} in distinctiveness and thus characterizes bisimilarity.
  4. The observation language \mathcal{O}^{\mathsf{strong}}_{(\infty, 1, 0, 0, 1, 1)} matches failure observations \mathcal{O}^{}_{\mathrm{F}} of Definition 3.3 in distinctiveness.

Proof.

  • Claim (1) for traces is trivial.
  • Claim (2) for simulation is trivial, given flattening of conjunctions.
  • For claim (3) of bisimilarity, observe that \mathcal{O}^{}_{\mathrm{\lfloor B \rfloor}} \subseteq \mathcal{O}^{\mathsf{strong}}_{(\infty, \infty, \infty, \infty, \infty, \infty)} by examining its grammar in Definition 2.16. As \mathcal{O}^{}_{\mathrm{\lfloor B \rfloor}} already has complete \mathsf{HML} distinctiveness by Lemma 2.7, so must its superlogic \mathcal{O}^{\mathsf{strong}}_{(\infty, \infty, \infty, \infty, \infty, \infty)}.
  • For claim (4) of failures, we must note that \mathcal{O}^{\mathsf{strong}}_{(\infty, 1, 0, 0, 1, 1)} also contains failure observations that end in conjunctions with a \neg\top-conjunct. But these are trivially false and thus cannot add to distinctiveness.

So far, we have only established that the six-dimensional spectrum covers the notions that the diamond of Example 3.3 has already covered–in a more complicated way. The extra dimensions will pay off in the next subsection.

3.2.3 The Strong Linear-Time–Branching-Time Spectrum

Using the six dimensions of Definition 3.7, we can assign coordinates to all other common notions of the strong linear-time–branching-time spectrum.

Definition 3.8 (Strong linear-time–branching-time spectrum) Coordinates with respect to the notions of Definition 3.7 for the common notions of behavioral equivalence and preorder in the strong linear-time–branching-time spectrum are given in Figure 3.8.10

10 When writing vectors in labels and figures, we omit the parentheses (\dots) for readability.

Figure 3.8: Hierarchy of common equivalences/preorders ordered by observability coordinates.

The coordinates of Definition 3.8 define a hierarchy of modal languages. Figure 3.9 and Figure 3.10 list the grammars that are described through the coordinates in interplay with Definition 3.7. The defining aspects of each grammar are marked in \textcolor{RoyalBlue}{\textrm{blue}}. The conjunction productions with “\dots” are to be read in the sense that they allow arbitrary many conjuncts; in particular, empty and infinitary conjunctions are possible. If a non-terminal appears only once in the conjunction production, at most one such subformula is allowed.

Figure 3.9: Grammars induced by coordinates for strong linear-time notions of equivalence.
Figure 3.10: Grammars induced by coordinates for strong branching-time notions of equivalence.

For the rest of the thesis, we will take the equivalences as defined by the coordinates as canonical. But, of course, it is natural to ask whether the equivalences thus defined correspond to previous definitions in this thesis and the literature. Lemma 3.3 already establishes that the coordinates of traces, simulation, failures, and bisimulation match the common definitions.

Mattes (2024) proves in Isabelle/HOL that our coordinate system spectrum matches the distinctiveness of the modal characterizations by van Glabbeek (2001).11 This entails a lot of fine print, which we will not reproduce here.

11  To be precise, Mattes (2024) works with the version of the spectrum from Bisping (2023). The only real difference is that, there, \top is priced at 1 conjunction, while the present spectrum prices it at \mathbf{0}, cf. Remark 3.1.

The grammars already contain a trick to handle equivalences of decorated traces, which we should discuss as it will be mirrored in game rules later on: The idea behind failure traces is that one observes a trace of actions and at each step a set of actions that are disabled. Ready traces work similarly, but with disabled and enabled actions in between.

Example 3.5 (Failure traces) Consider the following processes, which are slightly deeper variants of the situation we encountered with \mathsf{Q} and troll process \mathsf{T} in Example 2.7. \begin{aligned} \mathsf{Q'} \mathrel{≔}\, & \tau\ldotp\! (\mathsf{a}\ldotp\! \mathsf{a} +\mathsf{b}\ldotp\! \mathsf{b}) \\ \mathsf{T'_{\tau a a}} \mathrel{≔}\, & \mathsf{Q'} +\tau\ldotp\!\mathsf{a}\ldotp\! \mathsf{a} \\ \mathsf{T'_{\tau a}} \mathrel{≔}\, & \mathsf{Q'} +\tau\ldotp\!\mathsf{a} \end{aligned} \mathsf{T'_{\tau a a}} and \mathsf{T'_{\tau a}} are simulation equivalent. But they are distinguished by the failure-trace observation \langle \tau \rangle \textstyle\bigwedge \{\langle \mathsf{a} \rangle\langle \mathsf{a} \rangle, \neg\langle \mathsf{b} \rangle\}. The intuition is that we can observe the trace \tau \mathsf{a} \mathsf{a} together with the fact that \mathsf{b} is impossible after a first step of \mathsf{T'_{\tau a a}}, but not of \mathsf{T'_{\tau a}}.

The formula pricing works out, that is, \langle \tau \rangle \textstyle\bigwedge \{\langle \mathsf{a} \rangle\langle \mathsf{a} \rangle, \neg\langle \mathsf{b} \rangle\} \in \mathcal{O}^{\mathsf{strong}}_{(3,1,2,0,1,1)} \subseteq \mathcal{O}^{\mathsf{strong}}_{\mathrm{\mathsf{FT}}}. The important point here is that we can allow one arbitrarily deep positive conjunct but prevent any other, which would undermine the trace-likeness of the observation.

Example 3.5 shows how it pays off that the spectrum grammar (Definition 3.7) has a more lenient pricing for one of the positive conjuncts. We will refer to the deep positive conjunct of a conjunction as the revival, because revivals equivalence (Reed et al., 2007) is the minimal notion with this feature. It also matters for ready traces, as seen in the ready trace formula of Figure 3.7.

3.2.4 Any Questions?

There are a few standard questions that come to mind for people who are familiar with the various spectra of equivalence when seeing Figure 3.8. The following remarks address these points.

Remark 3.2 (Selection of notions). At the core, we treat the same notions as van Glabbeek (1990). But we feature a slightly more modern selection.

Our spectrum additionally includes strong versions of impossible futures (Voorhoeve & Mauw, 2001) and revivals (Reed et al., 2007; Roscoe, 2009) as equivalences whose relevance has only been noted after the publication of van Glabbeek (2001).

On the other hand, we glimpse over completed trace, completed simulation, and possible worlds observations like Kučera & Esparza (1999), who studied properties of “good” observation languages. These notions would need a different HML grammar, featuring exhaustive conjunctions \textstyle\bigwedge_{\alpha \in \mathit{Act}}\varphi_\alpha, where the \varphi_\alpha are deactivated actions for completed traces, and more complex trees for possible worlds.

Remark 3.3 (Synonymous coordinates). For many of the logics in Figure 3.8, there are multiple coordinates that characterize the same logic. For instance, due to the second dimension (conjunctions) being set to 0 for traces \mathrm{T}, the higher dimensions do not matter and any coordinate N = (\infty, 0, N_3, N_4, N_5, N_6) will lead to the same observation language \mathcal{O}^{\mathsf{strong}}_{N} = \mathcal{O}^{\mathsf{strong}}_{\mathrm{T}}.

Ruling out such equalities in the design of the lattice would be quite tedious. Luckily, Definition 3.5 only demands N \leq M to imply \mathcal{O}^{}_{N} \subseteq \mathcal{O}^{}_{M}, and not the converse.

Indeed, Figure 3.8 always selects the least coordinate to characterize a sublogic, in order for domination of coordinates in the figure and entailment between behavioral preorders to coincide.

At the same time, some notions could be characterized by strictly smaller coordinates due to sublogics of matching expressiveness. In particular, all (\infty, \infty, N_3, N_4, \infty, \infty) would characterize bisimilarity due to the unbounded possibility of “hiding” positive conjuncts in double negations. This observation will become relevant again later for varying abstractions of bisimilarity in the spectrum of weak equivalences in Section 6.3.2.

Remark 3.4 (Other coordinates). We have singled out a handful of coordinates. Many other coordinates will still correspond to distinct equivalences. For instance, we could consider N^{\mathrm{2T}} = (2,0,0,0,0,0), preordering states that cannot be distinguished by traces up to a length of 2. But it is difficult to make a case for such a “notion of equivalence,” which washes away differences of future behavior after exactly two steps.

Some kinds of depth-bounded families, however, are common in the literature to approximate bisimilarity and can also be placed in our spectrum:

  • k-step bisimilarity: (k,\infty,\infty,\infty,\infty,\infty) is a depth-k approximation of bisimilarity that sometimes appears in its fixed point characterizations, for instance in Aceto et al. (2007, Section 4.3).
  • k-stratified bisimilarity: (\infty,k,\infty,\infty,\infty,\infty) would be what Milner (1989, Section 10.4) calls “stratification of bisimilarity,” also appearing as “(k+1)-nested trace equivalence” in Aceto et al. (2004).
  • k-nested similarity: (\infty,\infty,\infty,\infty,\infty,k-1) for k>1 defines a spectrum of modal quantifier alternation depth between similarity and bisimilarity.

Remark 3.5 (Alternate dimensions). In principle, one can choose different dimensions to characterize the strong linear-time–branching-time spectrum. (Indeed, Bisping et al. (2022), Bisping (2023) and this thesis all use slightly different dimensions.)

Naturally, one may ask whether the same spectrum can be characterized with fewer than six dimensions. As some of the preceding examples also show, the dimensions we chose are not entirely orthogonal.

If we restrict our focus to a grid of ternary entries \{0,1,\infty\}, we can be sure to need at least five dimensions: With four dimensions, the height of the lattice is nine, that is, the maximal number of nodes on increasing paths between (0,0,0,0) and (\infty, \infty, \infty, \infty). But the hierarchy of Figure 3.8 has height ten!

With a grid of five ternary dimensions, we can recreate the hierarchy of Figure 3.8, and “hard-code” the logics for coordinates, a bit as it happens in Example 3.3. On the other hand, this would align less nicely with syntactic features of Hennessy–Milner logic.

Remark 3.6 ((In-)finitary variants). One can introduce more dimensions to the spectrum with respect to the possibility of infinitary observations. Our choice focuses on natural and most common versions of the equivalences, in particular: similarity and bisimilarity with unbounded (infinitary) branching and trace-like notions with finitary depth. Notions in Figure 3.8 correspond precisely to those without superscripts in the infinitary linear-time–branching-time spectrum of van Glabbeek (2001, Figure 9).

3.2.5 Non-Intersectionality

The strong spectrum of Definition 3.8 is much richer than the diamond spectrum from Example 3.3. Still, its observation languages form no lattice. For instance, the lines of simulation and failures join at ready simulation—and their coordinates as well (\infty,\infty,\infty,\infty,0,0) \sqcup(\infty,1,0,0,1,1) = (\infty,\infty,\infty,\infty,1,1). But \mathcal{O}^{\mathsf{strong}}_{\mathrm{S}} \cup \mathcal{O}^{\mathsf{strong}}_{\mathrm{F}} \neq \mathcal{O}^{\mathsf{strong}}_{\mathrm{RS}} and this makes a difference:

Example 3.6 (Simulation + failures \neq ready-simulation) Consider the \textsf{CCS} processes \mathsf{a}\ldotp\! (\mathsf{a}\ldotp\! \mathsf{b} +\mathsf{a}) and \mathsf{a}\ldotp\! \mathsf{a}\ldotp\! \mathsf{b} +\mathsf{a}\ldotp\!\mathsf{a}. They cannot be told apart by \mathcal{O}^{\mathsf{strong}}_{\mathrm{S}} or \mathcal{O}^{\mathsf{strong}}_{\mathrm{F}} and thus are simulation and failure equivalent (and moreover even ready-trace equivalent).

Still, the formula \langle \mathsf{a} \rangle\textstyle\bigwedge \{\langle \mathsf{a} \rangle\textstyle\bigwedge \{\neg\langle \mathsf{b} \rangle\}, \langle \mathsf{a} \rangle\langle \mathsf{b} \rangle\} \in \mathcal{O}^{\mathsf{strong}}_{\mathrm{RS}} distinguishes the first process from the second. Therefore, the processes are not ready-simulation equivalent.

What Example 3.6 shows is that one cannot prove two states to be ready-simulation-equivalent by showing that they are equated by simulation and failures: {\sim_\mathrm{S}} \cap {\sim_\mathrm{F}} \, \nsubseteq \, {\sim_\mathrm{RS}}. The relationship between the characterized equivalences is non-intersectional.

In general, multiple preorders may relate two states without this entailing a stronger equivalence. So the question “Which equivalence from a spectrum relates two states?” is too simple—one has to ask in plural: “Which equivalences relate two processes?”

This plural motivates the spectroscopy problem.

3.3 Spectroscopy

Now that we have a formal way of describing equivalence spectra, we can make formal the spectroscopy problem—the core topic of this thesis. We will also collect first thoughts on its complexity.

3.3.1 The Spectroscopy Problem

The problem has originally been introduced in Bisping et al. (2022) as the “abstract observation preorder problem” with respect to modal characterizations of the strong spectrum. We here reintroduce it in a more generic form.

Problem 3.1: Spectroscopy problem

In the context of a transition system \mathcal{S} and a spectrum (\mathbf{N}, \leq, \mathcal{O}^{}_{N \in \mathbf{N}}), the spectroscopy problem asks:

Input
States p and q.
Output
Maximal set of notions \mathbf{N}_{p,q} \subseteq \mathbf{N}, such that p \preceq_{\mathcal{O}^{}_{N}} q for each N \in \mathbf{N}_{p,q}.

Intuitively, the problem is about finding all the ways in which processes can be related, beyond the black-and-white of the bisimilarity problem. We aim to split up information on possible distinctions, analogously to a prism with light (Figure 3.11). Given that the equivalence hierarchies are commonly referred to as spectra, it is natural to borrow the name spectroscopy from physical experiments.

Example 3.7 (Warm-up spectroscopy) In Example 2.4, we have noticed that it is easy to distinguish \mathsf{q_{ab}} \not\preceq_\mathrm{T} \mathsf{p_a} through the 1-symbol-trace \mathsf{b}. In \mathsf{HML}, the difference is expressed as \langle \mathsf{b} \rangle\top.

The solution to the strong spectroscopy problem on \mathsf{q_{ab}} and \mathsf{p_a} is \mathbf{N}^{\mathsf{strong}}_{\mathsf{q_{ab}}, \mathsf{p_{a}}} = \{N \in \mathbf{N}^{\mathsf{strong}} \mid N_1 < 1\}. All notions thus characterized correspond to universal equivalence \mathrm{U} in distinctiveness. In other words, the states are not equivalent with respect to any notion where states are told apart at all. They are as different as possible, in our metric.

Example 3.8 (The spectrum of trolled philosophers) For the “trolled philosophers” of Example 2.7, we have determined that the systems are simulation-preordered, but not bisimilar, that is, \mathsf{Q} \preceq_\mathrm{S} \mathsf{T}, but \mathsf{Q} \not\preceq_\mathrm{B} \mathsf{T}. The first fact implies \mathsf{Q} \preceq_\mathrm{T} \mathsf{T}.

But what about other notions from the strong spectrum of Section 3.2.3? Besides similarity, there might well be incomparable or finer notions that also preorder \mathsf{Q} to \mathsf{T}!

The solution to the spectroscopy problem on \mathsf{Q} and \mathsf{T} is \mathbf{N}^{\mathsf{strong}}_{\mathsf{Q}, \mathsf{T}} = \{N \in \mathbf{N}^\mathsf{strong} \mid (2,2,0,0,2,2) \nleq N\}. A minimal formula to distinguish \mathsf{Q} from \mathsf{T} with coordinate (2,2,0,0,2,2) would be \textstyle\bigwedge \{\neg\langle \tau \rangle\textstyle\bigwedge \{\neg\langle \mathsf{a} \rangle\top\}\}. (The following chapters will reveal how to reliably arrive at this knowledge, in particular, the minimality.)

Figure 3.12 shows how the distinction is above the distinction spaces of most notions we named.

Because the coordinate of 2-nested simulation, \mathrm{2S} = (\infty,\infty,\infty,\infty,\infty,1) is not above (2,2,0,0,2,2), we arrive at \mathsf{Q} \preceq_\mathrm{2S} \mathsf{T}, which implies all preorders of Figure 3.8 except for bisimilarity.

Figure 3.12: Cross section of the strong spectrum showing the dimensions conjunctions, negative conjunct depth, and negation depth. All preorders that are not hit by the red mark at (2,2,2) hold in Example 3.8.

Note that we have expressed \mathbf{N}^{\mathsf{strong}}_{\mathsf{Q}, \mathsf{T}} through a negation (“(2,2,0,0,2,2) \nleq N”). The reason is that a positive description is usually unwieldy. In this (comparably easy) case, we could for example list the half-spaces undercutting the cheapest distinction, and this would read: \mathbf{N}^{\mathsf{strong}}_{\mathsf{Q}, \mathsf{T}} = (\{0,1\} \times \mathbb{N}_\infty^5) \cup (\mathbb{N}_\infty\times \{0,1\} \times \mathbb{N}_\infty^4) \cup (\mathbb{N}_\infty^4 \times \{0,1\} \times \mathbb{N}_\infty) \cup (\mathbb{N}_\infty^5 \times \{0,1\}).

Technically, it is convenient to not compute \mathbf{N}_{p,q} directly. Rather we aim to construct the Pareto front of minimal notions that do not hold, \operatorname{\mathrm{Min}}(\mathbf{N}\mathbin{\backslash}\mathbf{N}_{p,q}). The Pareto front serves as a unique representation, from which \mathbf{N}_{p,q} can be constructed as complement of the upward closure \mathbf{N}\mathbin{\backslash}{}\uparrow\operatorname{\mathrm{Min}}(\mathbf{N}\mathbin{\backslash}\mathbf{N}_{p,q}). Pareto fronts form anti-chains and appear naturally in optimization problems.

All spectra we are concerned with are well-quasi ordered, which means that each \operatorname{\mathrm{Min}}(\mathbf{N}\mathbin{\backslash}\mathbf{N}_{p,q}) must be finite in size (Kruskal, 1972) and thus “more handy” than the full sets \mathbf{N}_{p,q} or \mathbf{N}\mathbin{\backslash}\mathbf{N}_{p,q}.

So, effectively, we will be asking: What are the minimal notions to distinguish p from q—and then often talk about the converse: The most-fitting notions to preorder or equate the states. Everything else is implied.

Remark 3.7 (Infinitely many notions). The spectrum as formulated in Definition 3.7 contains infinitely many notions. This would be a problem in a naive solution to Problem 3.1 that relies on deciding equivalences individually, but will be no problem for us. Where we, however, assume finiteness for algorithms, is in the state-space size of \mathcal{S}.

3.3.2 Spectroscopy as Abstract Subtraction

Another way of viewing the spectroscopy problem is that we aim to compute an abstracted kind of difference between programs.

Definition 3.9 (Observations and difference) On a transition system \mathcal{S}, the possible observations of a state, \llbracket \cdot \rrbracket^👁 \colon \mathcal{P}\to 2^{\mathsf{HML}}, are defined as: \llbracket p \rrbracket^👁 ≔ \{φ ∈ \mathsf{HML}\mid p ∈ \llbracket φ \rrbracket\}. The difference between p and q is defined as: \Delta(p,q) ≔ \llbracket p \rrbracket^👁 \mathbin{\backslash}\llbracket q \rrbracket^👁.

\Delta(p,q) expresses the set of observations one could make of p that one cannot make of q. This set will be empty when the states are bisimilar, or infinite, otherwise.

With this notation, we could rephrase how preorders derive from \mathsf{HML} subsets in Definition 2.13:

Proposition 3.1 Two states p and q are preordered with respect to a sublogic \mathcal{O}^{}_{} ⊆ \mathsf{HML}: p \preceq_{\mathcal{O}^{}_{}} q ⟺ \Delta(p,q) \cap \mathcal{O}^{}_{} = \varnothing.

The spectroscopy problem then is about computing some abstraction \Delta_A such that N \in \Delta_A(p,q) precisely if \Delta(p,q) \cap \mathcal{O}^{}_{N} \neq \varnothing. \mathbf{N}_{p,q} plays the role of \Delta_A(p,q).

This falls in line with our observations about the \leq-game on numbers in Example 2.14 and (bi-)simulation games. Comparison is inherently linked to subtraction.

3.3.3 Complexities

What complexities to expect when deciding spectroscopy problems on finite systems? Details depend, of course, on the specific spectrum and flavor of Hennessy–Milner logic we are concerned with. Still, solving the spectroscopy problem cannot be easier than solving the covered individual equivalence problems.

To get a first idea, let us examine the complexities of common equivalence checking problems in the strong spectrum. The rule of thumb is that trace-like equivalences are \textsf{PSPACE}-complete and bisimilarities are \textsf{P}-complete (Balcázar et al., 1992; Hüttel & Shukla, 1996; Kanellakis & Smolka, 1983).

Bisimilarity finds itself in a valley of tractability, if we look at a cross section through the equivalence spectrum as in Figure 3.13. The best known bisimilarity algorithms for finite-state transition systems take \mathit{O}(\smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|} \log \smash{|{\mathcal{P}}|}) time. They usually employ partition refinement (e.g. Valmari, 2009), deriving from Paige & Tarjan (1987).

Figure 3.13: Bisimilarity’s complexity valley.

For coarser simulation-like equivalences, the best known algorithms need \mathit{O}(\smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|} \smash{|{\mathcal{P}}|}) time (Ranzato & Tapparo, 2010).12

12 Or \mathit{O}(\smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|} \smash{|{\smash{S_{/\sim_\mathrm{S}}}}|}) to name the bound as Ranzato & Tapparo (2010) present it.

The finer graph-isomorphism equivalence (Definition 2.8) again is harder with the best known solution (Babai, 2016) in quasi-polynomial time 2^{\mathit{O}((\log n)^3)}.

There are few strict hardness results at this level of granularity. So, better time complexities for graph isomorphism, bisimilarity, and similarity are conceivable (albeit improbable). Groote et al. (2023) show that at least partition-refinement algorithms for bisimilarity cannot do better than \mathit{O}(\smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|} \log \smash{|{\mathcal{P}}|}). In a recent preprint, Groote & Martens (2024) establish that similarity is strictly more complex than bisimilarity.

The trivial equivalences at the end of the cross section, identity \mathrm{ID} and universal equivalence \mathrm{U}, can be solved directly. Enabledness equivalence \mathrm{E} can as well be computed quite quickly by just comparing outgoing transitions.

In this thesis, we solve the spectroscopy problem for the strong and weak spectrum. So, we must be at least as complex as the equivalences between bisimilarity and universal equivalence, boxed in Figure 3.13. Consequently, the spectroscopy problem for the standard equivalence spectra is \textsf{PSPACE}-hard.

3.4 Discussion

In this chapter, we have formalized how to handle spectra of equivalence (Idea 3.1), and instantiated the approach to the strong spectrum of van Glabbeek (2001). From there, we have introduced the spectroscopy problem, which asks for notions to preorder compared states (Idea 1.1).

The shifted problem.   By formulating the problem in terms of a lattice over \mathbb{N}_\infty-vectors, the family of qualitative strong preorder/equivalence problems becomes a single quantitative problem: The spectroscopy problem for the strong spectrum. As we will see, the perspective of one quantitative problem is more insightful than the view of loosely-related, isolated equivalence problems.

We have already laid the groundwork to shift the semantic question of equivalence into a syntactic question of the shape of distinguishing formulas.

Prior publications.   The core ideas of this section have already been explored in Bisping et al. (2022) and Bisping (2023) for the strong spectrum. However, in my prior work the expressiveness prices played a more crucial role. Here, we instead opted for a parameterized grammar to define notions and their observations \mathcal{O}^{}_{N}. In this grammar, we count \top as part of the \mathbf{0}-notion. These are mostly superficial changes to streamline the following presentation. We have shown that traces, failures, simulation and bisimulation equivalence as defined by the notion coordinates match their textbook definitions. Mattes (2024) addresses all notions in Isabelle/HOL.

What's next?   So far, we have a problem and confidence that its solution conveys information about equivalences of the strong spectrum. Section 3.3.3 has established that spectroscopy complexity must be at least \textsf{PSPACE} on the strong spectrum.

However, there is a polynomial-time-easy fragment of the spectrum around bisimilarity and (ready) similarity. In Part II, comprising the next two chapters, we will first solve the spectroscopy problem for this \textsf{P}-easy slice and then extend to the whole strong spectrum. After that, we will also consider the weak spectrum in Part III.