3 Context: The Spectrum of Equivalences

We will now take a deeper dive into 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 Glabbeek (1990), the so-called “strong spectrum.” However, we will order the equivalences using the approach of parameterized notions of observability from the later Glabbeek (1993).

Glabbeek, R. J. van. (1990). The linear time–branching time spectrum: Extended abstract. In J. C. M. Baeten & J. W. Klop (Eds.), CONCUR’90 (Vol. 458, pp. 278–297). Springer. https://doi.org/10.1007/BFb0039066

The first core idea of this chapter is:

Note 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 will quickly run into the second core idea:

Note 3.2: We have a Spectroscopy problem

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

Section 3.3 will define the 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 Subsection 2.3.3 that modal logics can nicely rank equivalences. The intuition is that \textsf{HML} sublogics capture what we consider to be observable. The more we mark as observable, the finer the resulting equivalence relations do become.

3.1.1 Understanding the Equivalence Hierarchy through Modal Logics

As promised, we revisit the hierarchy between bisimilarity, similarity, and trace equivalence of Subsection 2.2.3, modally. So far, we have only looked into the characterization of bisimilarity through the whole of \textsf{HML} in Theorem 2.1 or through \mathcal{O}_\mathrm{\lfloor B \rfloor} in Example 2.11.

Definition 3.1 We define the two \textsf{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 p \preceq_\mathrm{T} q precisely if p \preceq_{\mathcal{O}_\mathrm{T}} q.¹

theorem HML_Spectrum.lts.observations_traces_characterizes_trace_preorder

Lemma 3.2 p \preceq_\mathrm{S} q precisely if p \preceq_{\mathcal{O}_\mathrm{S}} q.²

theorem HML_Spectrum.lts.observations_simulation_characterize_simulation_preorder

Clearly, \mathcal{O}_\mathrm{T} \subset \mathcal{O}_\mathrm{S} \subset \textsf{HML}. So, Proposition 2.4 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 Subsection 2.2.3.³

³ Taking the two previous lemmas together with Theorem 2.1 for \sim_\mathrm{B} and \textsf{HML}.

While the relational definitions for (bi-)similarity of Definition 2.7 and the denotational definition of trace equivalence Definition 2.5 live in different worlds, the two equivalences become naturally comparable in the modal realm.

The modal view also reveals an intuitive hierarchy of “testing scenarios” for the equivalences, framed as black box tests:

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

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) is recursively defined as

(\texttt{()}, X) ∈ \mathsf{Failures}(p) if X \cap \operatorname{Ini}(p) = \varnothing,
(α \cdot \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 every new notions of observability we consider? Fortunately, we can save the work, by directly employing modal logics:

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

The distinguishing failure (\tau, \{\mathsf{a}\}) can be 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, but \mathsf{P} \preceq_\mathrm{S} \mathsf{Q} (cf. Example 2.5). On the other hand, no failure from \mathcal{O}_\mathrm{F}, distinguishes \mathsf{Q} from \mathsf{P}, but \mathsf{Q} \not\preceq_\mathrm{S} \mathsf{P}.

  flowchart TD
    B["Bisimilarity"] --> S["Similarity"] --> T["Trace Equivalence"]
    B --> F["Failure Equivalence"] --> T

Figure 3.1: Preorder/equivalence hierarchy.

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.1. 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 be working 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'.⁴

⁴ Note that not necessarily b \in B'!

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 \sqcap-complete or \sqcup-complete if only one of the two is true.

We call 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.

Figure 3.2: Lattice of subsets from Example 3.1.

Example 3.1 (Subset Lattice) Given any set B, its subsets and 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. \varnothing \in 2^{B} is the least element, B \in 2^{B} is itself the greatest bound.

Consider the subset lattice over B = \{1,2,3\}. It is “cube-like,” as can be seen in its Hasse diagram in Figure 3.2. 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. \{\{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.3: 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 linearly-ordered set (B, \leq_B), its n-ary Cartesian product with pointwise order (B^n, \leq) forms a lattice, where b \leq b' iff b_k \leq b'_k for all k \in \{1, …, n\}. Greatest lower bounds and least upper bounds can be transferred pointwisely from B.

For instance, pairs of natural numbers, (\mathbb{N}^2, \leq), form a lattice, as visualized in Figure 3.3. It is \sqcap-complete, that is, for any set from \mathbb{N}^2, one can pick a greatest lower bound. However, the lattice is not \sqcup-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.

3.2 The Linear-Time–Branching-Time Spectrum

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

⁵ In particular, the weak spectrum (Glabbeek, 1993) makes this really formal.

Glabbeek, R. J. van. (1993). The linear time–branching time spectrum II: The semantics of sequential systems with silent moves; extended abstract. In E. Best (Ed.), CONCUR’93 (Vol. 715, pp. 66–81). Springer. https://doi.org/10.1007/3-540-57208-2_6

3.2.1 Spectra as Observability Lattices

As we will discuss various equivalence spectra (van Glabbeek (1993, 2001) 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, \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^{\textsf{HML}} for N \in \mathbf{N}.

\mathcal{O}_{N \in notions} 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.1.

Example 3.3 Consider the notions \mathbf{N}^\mathsf{simple} ≔ 2^{\{\mathsf{(\land)}, \mathsf{(\neg)} \}}, ordered by subset inclusion, and the family of observation languages \mathcal{O}_{N \in \mathbf{N}^\mathsf{simple}} 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{(\land)} \in N$} \\ & \;\mid\;& \textstyle\bigwedge_{i \in I} \neg\langle α_i \rangle\top& \text{ if $\mathsf{(\neg)} \in N$} \\ & \;\mid\;& \neg φ^N & \text{ if $\{\mathsf{(\land)}, \mathsf{(\neg)} \} = 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.4. It matches the diamond of Figure 3.1, but this time, the hierarchy is an effect of the ordered notions.

flowchart TD
  B["Bisimilarity <br> {(∧), (¬)}"] --- S["Similarity <br> {(∧)}"] --- T["Trace Equivalence <br> ∅"]
  B --- F["Failure Equivalence <br> {(¬)}"] --- T

Figure 3.4: Hierarchy of simple notions of equivalence.

While the incomparable languages of Subsection 3.1.2 form no lattice, e.g. \mathcal{O}_\mathrm{S} \cup \mathcal{O}_\mathrm{F} \neq \textsf{HML}, the notions of the present Example 3.3 do form a lattice, as \{\mathsf{(\land)}\} \cup \{\mathsf{(\neg)}\} = \{\mathsf{(\land)}, \mathsf{(\neg)}\}. 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 \sqcap-complete 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 is defined as \mathsf{expr}(\varphi) := \inf \{N \in \mathbf{N}\mid \varphi \in \mathcal{O}_{N}\}.

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: \mathsf{expr}(\langle \tau \rangle\langle \mathsf{a} \rangle) = \varnothing \subset \{(\neg)\} = \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.

3.2.2 The Strong Notions of Observability

Now we can approach the strong spectrum. 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 \textsf{HML}-formulas:

Formula modal depth of observations.
Formula nesting depth of conjunctions.
Maximal modal depth of deepest positive clauses in conjunctions.
Maximal modal depth of the other positive clauses in conjunctions.
Maximal modal depth of negative clauses in conjunctions.
Formula nesting depth of negations.

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, and the family of strong observation languages \mathcal{O}_{N \in \mathbf{N}^\mathsf{strong}}^\mathsf{strong} given by the parameterized grammar starting from φ^N:⁶

primrec Priced_HML.formula_of_price

\begin{array}{rcll} φ^N & \;::=\;& \top{} & \\ & \;\mid\;& \langle α \rangle φ^{N - \mathbf{\hat{e}}_{1}} & \\ & \;\mid\;& \textstyle\bigwedge \{ψ^{N-\mathbf{\hat{e}}_{2}}, ψ^{(N-\mathbf{\hat{e}}_{2}) \sqcap (\infty, \infty, N_4, \infty, \infty, \infty)}, ψ^{(N-\mathbf{\hat{e}}_{2}) \sqcap (\infty, \infty, N_4, \infty, \infty, \infty)}, \ldots\} & \\ ψ^N & \;::=\;& \langle α \rangle φ^{(N \sqcap (N_3, \infty, \infty, \infty, \infty, \infty)) - \mathbf{\hat{e}}_{1}} & \\ & \;\mid\;& \neg\langle α \rangle φ^{(N \sqcap (N_5, \infty, \infty, \infty, \infty, \infty))- \mathbf{\hat{e}}_{1} - \mathbf{\hat{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 - \mathbf{\hat{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}.

Example 3.4 The smallest notion to cover the failure formula of Subsection 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}_{(2,1,0,0,1,1)^\mathsf{strong}}. 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 clauses. 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 the upcoming Figure 3.5. 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\langle \mathsf{a} \rangle\varphi^{(0,0,0,0,1,0)}\} \\ & \leadsto & \langle τ \rangle\textstyle\bigwedge \{\neg\langle \mathsf{a} \rangle\top\}. \end{array} If we reexamine the grammar of \mathcal{O}_\mathrm{F} in Definition 3.3, we notice that the formulas it can produce match those of \mathcal{O}_{(\infty,1,0,0,1,1)}^\mathsf{strong} of the strong spectrum in Definition 3.7.

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

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

Figure 3.6: 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 e = (3,1,2,1,1,1).

Lemma 3.3 The strong spectrum of Definition 3.7 contains the notions of behavioral equivalence we have discussed so far.

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

theorem Priced_Spectrum.lts.traces_priced_characterization

theorem Priced_Spectrum.lts.simulation_priced_characterization

Proof. The only non-trivial case is (3) for bisimilarity:

Observe that \mathcal{O}_\mathrm{\lfloor B \rfloor} \subseteq \mathcal{O}_{(\infty, \infty, \infty, \infty, \infty, \infty)}^\mathsf{strong} by examining its grammar in Example 2.11. As \mathcal{O}_\mathrm{\lfloor B \rfloor} already has complete \textsf{HML}-distinctiveness by Lemma 2.8, so must its superlogic \mathcal{O}_{(\infty, \infty, \infty, \infty, \infty, \infty)}^\mathsf{strong}.

So far, we have only established that the six-dimensional spectrum also covers the notions that 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.7.⁹

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

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

For the rest of the thesis, we will take the equivalences as defined by the coordinates as canonical. Lemma 3.3 has established that the coordinates of traces, simulation, failures, and bisimulation match the definitions one commonly finds in the literature. To establish the same for the other notions, would mean a lot of (repetitive) definitions, which mostly reproduce van Glabbeek’s survey (2001). Mattes (2024) proves in Isabelle/HOL that the coordinate system of the conference version of this spectrum (Bisping, 2023) match distinctiveness of the modal characterizations in (Glabbeek, 2001).

Mattes, K. P. P. (2024). Measuring expressive power of HML formulas in Isabelle/HOL [Bachelor's Thesis, Technische Universität Berlin]. https://github.com/ekeln/BA_formula_prices/raw/main/output/outline.pdf

Warning

I might add such a marathon if there’s strong popular demand.

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

Remark 3.1 (Selection of Notions). At the core, we treat the same notions as Glabbeek (2001). But we feature a slightly more modern selection.

Voorhoeve, M., & Mauw, S. (2001). Impossible futures and determinism. Information Processing Letters, 80(1), 51–58. https://doi.org/10.1016/S0020-0190(01)00217-4

Roscoe, A. W. (2009). Revivals, stuckness and the hierarchy of CSP models. Journal of Logic and Algebraic Programming, 78(3), 163–190. https://doi.org/10.1016/j.jlap.2008.10.002

Our spectrum additionally includes strong versions of impossible futures (Voorhoeve & Mauw (2001)) and revivals (Roscoe (2009)) as equivalences whose relevance has only been noted after the publication of 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_{a \in \mathit{Act}}\varphi_a, where the \varphi_a are deactivated actions for completed traces, and more complex trees for possible worlds.

Kučera, A., & Esparza, J. (1999). A logical viewpoint on process-algebraic quotients. In J. Flum & M. Rodriguez-Artalejo (Eds.), Computer science logic: CSL (Vol. 1683, pp. 499–514). Springer. https://doi.org/10.1007/3-540-48168-0_35

Remark 3.2 (Ambiguous Coordinates). For many of the logics in Figure 3.7, 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}_{N}^\mathsf{strong} = \mathcal{O}_\mathrm{T}^\mathsf{strong}.

Indeed, Figure 3.7 always selects the least coordinate to characterize a sublogic, which ensures that domination of coordinates in the figure and entailment between behavioral preorders coincide.

Remark 3.3 (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.

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

k-step bisimilarity: (k,\infty,\infty,\infty,\infty,\infty) is a k-observation approximation of bisimilarity that sometimes appears in proofs.¹⁰
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.

¹⁰ TODO: look up example

Remark 3.4 ((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.7 correspond precisely to those without superscripts in the infinitary linear-time–branching-time spectrum of Glabbeek (2001, Figure 9).

3.2.4 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}_\mathrm{S}^\mathsf{strong} \cup \mathcal{O}_\mathrm{F}^\mathsf{strong} \neq \mathcal{O}_\mathrm{RS}^\mathsf{strong} and this makes a difference:

Example 3.5 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}_\mathrm{S}^\mathsf{strong} or \mathcal{O}_\mathrm{F}^\mathsf{strong} 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}_\mathrm{RS}^\mathsf{strong} distinguishes the first process from the second. Therefore, the processes are not ready-simulation equivalent.

What this shows is that one cannot prove two states to be ready-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 to simple, one has to ask: “Which equivalences relate two processes?”

This 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.

Definition 3.9 (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: 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}.

Example 3.6 For the “trolled philosophers” of Example 2.6, 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 Subsection 3.2.3? Besides similarity, there might well be incomparable or finer notions that too 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 N \nleq (2,2,0,0,2,2)\}. A minimal formula to distinguish \mathsf{Q} from \mathsf{T} with this coordinate 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.)

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

Figure 3.8: Cross section of the strong spectrum showing the dimensions conjunctions, negative clause depth, and negation depth. All preorders below the red mark at (2,2,2) hold in Example 3.6.

Note that we have expressed \mathbf{N}^{\mathsf{strong}}_{\mathsf{Q}, \mathsf{T}} through a negation (“\dots \nleq (2,2,0,0,2,2)”). The reason is that a positive description is usually unwieldy. In this (comparably easy) case, we could for example list the half-spaces below 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 upwards closure \mathbf{N}\mathbin{\backslash}{}\uparrow\operatorname{\mathrm{Min}}(\mathbf{N}\mathbin{\backslash}\mathbf{N}_{p,q}) (where {{}\uparrow\! B} := \{b \mid \exists b' \in B \ldotp b' \leq b\} is the upwards closure for B subset of some partially-ordered set). Clearly, 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}.

Kruskal, J. B. (1972). The theory of well-quasi-ordering: A frequently discovered concept. Journal of Combinatorial Theory, Series A, 13(3), 297–305. https://doi.org/10.1016/0097-3165(72)90063-5

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.

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.10 (Observations and Difference) On a transition system \mathcal{S}, the possible observations of a state, \llbracket \cdot \rrbracket^👁 \colon \mathcal{P}\to 2^{\textsf{HML}}, are defined as: \llbracket p \rrbracket^👁 ≔ \{φ ∈ \textsf{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 Definition 2.12:

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

A spectroscopy then is about computing some abstraction \Delta_\alpha such that N \in \Delta_\alpha(p,q) precisely if \Delta(p,q) \cap \mathcal{O}_{N} \neq \varnothing.

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).

Balcázar, J., Gabarro, J., & Santha, M. (1992). Deciding bisimilarity is p-complete. Formal Aspects of Computing, 4, 638–648. https://doi.org/10.1007/BF03180566

Hüttel, H., & Shukla, S. (1996). On the complexity of deciding behavioural equivalences and preorders. A survey (BRICS RS-96-39H). University of Aarhus. https://doi.org/10.7146/brics.v3i39.20021

Paige, R., & Tarjan, R. E. (1987). Three partition refinement algorithms. SIAM Journal on Computing, 16(6), 973–989.

Bisimilarity finds itself in a valley of tractability, if we look at a cross section through the equivalence spectrum as in Figure 3.9. The best known bisimilarity algorithms for finite-state transition systems take \mathit{O}(\left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right| \log \left|S\right|) time (usually deriving from Paige & Tarjan, 1987).

Figure 3.9: Bisimilarity’s complexity valley.

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

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

Ranzato, F., & Tapparo, F. (2010). An efficient simulation algorithm based on abstract interpretation. Information and Computation, 208(1), 1–22. https://doi.org/10.1016/j.ic.2009.06.002

Babai, L. (2016). Graph isomorphism in quasipolynomial time [extended abstract]. Proceedings of the Forty-Eighth Annual ACM Symposium on Theory of Computing, 684–697. https://doi.org/10.1145/2897518.2897542

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 however are little 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}(\left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right| \log \left|S\right|). In a recent preprint, Groote & Martens (2024) establish that similarity is strictly more complex than bisimilarity.

Groote, J. F., Martens, J., & Vink, Erik. P. de. (2023). Lowerbounds for bisimulation by partition refinement. Logical Methods in Computer Science, Volume 19, Issue 2. https://doi.org/10.46298/lmcs-19(2:10)2023

Groote, J. F., & Martens, J. (2024). A quadratic lower bound for simulation. https://doi.org/10.48550/arXiv.2411.14067

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.9. 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 (Note 3.1), and instantiated the approach to the strong spectrum of Glabbeek (2001). From there, we have introduced the spectroscopy problem, which asks for notions to preorder compared states (Note 3.2).

Glabbeek, R. J. van. (2001). The linear time–branching time spectrum I: The semantics of concrete, sequential processes. In J. A. Bergstra, A. Ponse, & S. A. Smolka (Eds.), Handbook of process algebra (pp. 3–99). Elsevier. https://doi.org/10.1016/B978-044482830-9/50019-9

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.

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

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 force observations in clauses of conjunctions and 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.

Bisping, B., Jansen, D. N., & Nestmann, U. (2022). Deciding All Behavioral Equivalences at Once: A Game for Linear-Time–Branching-Time Spectroscopy. Logical Methods in Computer Science, 18(3). https://doi.org/10.46298/lmcs-18(3:19)2022

Bisping, B. (2023). Process equivalence problems as energy games. In C. Enea & A. Lal (Eds.), Computer aided verification (pp. 85–106). Springer Nature Switzerland. https://doi.org/10.1007/978-3-031-37706-8_5

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

However, there is a polynomial-time part of spectrum around bisimilarity and (ready) similarity. In the next two chapters, we will first solve the spectroscopy problem for this polynomial slice and then extend to the whole strong spectrum. After that, we will also consider the weak spectrum.