Updates since Publication

The version of this document that you are reading updates the published PhD thesis with small corrections and additional information.

• In Definition 7.1, the stable finishing move now starts from an arbitrary stable conjunction position \smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle s}}, rather than only from \smash{\color{gray}(}p,\varnothing\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle s}}. This corrects the underpricing of the negation in the stability test: The defender should be able to require the budget for this test even when Q is nonempty.
• The list of game positions for Definition 7.1 correctly assigns attacker branching positions \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\eta}} to G_{\mathrm{a}}, rather than G_{\mathrm{d}}.
• In the rules for Definition 7.2, the scope of \forall q \in Q in conjunction answer and stable conjunction answer now includes the game-move premise as well as the budget and strategy-formula premises. The conclusion of the stable finishing rule explicitly refers to \smash{\color{gray}(}p,\varnothing\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle s}}, rather than to a position with an unspecified set Q.
• The overview of standard queries in Usage includes eta-simulation. The implementation summary now states that equiv.io supports more than 39 notions of the strong and weak spectrum, rather than more than 30.
• References to the silent-step spectroscopy preprint have been updated to the published journal article Bisping & Jansen (2026), Deciding all behavioral equivalences at once II: The silent-step spectrum, published in Information and Computation 313 (2026), article 105499, doi:10.1016/j.ic.2026.105499.

Bisping, B., & Jansen, D. N. (2026). Deciding all behavioral equivalences at once II: The silent-step spectrum. Information and Computation, 313, 105499. https://doi.org/10.1016/j.ic.2026.105499