Document [original]

Information and Computation 300 (2024) 105191

Contents lists available at ScienceDirect

Information and Computation

journal homepage: www.elsevier.com/locate/yinco

Characterizing contrasimilarity through games, modal logic,

and complexity ✩

Benjamin Bisping ∗, Luisa Montanari

Technische Universität Berlin, Berlin, Germany

a r t i c l e i n f o a b s t r a c t

Article history:

Received 3 April 2023

Received in revised form 14 March 2024

Accepted 7 July 2024

Available online 10 July 2024

Keywords:

Game theory

Behavioral equivalence

Modal logics

We present the ﬁrst game characterization of contrasimilarity, the weakest form of

bisimilarity. It corresponds to an elegant modal characterization of nested trees of

impossible future behavior. The game is exponential but ﬁnite for ﬁnite-state systems

and can thus be used for contrasimulation equivalence checking, of which no tool has

been capable to date. By reduction from weak trace equivalence, we establish that

contrasimilarity is PSPACE-complete. A machine-checked Isabelle/HOL formalization backs

our work and enables further use of contrasimilarity in veriﬁcation contexts.

CC BY license (http://creativecommons .org /licenses /by /4 .0/).

1. Introduction

Contrasimilarity is the weakest equivalence for systems with internal τ-transitions in van Glabbeek’s linear-time–

branching-time spectrum [2] that instantiates to strong bisimilarity if there is no internal behavior. It differs from the

more commonly used weak bisimilarity in granting the additional equalities CS :τ. (τ. X+Y) =τ. X+Y, which it shares

with coupled similarity, and C :a. (τ. X+τ. Y) =a. X+a. Y. Contrasimilarity is about “as weak as one can get” with respect

to τ-steps without losing the distinguishing power of strong bisimilarity with respect to visible behavior.

Although this position “on the edge” makes contrasimilarity (and the contrasimulation preorder) particularly interesting,

there has been only little research into it. It has been investigated as an equivalence notion justifying parallelizing trans-

formations in compilers by Bell [3], as a strong way of relating context-free processes to their encodings as push-down

automata by Baeten et al. [4,5], and as the limit of arbitrarily-nested statements about impossible futures by Voorhoeve and

Mauw [6].

In this paper, we give the ﬁrst game characterization of the contrasimulation preorder, prove its correctness, and relate

it to modal-logical characterizations. All the stronger (branching-time) notions of the linear-time–branching-time spectrum

with internal steps already have game characterizations by de Frutos Escrig et al. [7], and by Bisping and Nestmann [8]. All

the weaker (linear-time) notions can readily be characterized by slightly adapting Chen and Deng’s games [9]or Bisping

et al.’s game [10]of the linear-time–branching-time spectrum without internal steps [11]. Our contribution therefore in-

serts the last puzzle piece to have game characterizations for the whole linear-time–branching-time spectrum with internal

steps [2]. We also pinpoint contrasimilarity to be where the spectrum of equivalence problems ﬂips from polynomial time

to polynomial space complexity.

✩This article is a revised version of “A Game Characterization for Contrasimilarity” [1], extended by results on complexity and modal characterizations.

*Corresponding author.

E-mail addresses: benjamin.bisping@tu-berlin.de (B. Bisping), montanariluisa@protonmail.com (L. Montanari).

URL: https://bbisping.de (B. Bisping).

https://doi.org/10.1016/j.ic.2024.105191

creativecommons .org /licenses /by /4 .0/).

B. Bisping and L. Montanari Information and Computation 300 (2024) 105191

PcPp

◦

aEats

bEats

ττ

Rcp

Fig. 1. The reﬂexive closure of Rcp is a contrasimulation on the philosopher system from Example 1. (For colors in ﬁgures, the reader is referred to the

web version of this article.)

Contributions and Structure. This paper makes the following contributions:

•We assemble a concise overview of the bisimulation-like properties of contrasimilarity in Section 2.

•By reducing trace inclusion to contrasimulation preorder, Section 3establishes PSPACE-hardness of contrasimilarity, which

has not been done before.

•In Section 4, we present a new game for the contrasimulation preorder based on subset constructions, which is ﬁnite (albeit

exponential) for ﬁnite-state systems.

•Section 5proves the correctness of the game characterization by relating defender winning strategies and contrasimulations,

which turns out to be slightly trickier than for stronger equivalences.

•In Section 6, we show the contrasimulation game corresponds to a sensibly weakened form of Hennessy–Milner modal logic.

•Section 7discusses how our modal characterization ﬁts in nicely among other equivalences and how it can easily be adapted

to characterize the notion of stable bisimilarity.

All core deﬁnitions and proofs of this paper have been formalized in the interactive proof assistant Isabelle/HOL [12]. Lemmas

come with footnotes pointing to their Isabelle proof in the Archive of Formal Proofs [13]at https://www.isa -afp .org /entries /

Coupledsim _Contrasim .html.

What’s new? Compared to the EXPRESS/SOS 2021 publication [1], this paper adds the new PSPACE-complexity argument of

Section 3, the modal characterization of Section 6, and a deeper discussion of related characterizations in Section 7, as well

as some general small improvements.

2. Contrasimilarity: the weakest bisimilarity

Notions of equivalence formalize when two process models can be considered indistinguishable given a certain model

of communication or observation. The most famous such notion is bisimilarity, which holds if two processes can match

each other’s transitions repeatedly. Contrasimilarity is a reformulation of this, saying that every transition sequence by

one process can be matched by the other process in such a way that they could continue with their roles swapping each

time. This section explains systems with internal behavior (Subsection 2.1) and gives a formal deﬁnition of contrasimilarity

(Subsection 2.2). We then show that contrasimilarity and bisimilarity actually are the same concept unless there is internal

behavior (Subsection 2.3) and brieﬂy examine systems that are not contrasimilar (Subsection 2.4). For this section, we omit

the proofs; the Isabelle proofs can be found via the footnotes.

2.1. Systems with internal steps

In order to illustrate what kinds of systems contrasimilarity equates, we start with an example of two systems with inter-

nal communication behavior that are equivalent with respect to contrasimilarity, but not with respect to weak bisimilarity.

(The example behaves similarly to the one in [3]. Its transition system is given in Fig. 1.)

Example 1 (Dining hall philosophers). Two philosophers Aand Bwant to eat pasta. They can get their spaghetti (sp) once the

dining hall counter opens (op). However, there is only one plate (pl), which must be taken before picking up the spaghetti

B. Bisping and L. Montanari Information and Computation 300 (2024) 105191

(regardless of whether the counter has opened). We are waiting for them in the dining area outside; so we only observe

whether the counter has opened and who eats, whereas the plate and spaghetti grabbing are invisible to us.

The following CCS structure models the situation of the philosophers waiting at the counter Pcin the notation of Mil-

ner [14]. The resources correspond to sending actions like sp (which can be consumed only once) and obtaining the

resources corresponds to receiving actions like sp. The subprocesses run in parallel (...|...) and internal communication is

hidden from the outside (...\{sp}).

def

=pl.sp.aEats |pl.sp.bEats |pl |op.sp \{

pl,sp}

With sp being hidden: Does it make a difference to the observer if it is not the spaghetti counter waiting for the opening

event before handing out pasta, but rather the philosophers waiting for the event before grabbing the pasta? This would

amount to the following model of patient philosophers Pp.

def

=pl.op.sp.aEats |pl.op.sp.bEats |pl |sp \{

pl,sp}

If one’s application needs to abstract over “where exactly” internal waiting is happening, and thus equate Pcand Pp, this

suggests to pick contrasimilarity for the semantics (respectively, a weaker or incomparable equivalence).

To formally speak about the semantics of processes and programs, it is customary to express their operational semantics

as labeled transition systems, or LTS for short.

Deﬁnition 1 (LTS). A labeled transition system, (S, Actτ, −→)consists of a set of states S, of a set Actτ=Act ∪{τ}of visible

actions Act and a special internal action τ/∈Act, and of a transition relation −→⊆S×Actτ×S.

The transition system for Example 1is depicted as the black part in Fig. 1. All deadlocks are combined into the state

0. The transitions where communication internal to the system happens are labeled by τ, which denotes internal behavior.

Where there are multiple internal transitions originating from the same process state, the system performs an internal

choice. In process Pp, the internal choice happens at the start, whereas in Pc, the choice is interleaved with the observable

occurrence of op.

Unless stated otherwise, our following deﬁnitions and proofs are to be read in a context where an LTS (S, Actτ, −→)has

been ﬁxed.

Deﬁnition 2 (Transitions). We employ the following notation for transitions in the system (with p, p, q ∈S; α∈Actτ):

(1) Strong steps: p α

−→ piff (p, α, p) ∈−→.

(2) Internal steps: p =⇒ piff p τ

−→∗p.

(3) Delay steps: p α

== piff α=τwith p =⇒ por α∈Act with p =⇒ α

−→ p.

(4) Weak steps: p ˆ

=⇒ piff p α

== =⇒p.

(5) Weak word steps: p

#‰

=⇒ piff p ˆ

==⇒ ˆ

==⇒ ... ˆ

==⇒ pwith #‰

w=w0w1...wn∈Act∗or p =⇒ pfor the empty word #‰

w=ε.

(6) Absence of steps: p α

−→, p ˆ

=⇒ and p 

#‰

=⇒ to denote that certain transitions are not possible from p. pis called stable iff

p τ

−→.

(7) Lifting of steps to sets: Pα

−→ Piff P={p|∃p ∈P:p α

−→ p}, and Pα

−→ piff there is a p ∈Pwith p α

−→ p; analogously

for =⇒, α

== , ˆ

=⇒, and

#‰

=⇒.

Note that delay steps a

== differ from the more common weak steps ˆ

=⇒ (a ∈Act) in that the step ends in the a

−→-

transition with no trailing internal behavior. Also note that Pα

−→{p}is stronger than Pα

−→ pin that it rules out possible

other α

−→-transitions.

B. Bisping and L. Montanari Information and Computation 300 (2024) 105191

2.2. Deﬁning contrasimulation preorder and contrasimilarity

It is common to deﬁne notions of behavioral equivalence and behavioral preorders in terms of relations between pro-

cess states that fulﬁll certain properties. For instance, the widespread “strong bisimilarity” can be characterized through

symmetric strong simulations:

Deﬁnition 3 (Strong bisimilarity). A strong simulation is a relation Rwhere, for all (p, q) ∈Rwith p α

−→ p, there is a qwith

q α

−→ qand (p, q) ∈R. If Ris a symmetric strong simulation and two processes (p, q) ∈R, then the processes are called

strongly bisimilar (p ∼Bq).

Weak similarity and bisimilarity are deﬁned in terms of weak simulation relations, which also induce a weak simulation

preorder. Contrasimilarity is obtained by making a subtle change to the weak simulation property.

Deﬁnition 4 (Weak simulation). Aweak simulation is a relation Rwhere, for all (p, q) ∈Rwith p α

−→ p, there is a qwith

q ˆ

=⇒ qand (p, q) ∈R. We say that pis weakly simulated by q, written p WS q, iff there is a weak simulation Rwith

(p, q) ∈R. If p WS q WS p, the two are weakly similar, written p ∼WS q. If Ris a symmetric weak simulation, the

processes are called weakly bisimilar (∼WB), which implies all of the above.

On the processes of Example 1, {(p, p) |p ∈S} ∪{(Pp, Pc)}is a weak simulation because the steps from Ppare a subset

of the steps from Pc. This implies PpWS Pc. However, there is no weak simulation in the opposite direction because Pc

can op-step to a state where aEats and bEats are weakly enabled, while Ppcannot. Thus, weak similarity and hence also

weak bisimilarity distinguish the two systems.

Due to its inherent recursiveness, Deﬁnition 4can also be rephrased in terms of words instead of single actions:

Lemma 1 (Weak simulation over words). Ris a weak simulation precisely if, for all (p, q) ∈Rwith #‰

w∈Act∗and p

#‰

=⇒ p, there is a

qwith q

#‰

=⇒ qand (p, q) ∈R.1

This observation motivates why the following deﬁnition with pand qswapping sides at the end has been named

contra-simulation (alluding e.g. to “contravariance” with a comparable inversion in subtyping):

Deﬁnition 5 (Contrasimulation). Acontrasimulation is a relation Rwhere, for all (p, q) ∈Rwith #‰

w∈Act∗and p

#‰

=⇒ p, there

is a qwith q

#‰

=⇒ qand (q, p) ∈R. The contrasimulation preorder Cand contrasimilarity ∼Care deﬁned analogously to

Deﬁnition 4.

The reﬂexive closure of the relation in Fig. 1, Rcp ∪{(p, p) |p ∈S}, is a contrasimulation. Hence, Pcand Ppare con-

trasimilar, Pc∼CPp.

Let us quickly stress that the contrasimulation preorder indeed is a sensible behavioral preorder (which is not true for

its intransitive neighbors eventual simulation [3] and stability-coupled simulation [15]):

Lemma 2 (Properties of C). Some properties of the contrasimulation preorder include:

(1) Cis transitive,2as the interleaved concatenation R1R2∪R2R1of two contrasimulations R1and R2is itself a contrasimula-

tion.3

(2) Cis reﬂexive.4(More generally: p =⇒ pimplies pCp.5)

(3) Cis itself a contrasimulation6(and thus the greatest contrasimulation7).

2.3. Relationship of contra- and bi-similarity

Like the weak simulation preorder, the contrasimulation preorder is not symmetric for most systems (which also implies

∼C= C). Symmetric contrasimulations can also be used to establish bisimilarity of states:

1lemma Weak_Relations.lts_tau.weak_sim_word.

2lemma Contrasimulation.lts_tau.contrasim_trans.

3lemma Contrasimulation.lts_tau.contrasim_trans_constructive.

4lemma Contrasimulation.lts_tau.contrasim_reﬂ.

5lemma Contrasimulation.lts_tau.contrasim_tau_step.

6lemma Contrasimulation.lts_tau.contrasim_preorder_is_contrasim.

7lemma Contrasimulation.lts_tau.contrasim_preorder_is_greatest.

B. Bisping and L. Montanari Information and Computation 300 (2024) 105191

cubic

PSPACE

subcubic

strong bisimulation

strong simulation

weak bisimulation

coupled simulation

weak simulation

contrasimulation

impossible futures

weak traces

Fig. 2. Hierarchy of weak preorders / equivalences. Arrows denote implications of preordering. Thinner arrows collapse into bi-implication for systems

without internal steps. Blue parts indicate slope of decision problem complexities.

Lemma 3 (Bisimulation characterization). There is a symmetric contrasimulation Rwith (p, q) ∈Rprecisely if p ∼WB q. In particular:

•If a contrasimulation Ris symmetric, then Rmoreover is a weak (bi)simulation.8

•If a weak (bi)simulation Ris symmetric, then Rmoreover is a contrasimulation.9

Unlike weak simulations, contrasimulations are “symmetric up to internal steps.” We call this property coupling, as it

differentiates coupled simulations from weak simulations [16]:

Lemma 4 (Coupling). If Ris a contrasimulation, then (p, q) ∈Rimplies there is a qsuch that q =⇒ qand (q, p) ∈R.10

On stable states, coupling locally is the same as conventional symmetry. This is nice for systems with no internal behav-

ior:

Lemma 5 (Contra/Bi-simulation). If −→ contains no τ-steps, and Ris a contrasimulation, then Ris symmetric and thus a (strong)

bisimulation.11

Accordingly, C=∼

WB =∼

Bfor systems without internal steps. In this sense, contrasimilarity is much closer to strong

bisimilarity than weak similarity is: A weak simulation on a τ-free system is just a strong simulation but does not need to

be a bi-simulation.

The relevant hierarchy of equivalences is depicted in Fig. 2. Within the linear-time–branching-time spectrum, complexity

of the corresponding decision problems grows with the coarseness of the equivalences.12 Up to now, it has not been settled

on which side of the cliff between polynomial time and polynomial space (thus, in practice, exponential time) contrasimi-

larity lies. Fig. 2already places contrasimilarity on the PSPACE side, which will be the answer we reach over the course of

the next sections.

8lemma Contrasimulation.lts_tau.symm_contrasim_is_weak_bisim.

9lemma Contrasimulation.lts_tau.symm_weak_sim_is_contrasim.

10 lemma Contrasimulation.lts_tau.contrasim_coupled.

11 lemma Contrasimulation.lts_tau.contrasim_weakest_bisim.

12 Outside the spectrum, this does not hold. For instance, graph isomorphism is ﬁner than bisimilarity, but more complex; preordering by enabled actions

is coarser than trace inclusion, but less complex.

B. Bisping and L. Montanari Information and Computation 300 (2024) 105191

PcPl

◦

aEats

bEats

ττ

(a) The philosopher system from Exam-

ple 2.

Pab

◦

aEats

bEats

(b) Transitions of Example 3with a de-

committing τ-transition.

P

◦

aEats

bEats

step “contrasimulation.”

Fig. 3. Processes that are not contrasimilar.

2.4. No shortcuts

We already mentioned that contrasimilarity grants the equality a. (τ. X+τ. Y) =a. X+a. Y. However, this does not mean

that internal choice may commute over actions: The equality a. (τ. X+τ. Y) =τ. a. X+τ. a. Yis not sound for contrasimilarity,

as the following example illustrates:

Example 2 (Locked-out philosophers). Consider this slight modiﬁcation of Pc, where the opening op guards the plate pl instead

of the spaghetti sp:

def

=pl.sp.aEats |pl.sp.bEats |op.pl |sp \{

pl,sp}

As depicted in Fig. 3a, the result of this change is that the decision between philosophers Aand Bcan happen only after op.

The change is noticed by contrasimilarity, i.e. PcCPl. The reason is that PcCPlwith the left process resolving its

choice would imply PlCop. τ. aEats. But this does not hold because Pl

op,bEats

=====⇒0but not op. τ. aEats op,bEats

=====⇒0.

Weak similarity, by the way, equates the two Pc∼WS Pl.

It is also worthwhile to observe that, in general, the deﬁnition of contrasimulation (Deﬁnition 5) cannot straightforwardly

be simpliﬁed to use single steps ˆ

=⇒ instead of words

#‰

=⇒, as is the case with its ﬁner siblings like weak bisimulation. Such

a simpliﬁcation of contrasimulation is used by de Hoop [5]. However, this is not sound for general systems due to the

alternating sides in the deﬁnition.

Example 3 (Instable choice). Consider Pab

def

=op. (aEats +τ. bEats)and Pb

def

=op. bEats whose transitions can be found in

Fig. 3b. The processes are clearly not even weakly trace equivalent. But they are single-step “contrasimilar”, as both Pab

=⇒

aEats +τ. bEats and Pab

=⇒ bEats (matched by Pb

=⇒ bEats) lead to a situation that would (contra-)simulate bEats.

The counter-example can be generalized as hinted at in Fig. 3c, which would need at least a word length of four to

distinguish the named processes.

This implies that contrasimilarity somehow contains the complexities of word moves

#‰

=⇒, and thus of trace equivalences.

We will make this more precise in the next section.

3. Hardness of contrasimilarity

Contrasimilarity inhabits a unique position among equivalence notions in terms of hardness. All of the more common

ﬁner equivalences, such as contrasimilarity’s closest sibling, coupled similarity, can be decided in cubic time [8]. However,

B. Bisping and L. Montanari Information and Computation 300 (2024) 105191

Fig. 4. Example of a τ-sink expansion with Sin black and S⊥\Sin red.

coarser notions such as weak trace equivalence are PSPACE-complete [17]. In this section, we demonstrate that contrasimi-

larity, unfortunately, lies on the harder side of the exponentiality cliff. We do so by establishing a reduction from the trace

inclusion problem to the contrasimulation preordering problem.

Deﬁnition 6 (Weak trace inclusion). The set of weak partial traces13 of a state pis deﬁned as Tr(p) := {#‰

w∈Act∗|∃p:p

#‰

=⇒

p}. We write p Tqand say that pis trace-included by qif Tr(p) ⊆Tr(q). If p Tqand q Tp, the processes are called

trace-equivalent, p ∼Tq.

We deﬁne a τ-sink expansion of a transition system such that a state pis contrasimulated by a state qif and only if p

is trace-included by qon the system’s τ-sink expansion. The idea is to add a sink state to the system to which every state

can make a strong τ-transition. The sink itself has no outgoing transitions except for a reﬂexive τ-step.

Deﬁnition 7 (τ-sink expansion). Let S=(S, Actτ, −→)be an LTS. We deﬁne the τ-sink expansion S⊥of Sas

S⊥=(S∪{⊥},Actτ,−→∪{(p,τ,⊥)|p∈S∪ {⊥}}).

For clarity, we write p, q, ... for states belonging to Sand index all relations that refer to the expanded system S⊥with ⊥.

Fig. 4shows an example of a τ-sink expansion for some S.

Observe that weak traces are invariant with respect to τ-sinks. We can therefore decide weak trace inclusion (and

equivalence) on an instance Sby deciding it on its τ-sink expansion S⊥.

Lemma 6 (τ-sink invariance of weak traces). We have p Tqiff p T⊥qfor p, q ∈S.14

Proof. The addition of τ-sinks does not affect which words are reachable from a given state p. We therefore have Tr(p) =

Tr⊥(p)for all p ∈Sand thus p Tqiff p T⊥q.

Furthermore, weak trace inclusion and the contrasimulation preorder coincide for systems with τ-sinks.

Lemma 7 (Equivalence on τ-sink expansions). We have p T⊥qiff p C⊥q.15

Proof. Since Tis a coarser preorder than Cfor every system, we trivially have p T⊥qif p C⊥q. Now let Rbe the

maximal sub-relation of T⊥on the domain (S∪{⊥}) ×(S∪{⊥}). Let us assume p T⊥qor, equivalently, p Rq. Observe

ﬁrst that a τ-sink ⊥is trace-included by all possible states p: Since no word is reachable from a τ-sink, ⊥ Rpis trivially

satisﬁed. We now ﬁx a state pand a word #‰

wsuch that p

#‰

=⇒⊥p. By our assumption p Rq, there must therefore be a

state qsuch that q

#‰

=⇒⊥q. Since any state can make a τ-transition to ⊥, we have q

#‰

=⇒⊥q=⇒⊥⊥and therefore q

#‰

=⇒⊥⊥.

With ⊥ Rp, this implies that Ris a contrasimulation, and thus p C⊥q.

With these results, we can conclude that deciding the contrasimulation preorder must be at least as hard as deciding

trace inclusion, and the same for their equivalences:

Theorem 8. Every decision procedure for C(resp. ∼C) on a system Swith running time O(g(t)) can be used to decide T(resp. ∼T)

in running time O(g(2t)), where t=|−→| is the number of transitions in the system and gis some strictly increasing function.

13 deﬁnition Weak_Relations.lts_tau.trace_inclusion.

14 lemma Tau_Sinks.trace_inclusion_sink_invariant.

15 lemma Tau_Sinks.lts_tau.contrasim_trace_incl_equiv_on_sink_expansion.

B. Bisping and L. Montanari Information and Computation 300 (2024) 105191

Proof. Lemmas 6and 7imply that p Tqiff p C⊥q(and also p ∼Tqiff p ∼C⊥q). Deciding trace inclusion on a system S

therefore reduces to deciding contrasimulation preorder on S⊥, and so does trace equivalence to contrasimilarity. The size

increase from Sto S⊥is bounded by a factor of 2 since we add a single state and |S| +1 ∈O(|−→||)transitions. Because

we can transform Sto S⊥in linear time, we arrive at an overall runtime of O(g(2t)) for deciding trace inclusion and

equivalence this way. 

As the decision problems for trace inclusion and trace equivalence are PSPACE-complete [17,18], this immediately im-

plies:

Corollary 9 (Hardness of contrasimilarity). Deciding contrasimilarity as well as deciding contrasimulation preorder is PSPACE-hard.

Remark 1. We have only formalized the core of the reduction argument, but not the ﬁnal hardness argument in Isabelle/HOL

because the concepts of complexity and hardness are elusive at the level of abstraction of our Isabelle formalization.

Also, Hüttel and Shukla’s survey of complexities [18]does not directly consider weak traces, but only conventional

(strong) traces. For hardness, this makes no difference, given that strong trace inclusion on a system without τ-transitions

is just the same as weak trace inclusion.

4. The contrasimulation game

The contrasimulation preorder can be characterized by a game between two opposing players, the attacker and the

defender. For a given p, q ∈S, the attacker seeks to disprove p Cq, while the defender seeks to maintain p Cq. We ﬁrst

introduce some general thoughts about such games in Subsection 4.1, and then present the contrasimulation game at the

core of our contribution in Subsection 4.2.

4.1. Preliminaries

For this paper, we use Gale-Stewart-style games in the tradition of Stirling [19] where the attacker wins by getting the

defender stuck, and the defender wins by not getting stuck.

Deﬁnition 8 (Games). A simple reachability game G[g0] =(G, Gd, , g0)consists of

•a set of game positions G, partitioned into

–a set of defender positions Gd⊆G

– and attacker positions Ga:= G \Gd,

•a graph of game moves ⊆G ×G, and

•an initial position g0∈G.

Deﬁnition 9 (Plays and wins). We call the inﬁnite and ﬁnite paths g0g1...∈G∞with gigi+1plays of G[g0]. The defender

wins inﬁnite plays. If a ﬁnite play g0...gnis stuck, the stuck player loses: The defender wins if gn∈Ga, and the attacker

wins if gn∈Gd. Equivalently, the defender wins precisely those plays in which the defender is not stuck.

Deﬁnition 10 (Strategies). An attacker strategy is a partial mapping from initial play fragments to next moves f⊆

{(g0...gn, gn+1) ∈G∗×Ga|gngn+1}. We call f positional if f(g0...gn)only depends on the last position gn. A play g

is consistent with an attacker strategy fiff, for each move gigi+1with gi∈Gawhere f(g0...gi)is deﬁned, we have

gi+1=f(g0...gi). We denote the set of plays gconsistent with fby G∞

f[g0]for the initial game position g0. Defender

strategies are deﬁned analogously.

Deﬁnition 11 (Winning strategies and winning regions). If fis a player strategy and every stuck or inﬁnite play g∈G∞

f[g0]is

won by that player, then fis a winning strategy for the initial position g0. The player with a winning strategy for G[g0]is

said to win G[g0]. The attacker winning region Wa⊆Gcontains all positions gwhere the attacker wins G[g]. The defender

winning region is deﬁned analogously.

All simple reachability games are determined, that is, either the defender or the attacker wins. The winning regions of

ﬁnite simple games can be computed in linear time in the number of game moves. It is therefore desirable to ﬁnd ﬁnite

game characterizations of equivalences. For many weak equivalences, such characterizations can be obtained directly from

their standard coinductive characterization.

For contrasimilarity, this direct route is less helpful due to its word-based deﬁnition. That is why we only brieﬂy discuss

it here, and then move on to a different approach in the next subsection.

B. Bisping and L. Montanari Information and Computation 300 (2024) 105191

(p,q)a(#‰

w,p,q)d(q,p)a

#‰

=⇒ p] [q

#‰

=⇒ q]

Fig. 5. Schematic basic contrasimulation game. Boxes denote attacker positions, circles denote defender positions and arrows denote game moves. Each

game move is only possible if the condition in square brackets is satisﬁed. Dashed boxes are attacker positions with a new variable assignment and admit

analogous moves to the solid boxes.

If we directly transfer Deﬁnition 5into a game, we arrive at the following game alternating between attacker and

defender: The attacker may challenge p Cqby selecting a word #‰

w∈Act∗and a p∈Swith p

#‰

=⇒ p, to which the

defender has to name a q∈Swith q

#‰

=⇒ q. The sides of the game then swap, and the attacker can go on to question

qCp. The attacker wins if the defender is unable to answer with an appropriate q, and the defender wins if the play

goes on forever.

A schematic model of the basic contrasimulation game is given in Fig. 5. We proved its correctness in the Isabelle

formalization.16 Unfortunately, in ﬁnite-state systems with cycles, the attacker can challenge with inﬁnitely many words.

Such games will have an inﬁnite number of game positions and player moves, even for ﬁnite systems. We consequently

decided not to devote more space to this game. We rather move on to a set-based game in the following subsection.

4.2. The game

Let us now turn to the contrasimulation game that is the core contribution of this paper. The idea is to restrict the

attacker’s moves to single actions α∈Actτand perform a subset construction on states the defender might reach in the

right-hand component of game positions. We thus break the attacker’s word challenge for p Cqinto a simulation phase

and a swap request. During the simulation phase, the defender plays a set of states, which collapses at the swaps:

Deﬁnition 12 (C-game). For a transition system (S, Actτ, −→), the contrasimulation set game GC[g0] =(G, Gd, , g0)consists

•attacker positions (p,Q)a∈Gawith p ∈S, Q⊆S,

•defender simulation positions Sim(a,p,Q)d∈Gdwith a ∈Act, p ∈S, Q⊆S, and

•defender swapping positions Swap(p,Q)d∈Gdwith p ∈S, Q⊆S

and the following game moves

•simulation challenges (p,Q)aSim(a,p,Q)dif p a

== p,

•swap challenges (p,Q)aSwap(p,Q)dif p =⇒ p,

•simulation answers Sim(a,p,Q)d(p,Q)aif Qa

== Q, and

•swap answers Swap(p,Q)d(q,{p})aif Q=⇒ q.17

Practically, we will use attacker positions (p,{q})afor p, q ∈Sas initial positions g0in instantiations to characterize p Cq.

A schematic model of the game is given in Fig. 6.

Beginning from some position (p,{q})a, the attacker challenges the defender to successively simulate the actions wiof

a word #‰

w=w0...wnin the simulation phase. In response, the defender does not play a single state, but rather the set of

all states reachable by the known preﬁx w0...wkof #‰

w. When the attacker is done choosing #‰

win p

#‰

=⇒ p,they request

a swap. The defender must then select a speciﬁc state qwith q

#‰

=⇒ qfrom their state set. The players then change sides

and the attacker may now challenge qCp. Hence, the defender postpones the decision of how exactly to simulate the

challenged word until a swap is requested.

Example 4 (Contrasimulation game on Pc, Pp). A possible play of GCfor the philosopher transition system from Example 1

would be:

(Pc,{Pp})aSim(op,AB,{Pp})d(AB,{τ.aEats,τ.bEats})aSwap(τ.aEats,{τ.aEats,τ.bEats})d

(τ.aEats,{τ.aEats})aSim(aEats,0,{τ.aEats})d(0,{0})aSwap(0,{0})d....

16 theorem Contrasim_Word_Game.c_word_game.winning_strategy_in_c_word_game_iff_contrasim.

17 locale Contrasim_Set_Game.c_set_game.

B. Bisping and L. Montanari Information and Computation 300 (2024) 105191

(p,Q)a

Sim(a,p,Q)d

Swap(p,Q)d

(p,Q)a

(q,{p})a

[pa

== p]

[p=⇒ p]

[Qa

== Q]

[Q=⇒ q]

Fig. 6. Schematic contrasimulation set game (Deﬁnition 12).

The play ends in an inﬁnite loop of swaps and is thus won by the defender. The crucial point of this game is the defender

move highlighted in blue, where the defender answers a swap challenge by matching the states on both sides. After this, it

becomes impossible for the attacker to win. If the defender picked τ. bEats instead, they would lose. However, the defender

has a winning strategy no matter which moves the attacker chooses for GC[(Pc,{Pp})a].

The subset construction is a necessary evil in the switch from word moves to single-action moves: The defender does

not know the full word #‰

wthat the attacker will choose, but only the word preﬁx w0...wkchallenged up to this point

k ≤n. Deciding for single states early would thus put the defender at a disadvantage: There might be several states q

with q

# ‰

w0...wk

=====⇒qfor every such k, of which only some also satisfy q

# ‰

w0...wk

=====⇒q

# ‰

wk+1...wn

======⇒q for any q ∈S. Dually, forcing

early swapping would be disadvantageous to the attacker when the attack has to pass through instable states as seen in

Example 3.

Crucially, this construction yields a ﬁnite game for any ﬁnite-state system. As with the well-known subset construction

when transforming nondeterministic into deterministic ﬁnite automata, the game size is exponential in the size of the state

space S.

We chose to present the game as an alternating game where attacker and defender take turns. Several modiﬁcations

could be made to simplify some aspects of the game: Note, for example, that the Sim(...)

d-positions are not strictly

necessary, as the defender has exactly one move originating from each such position. Additionally, parts of the game moves

could be broken up into smaller steps on −→ instead of == . However, both changes would make the game non-alternating.

For the purpose of this paper, especially for intuitive proofs like in the following section, we consider the alternating

formulation superior.

5. Correctness of the contrasimulation game

Let us now demonstrate that the C-game does indeed correspond to the contrasimulation preorder in the sense that the

defender wins the game GC[(p,{q})a]precisely if p Cq. In Subsection 5.1, we ﬁrst establish soundness of the characteriza-

tion, that is, defender winning strategies in the game imply contrasimulations on the transition system. Subsection 5.2 then

shows completeness of the characterization by constructing a defender winning strategy from the greatest contrasimulation.

Our proofs must bridge the gap between the single-action game and the word-transition deﬁnition of the contrasimu-

lation property. While transition relations on single actions usually are non-deterministic, the transitions lifted to sets of

states are deterministic. To exploit this in proofs, we ﬁrst deﬁne the word successor function from delay steps:

Deﬁnition 13. We deﬁne the word successor function dsuccs :Act∗×2S→2Srecursively as follows:18

dsuccs(ε,Q)=Q

dsuccs(#‰

wa,Q)={q|dsuccs(#‰

w,Q)a

== q}

In this way, dsuccs computes the set of states reachable with a given word #‰

wfrom a starting set Q. Note that

dsuccs(#‰

w, Q)will return the empty set if no state in Qadmits a

#‰

=⇒-transition.

18 primrec Weak_Transition_Systems.lts_tau.dsuccs_seq_rec.

B. Bisping and L. Montanari Information and Computation 300 (2024) 105191

Lemma 10. Let #‰

w∈Act∗be a word and let q, qbe states in S. Then q

#‰

=⇒ qimplies dsuccs(#‰

w, {q}) =⇒ q.19 Furthermore, q∈

dsuccs(#‰

w, {q})implies q

#‰

=⇒ q.20

5.1. Soundness of the contrasimulation game

Let us ﬁrst show that the C-game is sound with respect to the contrasimulation preorder, that is, p Cqholds if the

defender wins GC[(p,{q})a]. To this end, we prove an intermediate result stating that the defender is always able to answer

simulation challenges over the preﬁx #‰

vof a nonempty word #‰

w=#‰

n. Furthermore, if the simulation phase over #‰

vwas

started from some attacker position (p,{q})a, then the defender state set at the end of the phase corresponds exactly to

dsuccs(#‰

v, {q}). We will use this result in later proofs to “fast-forward” the game to a state where the simulation phase has

been completed and a swap request may be initiated.

Lemma 11 (Word challenge building). Let f be a defender strategy on GC[g0]for some g0∈Gand let (p,{q})abe an attacker position

in a play consistent with f. Let #‰

w=#‰

n∈Act∗be a nonempty word and assume p

#‰

=⇒ pfor some p∈S. Then there exist p0, p1∈S

with p

#‰

=⇒ p0

=== p1=⇒ psuch that the defender position Sim(wn,p1,dsuccs(#‰

v,{q}))dcan be reached in some play consistent

with f.

Proof. We will prove this by nonempty induction on #‰

w=#‰

n∈Act∗:

•Base Case: #‰

w=wn=εwn.

From p wn

==⇒ pwe know there exists a p1such that p wn

=== p1=⇒ p. Hence, the attacker can move from (p,{q})ato

Sim(wn,p1,{q})d=Sim(wn,p1,dsuccs(ε,{q}))d. This play is still consistent with fas fis only deﬁned for defender

moves.

•Induction step: #‰

w=#‰

nfor some nonempty word #‰

v∈Act∗.

Then there exists a #‰

u∈Act∗such that #‰

v=#‰

n−1and p

#‰

=⇒ p0

wn−1

===⇒p1

==⇒ pfor some p0, p1∈S. We

assume the lemma holds for #‰

v, i.e. there exists a p01 ∈Swith p0

wn−1

===== p01 =⇒ p1such that the position

Sim(wn−1,p01,dsuccs(#‰

u,{q}))dcan be reached in some play consistent with f.

Because there always exists a (potentially empty) set Qwith dsuccs(#‰

u, {q}) wn−1

===== Q, the defender is not stuck at

Sim(wn−1,p01,dsuccs(#‰

u,{q}))d. There must therefore exist a position (p01,Q)a=f(g0...Sim(wn−1,p01,dsuccs(#‰

u,{q}))d

that the defender can move to. For Qwe have

Q={q|dsuccs(#‰

u,{q})wn−1

===== q}=dsuccs(#‰

n−1,{q})=dsuccs(#‰

v,{q}).

From our assumptions p01 =⇒ p1and p1

==⇒ pwe can infer the existence of a p

1with p01 =⇒ p1

=== p

1=⇒ p,

which we can shorten to p01

=== p

1=⇒ p. Hence, the attacker can move from (p01,Q)ato Sim(wn,p

1,Q)d=

Sim(wn,p

1,dsuccs(#‰

v,{q}))d, and therefore the defender position Sim(wn,p

1,dsuccs(#‰

v,{q}))dis reachable in a play

consistent with f. Furthermore, the second implication p

#‰

=⇒ p01

=== p

1=⇒ pfollows immediately from p

#‰

=⇒ p0

wn−1

=====

p01

=== p

1=⇒ pand #‰

v=#‰

n−1.

With this result, we are now able to prove the soundness of the C-game.

Lemma 12 (Soundness of the C-game). Let fbe a winning strategy for the defender on GC[(p0,{q0})a]for some p0, q0∈S. Then

we have p0Cq0.22

Proof. We construct a relation R ⊆S×Swhere

R={(p0,q0)}∪{(q,p)|∃g∈G∞

f[(p0,{q0})a]:∃k∈N:∃Q⊆S:gk=Swap(p,Q)d∧gk+1=(q,{p})a}.

Informally, Rcontains the states p0, q0of the initial position (p0,{q0})aand the states of all attacker positions following

a defender swap position in any play consistent with f. We claim that Ris a contrasimulation: Let p, p, q ∈Sbe states

and assume (p, q) ∈Rand p

#‰

=⇒ pfor some #‰

w∈Act∗. We will show that a state q∈Sexists such that q

#‰

=⇒ qand

(q, p) ∈R.

Since (p, q) ∈R, there exists a g∈G∞

f[(p0,{q0})a]and a k ∈N∪{−1}such that gk+1=(p,{q})ais an attacker position

in g. We will distinguish between empty and nonempty words #‰

19 lemma Weak_Transition_Systems.lts_tau.word_reachable_implies_in_dsuccs.

20 lemma Weak_Transition_Systems.lts_tau.in_dsuccs_implies_word_reachable.

21 lemma Contrasim_Set_Game.c_set_game.csg_defender_can_simulate_preﬁx.

22 lemma Contrasim_Set_Game.c_set_game.contrasim_set_game_sound.

B. Bisping and L. Montanari Information and Computation 300 (2024) 105191

•Case 1: #‰

w=ε.

By assumption, we have p ε

=⇒ pand thus p =⇒ p. Hence, the attacker can move from (p,{q})ato a defender position

Swap(p,{q})d. Because fis a winning strategy, the defender is not stuck at Swap(p,{q})d; there must therefore exist a

state q∈Ssuch that the defender can move to the position f(g0...Swap(p,{q})d) =(q,{p})a. It follows that q =⇒ q

and that there exists a play g∈G∞

f[(p0,{q0})a]in which (q,{p})acan be reached. Since the last position played is a

Swap(...)

dnode, we therefore have (q, p) ∈Rby our construction of R.

•Case 2: #‰

w=#‰

nfor some #‰

v∈Act∗and wn∈Act.

By Lemma 11, we know there exist p0, p1with p

#‰

=⇒p0

=== p1=⇒psuch that the position Sim(wn,p1,dsuccs(#‰

v,{q}))d

can be reached in some play g∈G∞

f[(p0,{q0})a]. Because fis a winning strategy, the defender is not stuck

at Sim(wn,p1,dsuccs(#‰

v,{q})d; there must therefore exist a set Q1allowing the defender to move to a position

f(g0...Sim(wn,p1,dsuccs(#‰

v,{q}))d) =(p1,Q1)a. For Q1we have

Q1={q1|dsuccs(#‰

v,{q})wn

=== q1}=dsuccs(#‰

n,{q})=dsuccs(#‰

w,{q}).

By our assumption p1=⇒ p, the attacker can keep moving to a defender position Swap(p,Q1)d. Again, the defender

is not stuck, and there exists a q∈Sallowing the defender to move to the position f(g0...Swap(p,Q1)d) =(q,{p})a.

It follows that Q1=⇒ q. For qwe have

q∈{q|∃q1∈Q1:q1=⇒ q}

q|∃q1∈dsuccs(#‰

w,{q}):q1=⇒ q}

⊆{

q|∃q1∈dsuccs(#‰

w,{q}):q

#‰

=⇒ q1∧q1=⇒ q}(Lemma 10)

⊆{q|q

#‰

=⇒ q}.

Hence, there exists a qsuch that q

#‰

=⇒ qand the position (q,{p})ais reachable from a play consistent with f. Then

we also have (q, p) ∈R, since the last played position was a Swap(...)

dnode.

Thus, Ris a contrasimulation by Deﬁnition 5. From (p0, q0) ∈Rthen follows p0Cq0.

5.2. Completeness of the contrasimulation game

Let us now prove that the C-game is complete with respect to the contrasimulation preorder, that is, the defender wins

GC[(p,{q})a]if p Cq. To this end, we deﬁne an auxiliary function trace_expansion with which we are able to construct a

defender strategy fCfrom the contrasimulation preorder C. We will prove that if p Cq, then fCis a winning strategy for

the defender on GC[(p,{q})a].

Our ﬁrst step is to rephrase the contrasimulation preorder into a form that will make it a little easier for us to relate

it to game positions: We deﬁne a relation C⊆S×2Swith C={(p, {q}) |p Cq}. We then expand Cto also include all

tuples (p, Q)that can be reached from any (p, {q}) ∈Cwith a weak delay word transition. This expanded relation can be

constructed by applying the following function trace_expansion :2S×2S→2S×2Sto C: 23

trace_expansion(R)={(p,dsuccs(#‰

w,Q)) |∃p∈S:(p,Q)∈R∧p

#‰

=⇒ p}

The motivation behind trace_expansion(C)becomes clear when we relate it back to the game: For any p Cq,

trace_expansion(C)contains the tuples of all possible word successor sets of qthat simulate word successors of pbe-

fore a side swap has occurred. These are precisely the players’ states (or state sets) captured in the simulation phase of the

game: The attacker has chosen a preﬁx of the word to simulate, but has not yet triggered a switch of positions.

Lemma 13 (Monotonicity). We have R ⊆trace_expansion(R)for all R ⊆S×2S.24

Lemma 14 (Existence of successor states). Let a ∈Act and let p, p∈Sbe states and Q⊆Sbe a set of states such that (p, Q) ∈

trace_expansion(C).

•If p a

== p, then there exists a set Q⊆Ssuch that Qa

== Qand (p, Q) ∈trace_expansion(C),25 and

•if p =⇒ p, then there exists a state q∈Ssuch that Q=⇒ qand (q, {p}) ∈trace_expansion(C).26

23 deﬁnition Contrasimulation.lts_tau.mimicking.

24 lemma Contrasimulation.lts_tau.R_is_in_mimicking_of_R.

25 lemma Contrasimulation.lts_tau.mimicking_of_C_guarantees_action_succ.

26 lemma Contrasimulation.lts_tau.mimicking_of_C_guarantees_tau_succ.

B. Bisping and L. Montanari Information and Computation 300 (2024) 105191

Proof. By construction of trace_expansion and our assumption (p, Q) ∈trace_expansion(C), we know there exist states

p0, q0∈Ssuch that (p0, {q0}) ∈C, p0

#‰

=⇒ pand Q=dsuccs(#‰

w, {q0})for some #‰

w∈Act∗. Hence, we also have p0Cq0.

We distinguish between τ-steps and delay steps:

•For p a

== p, we have p0

#‰

=⇒ p a

== pand thus p0

#‰

==⇒ p. With p0Cq0, there must then exist a q∈Ssuch that

#‰

==⇒ q. It follows from Lemma 10 that dsuccs(#‰

wa, {q0}) =⇒ q. For Q:= dsuccs(#‰

wa, {q0}), we then have (p, Q) ∈

trace_expansion(C)by our construction of trace_expansion and Qa

== Qby Deﬁnition 13.

•For p =⇒ p, we have p0

#‰

=⇒ p =⇒ pand thus p0

#‰

=⇒ p. With p0Cq0, there must then exist a q∈Ssuch that q0

#‰

=⇒ q

and qCp. Thus, we have (q, {p}) ∈C⊆trace_expansion(C)and q∈dsuccs(#‰

w, {q0}) =Qby application of Lemma 10.

It follows immediately that Q=⇒ q.

We can now construct a positional defender strategy fCusing trace_expansion(C).

Deﬁnition 14 (Defender strategy fCon GC). Wherever possible, a defender strategy fCderived from trace_expansion(C)maps

the current play fragment g0...gkto next positions as follows:

•If the last played position gkis a swap node Swap(p,Q)d, move to some attacker position (q,{p})awith (q, {p}) ∈

trace_expansion(C)and Q=⇒ q, and

•if the last played position gkis a simulation node Sim(a,p,Q)d, move to the attacker position (p,Q)awhere Qa

==

Q.27

Where there are no applicable moves, we leave fCundeﬁned. Note that there may exist several strategies satisfying

these conditions. In the following, fCis one of these defender strategies—it makes no difference which one.28

Lemma 15 (trace_expansion invariant). Let p0, q0∈Sbe states and let gbe a play of GC[(p0,{q0})a]consistent with fC. If p0Cq0,

then we have (p, Q) ∈trace_expansion(C)for all attacker positions (p,Q)ain g.29

Proof. This follows immediately from C⊆trace_expansion(C)for the initial position (p0,{q0})a. All other attacker positions

can only be reached if the defender moves to them, and, following fC, the defender always moves in accordance with

trace_expansion(C).

Lemma 16 (Completeness of the C-game). Let p0, q0∈Sbe states with p0Cq0. Then fCis a winning strategy on GC[(p0,{q0})a].30

Proof. We show by induction on g∈G∞

fC[(p0,{q0})a]that the defender is never stuck. Let g=g0g1...gkbe the current

play fragment on GC[(p0,{q0})a].

At the initial position g0=(p0,{q0})a, the defender cannot be stuck, since g0is an attacker position. We will assume

the lemma holds for the current play fragment g0...gk. For gk+1we have two cases:

•gk+1is an attacker position. Then the defender cannot be stuck by the same reasoning as for the base case.

•gk+1is a defender position. Then there exists a position gk=(p,Q)afrom which the attacker has moved to gk+1,

therefore (p, Q) ∈trace_expansion(C)must hold by Lemma 15. We will distinguish between types of defender positions

for gk+1:

–gk+1=Sim(a,p,Q)dis a simulation position. Then we have p a

== p. From Lemma 14 and (p,Q)∈trace_expansion(C)

we can deduce that there is a set Q⊆Ssuch that Qa

== Qand (p, Q) ∈trace_expansion(C). Thus, the defender can

move to (p,Q)awith fCand is therefore not stuck.

–gk+1=Swap(p,Q)dis a swapping position. Then we have p =⇒ p. From Lemma 14 and (p, Q) ∈trace_expansion(C),

it follows that there exists a state q∈Ssuch that Q=⇒ qand (q, {p}) ∈trace_expansion(C). Thus, the defender can

move to (q,{p})awith fCand is therefore not stuck.

Hence, the defender is never stuck in a play consistent with fC, and thus fCis a winning strategy for the defender. 

Combining Lemma 12 and Lemma 16, we get:

27 fun Contrasim_Set_Game.c_set_game.strategy_from_mimicking_of_C.

28 In our Isabelle/HOL formalization, we used its Hilbert’s choice operator SOME.

29 lemma Contrasim_Set_Game.c_set_game.c_set_game_strategy_retains_mimicking.

30 lemma Contrasim_Set_Game.c_set_game.contrasim_set_game_complete.

B. Bisping and L. Montanari Information and Computation 300 (2024) 105191

Theorem 17 (Correctness of the C-game). The defender wins GC[(p,{q})a]precisely if p Cq.31

5.3. Algorithmic complexity and PSPACE-completeness of contrasimilarity

The correctness of the game has further implications for the complexity of contrasimulation checking. Recalling the

results in Section 3, we can conclude the following:

Theorem 18 (Complexity of contrasimilarity). Deciding contrasimulation preorder (resp. contrasimilarity) is PSPACE-complete.

Proof. Due to Theorem 17, a PSPACE-algorithm to decide the contrasimulation preorder can be constructed from the game:

Unfold and traverse the game graph up to depth |S|, looking for an attacker winning position. This only requires bookkeeping

of the path currently visited, which may need up to |S|2space. By invoking the algorithm a second time with the starting

states swapped, it also checks contrasimilarity.

PSPACE-hardness has already been established in Corollary 9.

For a much more time-eﬃcient implementation, one might of course want to memoize the explored game graph and

attacker-won positions instead of only the current path. But this will take up exponential space.

Remark 2 (Comparing sizes of equivalence games). Due to the subset construction, the presented contrasimulation game needs

exponentially many game positions. Compared to deﬁning the equivalence games on words as Chen and Deng [9], the subset

construction is still preferable, as it directly yields ﬁnite games for ﬁnite-state systems. Our hardness result entails that the

complexity is necessary for contrasimulation games.

Finer weak bisimulation variants have polynomial games. De Frutos Escrig et al.’s games for branching, delay, ηand weak

bisimulation [7] and Bisping’s for coupled simulation [16]are polynomial in the size of the system state space.

For weak equivalence games and algorithms, an important nuance lies in how to handle the transitive closure of internal

steps =⇒, as it might be signiﬁcantly bigger than the size of τ

−→. In the games for branching/delay/η-bisimulation [7]and

coupled simulation [16], the closure is handled at the level of the game, meaning that only |τ

−→| and not |=⇒| appears as a

factor for the game size. The key trick for the size-reduction is having the defender move gradually through τ

−→-transitions

instead of giving a “big-step” ·

== answer.

A similar trick of gradual τ

−→-steps for the defender-side does not make sense in the context of our subset construction

for contrasimulation, as the defender does not get to pick their q ∈Qbefore the next visible action. Effectively, a gradual

formulation would lead to even more permutations of Q-sets that can appear in the game!

On the attacker-side, one can break up the challenge for contrasimulation with attacks referring to τ

−→ and a

−→ instead

of p a

== p. Bisping and Jansen’s spectroscopy game [20]does this, building on the present work to have one general

equivalence game for the whole spectrum with silent steps.

6. Modal-logical view on the game

Behavioral equivalence relations can also be understood through modal logic, where two states are equivalent if and only

if they satisfy the same formulas. This goes back to Hennessy and Milner [21] and their modal-logical characterizations of

strong and weak bisimilarity. We will demonstrate that contrasimilarity can also be characterized by a weakened variant

of the classic Hennessy–Milner logic. For this, we connect distinguishing formulas and winning attacker strategies in the

C-game.

6.1. Inﬁnitary Hennessy–Milner logic

Hennessy–Milner logic is an extension of propositional logic with a modal possibility operator, interpreted over labeled

transition systems. We use the inﬁnitary variant where conjunctions may have inﬁnite width. First, we explain the “strong”

variant and later turn to a construct to account for internal steps of “weak” observations in Subsection 6.2.

Deﬁnition 15 (HML and distinctions). We deﬁne Hennessy–Milner logic by the following grammar32:

ϕ::= aϕ|¬ϕ|i∈Iϕi,where a∈Act and Iis some index set.

We deﬁne the satisfaction relation |=⊆(S×HML)where

•p |= aϕif there exists a psuch that p a

−→ pand p|= ϕ,

31 theorem Contrasim_Set_Game.c_set_game.winning_strategy_in_c_set_game_iff_contrasim.

32 datatype HM_Logic_Inﬁnitary.HML_formula.

B. Bisping and L. Montanari Information and Computation 300 (2024) 105191

Pd0QL

aaa

Fig. 7. Two non-bisimilar states P,Qthat cannot be distinguished by any HML-formula of ﬁnite depth.

•p |= ¬ ϕif not p |= ϕ, written p |= ϕ, and

•p |= i∈Iϕiif p |= ϕifor all i ∈I.33

We say that ϕ∈HML distinguishes p from qif p |= ϕand q |= ϕ. A formula ϕdistinguishes pfrom a set Qof states if ϕis

true for pand false for each q ∈Q.

Note that the innermost leaves of the syntax will always have the form i∈∅ϕi(or i∈∅¬ϕi), which usually is written

. We have not explicitly deﬁned disjunction, but clearly i∈Iϕican be expressed by ¬i∈I¬ϕi.

Also note that we have not constrained the index sets Ito be ﬁnite, which provides us with the possibility of expressing

inﬁnite-breadth conjunctions. This is necessary to have HML distinguish precisely the processes that are not bisimilar, no

matter the size of the transition system. Otherwise, HML would be too weak as can be seen from the following standard

example.

Example 5 (Inﬁnite branching and conjunctions). Consider the two states Pand Qdepicted in Fig. 7. For every natural number

i ∈N, there exists a path consisting of i-many a

−→-steps from the initial states Pand Q. Qadditionally has a way to perform

an unbounded sequence of a-steps by moving to L. This possibility renders Pand Qnon-bisimilar.

But no HML formula with ﬁnite modal depth can tell the two states apart, as arbitrarily deep observations might be

needed to kill off all the di. In the classical Hennessy–Milner theorem [22], such situations are circumvented by imposing

image-ﬁniteness on the system.

However, inﬁnitary HML as we are using it here, can readily distinguish the two: A formula ϕifor each diand a “limit

formula” ϕare given by

ϕ0:= 

ϕi+1:= aϕi

ϕ:= ai∈Nϕi.

ϕis true for Qbut false for P. More generally, HML characterizes strong bisimilarity, no matter the branching degree of the

transition system.

Remark 3. Although it does allow inﬁnite syntax trees, Deﬁnition 15 is to be understood as inductive. By deﬁnition, HML

syntax trees are still well-founded, that is, ruling out inﬁnite chains. We can thus perform structural induction.

In particular, we do not include inﬁnitely nested formulas like “aω” that would follow from a co-inductive reading of

the deﬁnition. For a deeper exploration of such Hennessy–Milner logic variants, see van Glabbeek’s “inﬁnitary linear-time–

branching-time spectrum” in [11].

In the Isabelle/HOL formalization this kind of inductive deﬁnition works quite seamlessly due to Isabelle basing its

datatype construct on bounded natural functors, which can readily express syntax trees with inﬁnite branching [23]. The

caveat in Isabelle is that we have to put in more effort to establish that deﬁnitions like the one of |= too are inductive

by relating them to a well-founded order34. For simpler types, Isabelle derives such “termination” properties of function

deﬁnitions more automagically.

33 function HM_Logic_Inﬁnitary.lts_tau.satisﬁes.

34 lemma HM_Logic_Inﬁnitary.lts_tau.HML_wf_rel_is_wf.

B. Bisping and L. Montanari Information and Computation 300 (2024) 105191

In the Isabelle/HOL theory, we implicitly make cardinalities between transition system and index sets in formulas match

by assuming that indexes i ∈Iin conjunctions and states in the transition system use the same type.

HML, as we have deﬁned it, is not minimal. One could use fewer constructors for the propositional operators without

losing distinction power by, for instance, merging them into one inﬁnitary NOR ¬i∈Iϕi. Unfolding the negated disjunctions

into conjunctions of negations, this would read:

ϕ::= aϕ|i∈I¬ϕi.

We will take this part of HML as the starting point for our modal characterization of contrasimilarity. Even though we

syntactically are using conjunctions of negations, we will continue to call the operator NOR as this is the common name for

joint denial of logic statements.

6.2. How to weaken HML

The HML of Deﬁnition 15 cannot express observations following internal τ-steps. Obviously, what might happen after

internal behavior should make a difference when we compare processes. We cannot however straight-forwardly add a

τϕ-observation to our HML deﬁnition, as this would mean interpreting τas another visible action. Instead, the standard

approach is to add a fuzzier observation on the transitive closure of τ-steps, which traditionally is expressed by ε. So let

us extend Deﬁnition 15 by a εϕproduction (assuming ε/∈Act) and change the satisfaction relation to include:

•p |=  εϕif there exists a psuch that p =⇒ pand p|= ϕ.

For instance, εaϕdenotes that internal behavior might happen before we continue to observe aϕ(but it does not

denote observation of internal behavior).

We now adapt the mentioned constructor-minimal subset of HML by inserting places where internal behavior may occur,

marked by ε, at the beginning of both productions:

Deﬁnition 16 (HMLε). We deﬁne the weak formulas HMLε35 by the grammar:

ϕ::= εaϕ|εi∈I¬ϕi(with a= τ).

In HMLε, the observation of a possible action or of a NOR of observations may be delayed by internal behavior. Clearly, if

a transition system has no internal behavior, there is no difference in expressiveness between HML and HMLε.

Example 6. In Example 5, we observed Pand Qto be non-bisimilar. As there are no internal steps, they also are non-

contrasimilar. Despite the changed grammar, we can ﬁnd a ϕ∈HMLεthat distinguishes Qfrom P:

ϕ0:= ε

ϕi+1:= εaϕi

ϕ:= εaεi∈N¬ε{¬ϕi}.

6.3. How game and logic coincide

We will show that HMLεprecisely characterizes contrasimilarity. This is to say that there is an HMLε-formula distin-

guishing state pfrom qif and only if p Cq.

Example 7. A distinguishing formula for the non-contrasimilar systems of Example 2(true for Pcbut false for Pl) would be

ε

{¬εopεaEats}.

In our proof, we link HMLεto our game characterization for the contrasimulation preorder of Deﬁnition 12. We show

that a distinguishing formula can always be constructed from a winning attacker strategy, and that in turn the attacker is

guaranteed to win if a distinguishing formula exists.

Lemma 19 (Soundness of HMLε). If the attacker wins the contrasimilarity game from (p0,Q0)a∈Wa, then there is a formula ϕ∈

HMLεthat distinguishes p0from Q0.36

35 inductive_set HM_Logic_Inﬁnitary.lts_tau.HML_weak_formulas.

36 lemma Weak_HML_Contrasimulation.c_game_with_attacker_strategy.distinction_soundness.

B. Bisping and L. Montanari Information and Computation 300 (2024) 105191

Proof. Let fbe a positional attacker strategy, f:Ga→Gd, winning on the whole of the attacker winning region Wa. Then,

the function atk_form :(Wa∩Ga) →HMLε37 is deﬁned recursively as:

atk_form((p,Q)a):= εaatk_form((p,Q)a)if f((p,Q)a)=Sim(a,p,Q)dand Qa

== Q,

εq∈Q¬atk_form((q,{p})a)if f((p,Q)a)=Swap(p,Q)dand Q=⇒ Q.

As recursive invocations are referring to attacker positions that also must be in the attacker’s winning region, the func-

tion must be well-deﬁned. In particular, the positional attacker strategy being winning guarantees well-foundedness of the

recursion.38

By the assumption, the attacker wins from (p0,Q0)awith f. Then there is an (acyclic) subgraph f⊆of the

game sticking to attacker moves according to fwith branching at defender decisions. More formally, for the reachable

part, gfgif g=f(g)for g∈Gaand if ggfor g∈Gd. Because fis winning, all positions in the graph must be

attacker-won, and there must be a well-founded relation ≺on the graph such that gfgimplies g≺g.

We prove by well-founded induction that, at attacker positions, atk_form((p,Q)a)distinguishes pfrom Qin the

sense that it is true for pand false for each q ∈Q. So let us assume as induction hypothesis that for all attacker

positions (p∗,Q∗)a≺(p,Q)a, atk_form((p∗,Q∗)a)distinguishes p∗from Q∗. We proceed by examining the cases of

atk_form((p,Q)a)due to its deﬁnition (and the deﬁnition of ):

•Case atk_form((p,Q)a) =εaatk_form((p,Q)a)with (p,Q)afSim(a,p,Q)d, p a

== p, and Qa

== Q. We

know that Sim(a,p,Q)df(p,Q)a. Due to transitivity, (p,Q)a≺(p,Q)a. With the induction hypothesis,

atk_form((p,Q)a)must be true for pand false for each q∈Q. As p a

== pand Qa

== Q, the semantics of HML

thus yields that εaatk_form((p,Q)a)must distinguish pfrom Q.

•Case atk_form((p,Q)a) =εq∈Q¬atk_form((q,{p})a)with (p,Q)afSwap(p,Q)d, p =⇒ p, and Q=⇒ Q. For each

q∈Q, there is Swap(p,Q)df(q,{p})a. Consequently, (q,{p})a≺(p,Q)afor each q∈Q. With the induction

hypothesis, each atk_form((q,{p})a)is true for qand false for p. Due to the HML semantics, each ¬atk_form((q,{p})a)

is false for qand true for p. Likewise, q∈Q¬atk_form((q,{p})a)must distinguish pfrom Q. As p =⇒ pand Q=⇒ Q,

εq∈Q¬atk_form((q,{p})a)thus distinguishes pfrom Q.

As (p0,Q0)amust be part of the game subgraph, this proves atk_form((p0,Q0)a)to distinguish p0from Q0. Clearly,

atk_form((p0,Q0)a) ∈HMLεby its deﬁnition. 

Lemma 20 (Completeness of HMLε). If ϕ∈HMLεdistinguishes pfrom Q, then the attacker wins from (p,Q)a.39

Proof. For the base case, let us assume that ϕ=εi∈∅¬ϕi. We have p =⇒ pand, by assumption, p |= ϕ. Since q |= ϕ

for any q ∈Qand since ϕmust be distinguishing, we can conclude that Qmust be empty. Moving to Swap(p,Q)dwill

therefore get the defender stuck.

For the two inductive steps, we investigate all possible attacker positions (p,Q)awhere some ϕdistinguishes pfrom Q.

•Case I: ϕ=εaϕ. We assume the attacker wins from all positions (p,Q)awhere ϕdistinguishes pfrom Q. Then

there exists a pwith p a

== pand p|= ϕ. The attacker may choose one such pand move to Sim(a,p,Q)d, whereupon

the defender must move to (p,dsuccs(a,Q))a. As q |= ϕfor all q ∈Q, either no a

== -step is possible from Qor no

q∈dsuccs(a, Q)satisﬁes ϕ. In both cases, ϕdistinguishes pfrom dsuccs(a, Q)and the attacker wins by the induction

hypothesis.

•Case II: ϕ=εi∈I¬ϕi. We assume the attacker wins from any position (p,Q)awhere some formula ϕi∈HMLεwith

i ∈Idistinguishes pfrom Q. Then there must be some i ∈Isuch that q |= ε¬ϕifor all q ∈Q. It follows that q|= ¬ϕi

and therefore q|= ϕifor all qwith Q=⇒ q. Conversely, from p |= ϕwe can deduce p |=  ε¬ϕi; hence, there must exist

a psuch that p =⇒ pand p|= ϕi. The attacker may therefore choose one such pand move to Swap(p,Q)d. If Q

is empty, the attacker wins immediately by getting the defender stuck. Otherwise, the defender must choose a qwith

Q=⇒ qand move to (q,{p})a. Since ϕidistinguishes qfrom {p}, the attacker wins by the induction hypothesis. 

We can slightly weaken and combine Lemmas 19 and 20 to get:

Corollary 21. A formula ϕ∈HMLεdistinguishes pfrom qif and only if the attacker wins from (p,{q})a.

With Theorem 17 this immediately implies:

37 function Weak_HML_Contrasimulation.c_game_with_attacker_strategy.attack_formula.

38 The depth of strategies and formulas might reach ordinals if the transition system contains nondeterminism with inﬁnite branching as in Example 5.

This is no problem for our construction, which only relies on the well-foundedness.

39 lemma Weak_HML_Contrasimulation.c_game_with_attacker_formula.distinction_completeness.

B. Bisping and L. Montanari Information and Computation 300 (2024) 105191

5. weak bisimulation

ε{ϕ,¬ϕ,...}

4. coupled simulation

ε{¬ϕ,¬ϕ,...}|ε{ϕ,ϕ,...}

2. weak simulation

ε{ϕ,ϕ,...}

3. contrasimulation

ε{¬ϕ,¬ϕ,...}

1. weak traces

ε∅

Fig. 8. Lattice of weak conjunctions.

Theorem 22 (Hennessy–Milner theorem for HMLε). There exists a formula ϕ∈HMLεdistinguishing pfrom qif and only if p Cq.

7. Relation to other modal characterizations and weak bisimilarities

We can use the lense of modal logic to reveal the systematic connections between contrasimilarity and other notions

of equivalence. This section uses this lense to discuss related work and equivalences such as coupled simulation, stable

bisimulation, and impossible futures.

7.1. Relationship to weak (bi-)simulation and coupled simulation preorder

Let us brieﬂy explicate how modal distinctions shape the hierarchy of Fig. 2around contrasimilarity. At the core, the fol-

lowing recalls van Glabbeek’s spectrum [2], which contains modal characterizations for a wide range of behavioral preorders

and equivalences with silent steps, including weak bisimulation, weak simulation, coupled simulation and contrasimulation.

All weak equivalences allow for delayed observations, that is, if ϕis a formula of their observation language, then εaϕ

is, too (for a ∈Act). The languages differ in what kinds of conjunctions they allow. Fig. 8lays out the possible conjunctions

in the observation languages of the named notions. Each is preﬁxed by possible internal behavior ε.

1. Weak trace observations may only contain empty conjunctions, .

2. Weak simulation observations allow conjunctions of positive formulas.

3. Contrasimulation observations, as we have characterized them in HMLε, allow conjunctions of negative formulas, that is,

NORs.

4. Coupled simulation observations may exhibit positive conjunctions and NORs, but not mix positive and negative conjuncts

in the same conjunction.

5. Weak bisimulation generalizes this by allowing to mix positive and negative conjuncts.40

With these characterizations, it is clear why distinction at the bottom of Fig. 8implies distinction at the top, and dually,

why equivalence at the top implies equivalence at the bottom.

7.2. Comparison to Voorhoeve and Mauw’s nested impossible futures

Voorhoeve and Mauw [6]introduce the notion of impossible futures preorder and equivalence. They show that con-

trasimulation preorder is obtained as the limit of arbitrarily nesting impossible futures. This is roughly the same as our

characterization of contrasimilarity in terms of weak NORs, although there are some notational differences. So, this subsec-

tion is meant to explicate the connection.

Impossible futures offer a semantics that naturally generalizes failures (the common denotations in failure equivalence)

from impossible actions to impossible traces.

40 This characterization of weak bisimulation preorder / equivalence is slightly non-standard. More on why it works can be found in [20].

B. Bisping and L. Montanari Information and Computation 300 (2024) 105191

Deﬁnition 17 (Impossible futures equivalence). For a state p, its impossible futures are given by the set

IF(p):= {(

w,

X)|∃p.p

#‰

=⇒ p∧∀



x∈

X.p

#‰

=⇒}.

Two states pand qare impossible-futures preordered if IF(p) ⊆IF(q)and impossible-futures equivalent if IF(p) =IF(q).

Voorhoeve and Mauw [6]give a modal logic to characterize impossible futures and other equivalences. It consists of ,

conjunction ϕ∧ψ, negation ¬ϕand a special, path-restricted possibility modality on path sets Wϕwith W⊆Act∗, which

is true at piff there are 

w∈Wand pwith p

#‰

=⇒ psuch that ϕis true at p. As usual, other operators are derived as

aliases: ⊥ =¬, disjunction ϕ∨ψ=¬(¬ϕ∧¬ψ), and necessity Wϕ=¬W¬ϕ, also considering ¬¬ϕ=ϕ. They then go

on to deﬁne stratiﬁed sublogics C+

nwhere , ⊥ ∈C+

0, and where ϕ, ψ∈C+

nimplies ϕ∧ψ, ϕ∨ψ∈C+

n, and W¬ϕ∈C+

n+1.

For instance, a distinguishing formula between Pland Pcof Example 2would be {ε}{(op,aEats)}, meaning “wherever

we move by internal behavior, op.aEats must be possible.” It equals {ε}¬{(op,aEats)}¬ ∈C+

2. According to the deﬁni-

tions of [6], this formula disproves impossible-futures preordering from Pcto Pl(notice the reversed order!) and thus also

contrasimilarity. There is a swap of direction between the modal distinctions and the preorders [cf. 6, Theorem 1]. But

n≥0C+

n+1∪{¬ϕ|ϕ∈C+

n}in the end characterizes contrasimilarity.

It is not necessary to construct C+in a way that leads to the complication of switching directions of [6]. Choos-

ing W¬ϕ∈C+

n+1as the modality in the recursive case alleviates the issue. For Pc/Pl, one could then take the dual

{ε}¬{(op,aEats)}¬⊥ as distinction—which is equivalent to the HMLε-formula of Example 7, ε

{¬εopεaEats}.

A nice thing about the path-restricted modalities of [6]is that they make visible how contrasimilarity’s modal logic

alternates and modalities. The syntax-sugared version of the previous example formula reads: {ε}{(op,aEats)}⊥.

Our characterization through HMLε(Deﬁnition 16) has the advantage of being a subset of a more standard silent-step

Hennessy–Milner logic than the ones with special modalities of [2] and [6]. Also, it is more concise by featuring just two

constructors for formulas.

Impossible futures preorder arises naturally if we allow only one non-empty weak NOR per formula in the modal charac-

terization. Voorhoeve and Mauw [6] choose the name “impossible futures” in reference to the pre-existing “possible futures”

equivalence / preorder. In the modal characterization, a (weak) possible future observation has at most one non-empty weak

conjunction ε{ϕ1, ¬ϕ2, ...}, that is, a trace leading to a conjunction of the kind at the top of Fig. 8, where all subformu-

las state the possibility or impossibility of traces from that point. By this account, weak bisimilarity is obtained as the limit

of arbitrarily nesting possible futures and contrasimilarity through arbitrarily nesting im-possible futures.

Remark 4 (No easier nestings). Arbitrary nesting can reduce complexity of the characterized equivalence problem: While

deciding weak possible futures and nestings of possible futures equivalence falls within PSPACE, deciding its arbitrarily

nested limit, weak bisimilarity, lies in PTIME. It therefore would have been conceivable that, analogously, the arbitrarily

nested limit of impossible futures, contrasimilarity, might be less complex than impossible futures. Through Corollary 9, we

have ruled out this possibility. Contrasimilarity and impossible futures equivalence both are equally PSPACE-hard.

7.3. A weak contender: stable bisimulation

At the beginning of the article, we presented contrasimilarity to be the weakest form of bisimilarity. A close look into

the linear-time–branching-time spectrum with silent steps [2]reveals some variants of stable bisimilarity to be incomparable

to contrasimilarity. They too coincide with strong bisimilarity on systems without τ-steps. Thus they could be considered

as alternative “weakest bisimilarities.”

Stable bisimilarity is characterized by requiring non-empty conjunctions to refer to situations where no τis possible:

ε{¬τ, ϕ1, ¬ϕ2, ...}. Intuitively, this leads to a “bisimulation on ways to reach stable states,” which is a natural idea

to mediate between the worlds of weak bisimulation and of stable failures / revivals in CSP-like semantics. In particular, if

there are no τ-steps and thus no instable states, this notion coincides with strong bisimilarity. However, there are several

subtleties, especially when systems contain divergences, that is, inﬁnite τ-step sequences p τ

−→ω. To our knowledge, only

two publications aside from van Glabbeek [2]even mention stable bisimulation: Parrow and Sjödin [15]in the conclusion,

and Sangiorgi [24]in an exercise. In both cases, the characterization of stable bisimulation relations is ﬂawed in the sense

that the characterized bisimilarity neither is transitive nor does it imply weak trace equivalence in the face of divergences.

One can extract another, more general deﬁnition of stable bisimulation from [2]:

Deﬁnition 18 (Stable bisimilarity). A relation Ris a stable bisimulation if, for all (p, q) ∈Rwith #‰

w∈Act∗and p

#‰

=⇒ p, there

is a qwith q

#‰

=⇒ q, and in case pτ

−→, moreover qτ

−→ and (p, q) ∈R ∩R−1. Two states p0and q0are stably bisimilar if

there is a stable bisimulation Rwith (p0, q0) ∈R ∩R−1.

Example 8. On the processes of Example 1, {(p, p) |p ∈S} ∪{(Pc, Pp), (Pp, Pc)}is a stable bisimulation, which proves Pc

and Ppto also be stably bisimilar.

B. Bisping and L. Montanari Information and Computation 300 (2024) 105191

stability-respecting contrasimulation

ε{¬ϕ,¬ϕ,...}|ε{¬τ,¬ϕ,¬ϕ,...}

stable contrasimulation

(aka. stable bisimulation)

ε∅|ε{¬τ,¬ϕ,¬ϕ,...}

contrasimulation

ε{¬ϕ,¬ϕ,...}

Fig. 9. Hierarchy of stable / stability-respecting weak NORs.

Pcis not stably bisimilar to Plof Example 2, because Pccan reach a stable state where the choice has been re-

solved by internal behavior and Plcan not; they are distinguished by the stable impossible future formula ε

{¬τ,

¬εopεaEats}.

Like contrasimilarity, stable bisimilarity by this deﬁnition is an equivalence relation that coincides with strong bisimilarity

if there are no τ

−→-steps in the transition system. It differs from contrasimilarity in that, if a transition system has no stable

states, stable bisimilarity degenerates to trace equivalence, while contrasimilarity is oblivious to added divergence.

As with contrasimulation, the deﬁnition of stable bisimulation is in terms of transition sequences

#‰

=⇒. The complexity of

traces cannot be removed from the concept of stable bisimilarity. This is because the same reduction argument that works

for contrasimilarity in Section 3also works for stable bisimilarity:

Lemma 23 (Hardness of stable bisimilarity). Deciding stable bisimilarity is as hard as deciding weak trace equivalence, i.e. PSPACE-

hard.

Proof. One can use the construction of Section 3to reduce trace equivalence on Sto stable bisimilarity on S⊥. To see why,

consider again the relevant subrelation Rof the trace inclusion preorder T⊥. It must be a stable bisimulation on S⊥. The

reason is that S⊥of Deﬁnition 7has no stable states. This deactivates the second case of Deﬁnition 18, only leaving the

ﬁrst case, which expresses trace inclusion. Together with Lemma 6and using the arguments of Theorem 8, we again arrive

at PSPACE-hardness. 

This comparison reveals that stable bisimilarity shares the “downsides” of contrasimilarity (complexity, transition se-

quences), but moreover also loses all observability of liveness on instable states. This is why the concluding remarks of van

Glabbeek [2]single out contrasimilarity and coupled similarity as the most appropriate coarse notions for most branching-

time contexts, disregarding stable bisimilarity.

Contrasimilarity also is more versatile in another sense: It can be extended to account for stability. One can combine

the observability of stability into the weak NORs ε{¬τ, ¬ϕ1, ¬ϕ2, ...}. Allowing stable weak NORs leads to stability-

respecting contrasimilarity, which reﬁnes both contrasimilarity and stable bisimilarity. If we were to prescribe all non-empty

weak NORs to be stable, we would arrive at the same expressiveness as with stable bisimulation observations because we

can rephrase positive conjuncts in stable conjunctions as negative by “stable double negations”41:

p|=  ε{¬τ,ϕ1,¬ϕ2,...}⇐⇒p|=  ε{¬τ,¬ε{¬τ,¬ϕ1},¬ϕ2,...}

In this view, stable bisimilarity can be considered to just be a more intuitive alias for what we could systematically call

stable contrasimilarity. Fig. 9summarizes how stability and weak NORs can be combined to obtain different kinds of con-

trasimulation observations. Thus, (ordinary instable) contrasimulation and stable contrasimulation, aka. stable bisimulation,

are incomparable in expressiveness, but both are weakest abstractions of bisimulation. The title of contrasimilarity as “the

weakest bisimilarity” in Section 2is justiﬁed—there just are incomparable ways of mixing it with stability requirements,

and one of them is called “stable bisimilarity.”

8. Conclusion

The presented game closes the last interesting gap in the landscape of game characterizations for equivalences in the linear-

time–branching-time spectrum with internal steps [2]. The ﬁner variants of weak bisimilarities have been explored by De Frutos

Escrig et al.’s for branching, delay, ηand weak bisimulation [7] and Bisping for coupled simulation [16]. The present work

41 This expressiveness collapse is no new result, but already present in Proposition 3 of the unpublished fuller version of [2].

B. Bisping and L. Montanari Information and Computation 300 (2024) 105191

opens the way for Bisping and Jansen’s spectroscopy game [20]to provide one general equivalence (energy) game for the

whole spectrum with silent steps.

We have established PSPACE-hardness of contrasimilarity checking using a polynomial-time reduction from trace inclusion

to contrasimulation preorder. Combined with the exponential game characterization, this paper therefore shows PSPACE-

completeness of contrasimilarity checking. This is a non-trivial result, as other equivalences obtained through arbitrary

nestings of conjunctions are less complex (cf. Remark 4).

We have integrated the contrasimilarity algorithm into our prototypical coupled similarity checker on https://coupledsim .

bbisping .de. So, a side effect of the work presented here is to provide the ﬁrst tool support for checking contrasimilarity.

This article adds a modal-logical characterization of contrasimilarity in terms of only two delayed constructors, strongly

linked to the game and employing a more conventional HML for Voorhoeve and Mauw’s concept of arbitrarily nested

statements about impossible futures [6]. As in [10], the virtue of the single-action game construction lies in making attacker

strategies correspond closely with all relevant distinguishing Hennessy–Milner logic formulas. Observation aϕand logical

NOR ¬(ϕ1∨ϕ2∨...) form a functionally complete set of operators for HML and thus characterize (strong) bisimilarity. It

is satisfying that “weakening” this observation language by internal behavior in front of both productions leads precisely to

contrasimilarity. This provides further evidence that contrasimilarity is a natural way of generalizing bisimilarity to systems

with internal steps. We have also explicated how contrasimilarity subsumes stable bisimilarity.

We develop a formalization of contrasimilarity and its characterizing games and logics in Isabelle42 based on our prior

work in [25]. Before this, Peters and van Glabbeek [26,27] provided an Isabelle theory of contrasimilarity tailored to reduc-

tion semantics and to the analysis of encodings between formalisms. Moreover, Bell [3]developed a Coq formalization to

support the veriﬁcation of compilers using contrasimilarity, still available at http://people .csail .mit .edu /cj /par/.

Contrasimilarity is an only slightly coarser sibling of coupled similarity [15]. For coupled similarity, Bisping and Nest-

mann [8]use

the same reduction as in Section 3to show that it cannot be cheaper than deciding weak similarity. There,

however, a cubic-time algorithm can be given. The closeness of contrasimilarity and coupled similarity might reduce the

exponential complexity of deciding contrasimilarity in some cases. For models trying to avoid the exponentiality, it might

suﬃce to ensure that all observations are committed, which would rule out Example 3and the reduction of Section 3.

Fournet and Gonthier [28]showed that parts of the hierarchy of equivalences around contrasimilarity collapse for reduction

semantics if transient barbs are excluded. Then, however, cheaper algorithms for easier predicates such as coupled simula-

tion should also be applicable right away. More research would be needed in order to pinpoint where exactly one cannot

do without arbitrary-length word contrasimulation.

CRediT authorship contribution statement

Benjamin Bisping: Writing – review & editing, Writing – original draft, Visualization, Validation, Supervision, Software,

Project administration, Methodology, Investigation, Formal analysis, Conceptualization. Luisa Montanari: Writing – review &

editing, Writing – original draft, Visualization, Validation, Investigation, Formal analysis, Conceptualization.

Declaration of competing interest

The authors declare that they have no known competing ﬁnancial interests or personal relationships that could have

appeared to inﬂuence the work reported in this paper.

Acknowledgments

We are thankful to Uwe Nestmann, Rob van Glabbeek, Max Pohlmann, and the EXPRESS/SOS reviewers.

References

[1] B. Bisping, L. Montanari, A game characterization for contrasimilarity, in: O. Dardha, V. Castiglioni (Eds.), Proceedings Combined 28th International

Workshop on Expressiveness in Concurrency and 18th Workshop on Structural Operational Semantics, in: Electronic Proceedings in Theoretical Com-

puter Science, vol. 339, Open Publishing Association, 2021, pp. 27–42.

[2] R.J. van Glabbeek, The linear time–branching time spectrum II, in: International Conference on Concurrency Theory, Springer, 1993, pp. 66–81.

[3] C.J. Bell, Certiﬁably sound parallelizing transformations, in: G. Gonthier, M. Norrish (Eds.), Certiﬁed Programs and Proofs, vol. 8307, Springer Interna-

tional Publishing, 2013, pp. 227–242.

[4] J.C.M. Baeten, P.J.L. Cuijpers, P.J.A. van Tilburg, A context-free process as a pushdown automaton, in: F. van Breugel, M. Chechik (Eds.), CONCUR 2008 -

Concurrency Theory, Springer Berlin Heidelberg, Berlin, Heidelberg, 2008, pp. 98–113.

[5] Z. de Hoop, Context-free processes and push-down processes, Master’s thesis, Universiteit van Amsterdam, 2017, https://eprints .illc .uva .nl /id /eprint /

1561.

[6] M. Voorhoeve, S. Mauw, Impossible futures and determinism, Inf. Process. Lett. 80 (1) (2001) 51–58, https://doi .org /10 .1016 /S0020 -0190(01 )00217 -4.

[7] D. de Frutos Escrig, J.J.A. Keiren, T.A.C. Willemse, Games for bisimulations and abstraction, Log. Methods Comput. Sci. 13 (4) (2017) 1–40, https://

doi .org /10 .23638 /LMCS -13(4 :15 )2017.

[8] B. Bisping, U. Nestmann, Computing coupled similarity, in: Proceedings of TACAS, in: LNCS, Springer, 2019, pp. 244–261.

42 Available from https://github .com /luisamontanari /ContrasimGame and the Archive of Formal Proofs [13].

B. Bisping and L. Montanari Information and Computation 300 (2024) 105191

[9] X. Chen, Y. Deng, Game characterizations of process equivalences, in: G. Ramalingam (Ed.), Programming Languages and Systems, vol. 5356, Springer

Berlin Heidelberg, 2008, pp. 107–121.

[10] B. Bisping, D.N. Jansen, U. Nestmann, Deciding all behavioral equivalences at once: a game for linear-time–branching-time spectroscopy, Log. Methods

Comput. Sci. 18 (3) (2022), https://doi .org /10 .46298 /lmcs -18(3 :19 )2022.

[11] R.J. van Glabbeek, The linear time–branching time spectrum I. The semantics of concrete, sequential processes, in: Handbook of Process Algebra,

Elsevier, 2001, pp. 3–99.

[12] M. Wenzel, et al., The Isabelle/Isar reference manual, https://isabelle .in .tum .de /doc /isar-ref .pdf, 2021.

[13] B. Bisping, L. Montanari, Coupled similarity and contrasimilarity, and how to compute them, Arch. Form. Proofs (2023), https://isa -afp .org /entries /

Coupledsim _Contrasim .html.

[14] R. Milner, Communication and Concurrency, PHI Series in Computer Science, Prentice Hall, Englewood Cliffs, 1989.

[15] J. Parrow, P. Sjödin, The complete axiomatization of cs-congruence, in: Annual Symposium on Theoretical Aspects of Computer Science, Springer, 1994,

pp. 555–568.

[16] B. Bisping, U. Nestmann, K. Peters, Coupled similarity: the ﬁrst 32 years, Acta Inform. 57 (3) (2020) 439–463, https://doi .org /10 .1007 /s00236 -019 -

00356 -4.

[17] P.C. Kanellakis, S.A. Smolka, CCS expressions, ﬁnite state processes, and three problems of equivalence, Inf. Comput. 86 (1) (1990) 43–68, https://

doi .org /10 .1016 /0890 -5401(90 )90025 -D.

[18] H. Hüttel, S. Shukla, On the complexity of deciding behavioural equivalences and preorders. A survey, Tech. Rep. BRICS RS-96-39H, University of Aarhus,

1996, https://dx .doi .org /10 .7146 /brics .v3i39 .20021.

[19] C. Stirling, Bisimulation, modal logic and model checking games, Log. J. IGPL 7(1) (1999) 103–124, https://doi .org /10 .1093 /jigpal /7.1.103.

[20] B. Bisping, D.N. Jansen, Linear-time–branching-time spectroscopy accounting for silent steps, arXiv preprint, arXiv:2305 .17671, 2023, https://doi .org /10 .

48550 /arXiv.2305 .17671.

[21] M. Hennessy, R. Milner, Algebraic laws for nondeterminism and concurrency, J. ACM 32 (1) (1985) 137–161, https://doi .org /10 .1145 /2455 .2460.

[22] M. Hennessy, R. Milner, On observing nondeterminism and concurrency, in: J.W. de Bakker, J. van Leeuwen (Eds.), Automata, Languages and Program-

ming, in: LNCS, vol. 85, Springer, Berlin, 1980, pp. 299–309.

[23] J.C. Blanchette, L. Gheri, A. Popescu, D. Traytel, Bindings as bounded natural functors, Proc. ACM Program. Lang. 3 (POPL) (jan 2019), https://doi .org /10 .

1145 /3290335.

[24] D. Sangiorgi, Introduction to Bisimulation and Coinduction, Cambridge University Press, New York, NY, USA, 2012.

[25] B. Bisping, Isabelle/HOL proof and apache ﬂink program for TACAS 2019 paper: computing coupled similarity, https://doi .org /10 .6084 /m9 .ﬁgshare .

7831382 .v1, 2019.

[26] K. Peters, R.J. van Glabbeek, Analysing and comparing encodability criteria, in: Proceedings of the Combined 22th International Workshop on Ex-

pressiveness in Concurrency and 12th Workshop on Structural Operational Semantics, and 12th Workshop on Structural Operational Semantics,

EXPRESS/SOS, 2015, pp. 46–60.

[27] K. Peters, R.J. van Glabbeek, Analysing and comparing encodability criteria for process calculi, Arch. Form. Proofs (2015), https://isa -afp .org /entries /

Encodability _Process _Calculi .html.

[28] C. Fournet, G. Gonthier, A hierarchy of equivalences for asynchronous calculi, J. Log. Algebraic Program. 63 (1) (2005) 131–173, https://doi .org /10 .1016 /

j .jlap .2004 .01.006.