Barbara König

Christina Mika-Michalski
email: christina.mika-michalski@uni-due.de

Lutz Schröder
email: lutz.schroeder@fau.de

Explaining Non-Bisimilarity in a Coalgebraic Approach: Games and Distinguishing Formulas

Keywords: coalgebra, bisimulation games, distinguishing formulas, generic partition refinement

Behavioural equivalences can be characterized via bisimulation, modal logics, and spoiler-duplicator games. In this paper we work in the general setting of coalgebra and focus on generic algorithms for computing the winning strategies of both players in a bisimulation game. The winning strategy of the spoiler (if it exists) is then transformed into a modal formula that distinguishes the given non-bisimilar states. The modalities required for the formula are also synthesized on-the-fly, and we present a recipe for re-coding the formula with different modalities, given by a separating set of predicate liftings. Both the game and the generation of the distinguishing formulas have been implemented in a tool called T-Beg.

Introduction

There are many contexts in which it is useful to check whether two system states are behaviourally equivalent respectively bisimilar. In this way one can compare a system with its specification, replace a subsystem by another one that is behaviourally equivalent or minimize a transition system. Here we will concentrate on methods for explaining that two given states in a transition system are not bisimilar. The idea is to provide a witness for non-bisimilarity. Such a witness can be used to explain (to the user) why an implementation does not conform to a specification and give further insights for adjusting it.

Two states are bisimilar if they are related by a bisimulation relation. But this definition does not provide us with an immediate witness for non-bisimilarity, since we would have to enumerate all relations including that particular pair of states and show that they are not bisimulations. Hence, we have to resort to other characterizations of bisimilarity: bisimulation games [START_REF] Stirling | Bisimulation, modal logic and model checking games[END_REF], also known as spoiler-duplicator games, and modal logic. In the former case a proof of the non-bisimilarity of two states is given by a winning strategy of the spoiler. In the latter case the Hennessy-Milner theorem [START_REF] Hennessy | Algebraic Laws for Nondeterminism and Concurrency[END_REF] guarantees for image-finite labelled transition systems that, given two non-bisimilar states x 0 , x 1 , there exists a modal formula ϕ such that one of the states satisfies ϕ and the other does not. The computation of such distinguishing formulas is explained in [START_REF] Cleaveland | On Automatically Explaining Bisimulation Inequivalence[END_REF].

While the results and techniques above have been introduced for labelled transition systems, we are here interested in the more general setting of coalgebras [START_REF] Rutten | Universal coalgebra: a theory of systems[END_REF], which encompass various types of transition systems. Here we concentrate on coalgebras living in Set, where an endofunctor F : Set → Set specifies the branching type of the coalgebra (non-deterministic, probabilistic, etc.).

Modal logics have been extensively studied for coalgebras and it has been shown that under certain restrictions, modal coalgebraic logic is expressive, i.e., it satisfies the Hennessy-Milner theorem [START_REF] Pattinson | Coalgebraic modal logic: soundness, completeness and decidability of local consequence[END_REF][START_REF] Schröder | Expressivity of coalgebraic modal logic: The limits and beyond[END_REF]. However, to our knowledge, no explicit construction of distinguishing formulas in the coalgebraic setting has yet been given.

Coalgebraic games have been studied to a lesser extent: we refer to Baltag [START_REF] Baltag | Truth-as-Simulation: Towards a Coalgebraic Perspective on Logic and Games[END_REF][START_REF] Baltag | A logic for coalgebraic simulation[END_REF], where the game is based on providing subsets of bisimulation relations (under the assumption that the functor F is weak pullback preserving) and a generalization of Baltag's game to other functors in [START_REF] Kupke | Terminal Sequence Induction via Games (international tbilisi symposium on language, logic and computation)[END_REF]. Furthermore there is our own contribution [START_REF] König | Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras[END_REF], on which this article is based, and [START_REF] Komorida | Codensity Games for Bisimilarity[END_REF], which considers codensity games from an abstract, fibrational perspective.

We combine both the game and the modal logic view on coalgebras and present the following contributions:

We describe how to compute the winning strategies of the players in the behavioural equivalence game.

We show how to construct a distinguishing formula based on the spoiler strategy. The modalities for the formula are not provided a priori, but are synthesized on-the-fly as so-called cone modalities while generating the formula.

Finally we show under which conditions one can re-code a formula with such modalities into a formula with different modalities, given by a separating set of predicate liftings.

Both the game and the generation of the distinguishing formulas have been implemented in a generic tool called T-Beg 3 , where the functor is provided as a parameter. In particular, using this tool, one can visualize coalgebras, play the game (against the computer), derive winning strategies and convert the winning strategy of the spoiler into a distinguishing formula. Since the development of the tool was our central aim, we have made design decisions in such a way that we obtain effective algorithms. This means that we have taken a handson approach and avoided constructions that potentially iterate over infinitely many elements (such as the set of all modalities, which might be infinite). The partition refinement algorithm presented in the paper distinguishes states that are not behaviourally equivalent by a single equivalence class compared to other techniques which iterate over the final chain [START_REF] König | A Generalized Partition Refinement Algorithm, Instantiated to Language Equivalence Checking for Weighted Automata[END_REF][START_REF] Dorsch | Efficient Coalgebraic Partition Refinement[END_REF]. Separation via a single equivalence class is a technique used within known algorithms for checking bisimilarity in labelled transition systems [START_REF] Kanellakis | CCS Expressions, Finite State Processes, and Three Problems of Equivalence[END_REF][START_REF] Paige | Three Partition Refinement Algorithms[END_REF]. This requires a certain assumption on the endofunctor specifying the branching type (dubbed separability by singletons). Note that [START_REF] Paige | Three Partition Refinement Algorithms[END_REF] has already been generalized to a coalgebraic setting in [START_REF] Dorsch | Efficient Coalgebraic Partition Refinement[END_REF], using the assumption of zippability. Here we compare these two assumptions.

After presenting the preliminaries (Section 2), including the game, we describe how to compute the winning strategies in Section 3. In Section 4 we show how to construct and re-code distinguishing formulas, followed by a presentation of the tool T-Beg in Section 5. Finally, we conclude in Section 6. The proofs can be found in the full version of the paper [START_REF] König | Explaining Non-Bisimilarity in a Coalgebraic Approach: Games and Distinguishing Formulas[END_REF].

Preliminaries

Equivalence relations and characteristic functions: Let R ⊆ X ×X be an equivalence relation, where the set of all equivalence relations on X is given by Eq(X). For x 0 ∈ X we denote the equivalence class of x 0 by [

x 0 ] R = {x 1 ∈ X | (x 0 , x 1 ) ∈ R}. By E(R) we denote the set of all equivalence classes of R. Given Y ⊆ X, we define the R-closure of Y as follows: [Y ] R = {x 1 ∈ X | ∃ x 0 ∈ Y (x 0 , x 1 ) ∈ R}.
For Y ⊆ X, we denote its predicate or characteristic function by χ Y : X → {0, 1}. Furthermore, given a characteristic function χ : X → {0, 1}, its corresponding set is denoted χ ⊆ X.

We will sometimes overload the notation and for instance write [p] R for the R-closure of a predicate p. Furthermore we will write p 0 ∩ p 1 for the intersection of two predicates.

Coalgebra: We restrict our setting to the category Set, in particular we assume an endofunctor F : Set → Set, intuitively describing the branching type of the transition system under consideration. A coalgebra [START_REF] Rutten | Universal coalgebra: a theory of systems[END_REF], describing a transition system of this branching type, is given by a function α : X → F X. Two states x 0 , x 1 ∈ X are behaviourally equivalent (x 0 ∼ x 1 ) if there exists a coalgebra homomorphism f from α to some coalgebra

β : Y → F Y (i.e., a function f : X → Y with β•f = F f •α) such that f (x 0 ) = f (x 1
). We assume that F preserves weak pullbacks, which means that behavioural equivalence and coalgebraic bisimilarity coincide, and we will use the two terms interchangeably.

Preorder lifting: Furthermore we need to lift preorders under a functor F . To this end, we use the lifting introduced in [START_REF] Balan | Finitary functors: From Set to Preord and Poset[END_REF] (essentially the standard Barr extension of F [START_REF] Barr | Relational algebras[END_REF][START_REF] Trnková | General theory of relational automata[END_REF]), which guarantees that the lifted relation is again a preorder provided that F preserves weak pullbacks: Let ≤ be a preorder on Y , i.e. ≤ ⊆ Y × Y . We define a preorder ≤ F on F Y by t 0 ≤ F t 1 iff there exists t ∈ F (≤) such that F π i (t) = t i for i ∈ {0, 1}, where π i : ≤ → Y are the usual projections. More concretely, we consider the order ≤ = {(0, 0), (0, 1), (1, 1)} over 2 = {0, 1} and its corresponding liftings ≤ F .

Note that applying the functor is monotone wrt. the lifted order:

Lemma 1 ( [START_REF] König | Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras[END_REF]). Let (Y, ≤) be an ordered set and let p 0 , p 1 : X → Y be functions. Then p 0 ≤ p 1 implies F p 0 ≤ F F p 1 , with both inequalities read pointwise.

Predicate liftings: In order to define the modal logic, we need the notion of predicate liftings (also called modalities). Formally, a predicate lifting for F is a natural transformation λ : Q ⇒ QF , where Q is the contravariant powerset functor. It transforms subsets P ⊆ X into subsets λ(P ) ⊆ F X.

We use the fact that predicate liftings are in one-to-one correspondence with functions of type λ : F 2 → 2 (which specify subsets of F 2 and will also be called evaluation maps) [START_REF] Schröder | Expressivity of coalgebraic modal logic: The limits and beyond[END_REF]. We view subsets P ⊆ X as predicates p = χ P and lift them via p → λ•F p. In order to obtain expressive logics, we also need the notion of a separating set of predicate liftings. Definition 2. A set Λ of evaluation maps for a functor F : Set → Set is separating if for all sets X and t 0 , t 1 ∈ F X with t 0 = t 1 , there exists λ ∈ Λ and p : X → 2 such that λ(F p(t 0 )) = λ(F p(t 1 )). This means that every t ∈ F X is uniquely determined by the set {(λ, p) | λ ∈ Λ, p : X → 2, λ(F p(t)) = 1}. Such a separating set of predicate liftings exists iff (F p : F X → F 2) p : X→2 is jointly injective.

Here we concentrate on unary predicate liftings: If one generalizes to polyadic predicate liftings, a separating set of predicate liftings can be found for every accessible functor [START_REF] Schröder | Expressivity of coalgebraic modal logic: The limits and beyond[END_REF].

Separating sets of monotone predicate liftings and the lifted order on F 2 are related as follows: Proposition 3 ( [START_REF] König | Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras[END_REF]). An evaluation map λ : F 2 → 2 corresponds to a monotone predicate lifting (p :

X → 2) → (λ • F p : F X → 2) iff λ : (F 2, ≤ F ) → (2, ≤) is monotone.
Proposition 4 ( [START_REF] König | Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras[END_REF]). F has a separating set of monotone predicate liftings iff ≤ F ⊆ F 2 × F 2 is anti-symmetric and (F p : F X → F 2) p : X→2 is jointly injective.

Coalgebraic modal logics: Given a cardinal κ and a set Λ of evaluation maps λ : F 2 → 2, we define a coalgebraic modal language L κ (Λ) via the grammar

ϕ ::= Φ | ¬ϕ | [λ]ϕ where Φ ⊆ L κ (Λ) with card (Φ) < κ and λ ∈ Λ.
The last case describes the prefixing of a formula ϕ with a modality [λ]. Given a coalgebra α : X → F X and a formula ϕ, the semantics of such a formula is given by a map ϕ α : X → 2, where conjunction and negation are interpreted as usual and

[λ]ϕ α = λ • F ϕ α • α.
For simplicity we will often write ϕ instead of ϕ α . Furthermore for x ∈ X, we write x |= ϕ whenever ϕ (x) = 1. As usual, whenever ϕ α = ψ α for all coalgebras α we write ϕ ≡ ψ. We will use derived operators such as tt (empty conjunction), ff (¬tt) and (disjunction). The logic is always adequate, i.e., two behaviourally equivalent states satisfy the same formulas. Furthermore whenever F is κ-accessible and the set Λ of predicate liftings is separating, it can be shown that the logic is also expressive, i.e., two states that satisfy the same formulas are behaviourally equivalent [START_REF] Pattinson | Expressive logics for coalgebras via terminal sequence induction[END_REF][START_REF] Schröder | Expressivity of coalgebraic modal logic: The limits and beyond[END_REF].

Bisimulation game: We will present the game rules first introduced in [START_REF] König | Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras[END_REF]. At the beginning of a game, two states x 0 , x 1 are given. The aim of the spoiler (S) is to prove that x 0 x 1 , the duplicator (D) attempts to show x 0 ∼ x 1 .

-Initial configuration: A coalgebra α : X → F X and a position given as pair (x 0 , x 1 ) ∈ X × X. From a position (x 0 , x 1 ), the game play proceeds as follows: -Step 1: S chooses j ∈ {0, 1}, (i.e. x 0 or x 1 ) , and a predicate p j : X → 2.

-Step 2: D must respond for x 1-j with a predicate p 1-j satisfying

F p j (α(x j )) ≤ F F p 1-j (α(x 1-j )).
-Step 3: S chooses ∈ {0, 1} (i.e. p 0 or p 1 ) and an x ∈ X with p (x ) = 1.

-Step 4: D must respond with an x 1-∈ X such that p 1-(x 1-) = 1.

After one round the game continues in Step 1 with the pair (x 0 , x 1 ). D wins if the game continues forever or if S has no move at Step 3. In all other cases, i.e. D has no move at Step 2 or Step 4, S wins.

This game generalizes a bisimulation game for probabilistic transition systems from [START_REF] Desharnais | Approximate analysis of probabilistic processes: Logic, simulation and games[END_REF]. Note that -different from the presentation in [START_REF] Desharnais | Approximate analysis of probabilistic processes: Logic, simulation and games[END_REF] -we could also restrict the game in such a way that S has to choose index = 1 -j in Step 3. We now give an example that illustrates the differences between our generic game and the classical bisimulation game for labelled transition systems [START_REF] Stirling | Bisimulation, modal logic and model checking games[END_REF].

Example 5. Consider the transition system in Figure 1, which depicts a coalgebra α : X → F X, where F = P f (A × (-)) specifies finitely branching labelled transition systems. Clearly x 0 x 1 . Fig. 1: Spoiler has a winning strategy at (x 0 , x 1 ).

First consider the classical game where one possible winning strategy of the spoiler is as follows: he moves x 0 = 1 a → 4, which must be answered by the duplicator via x 1 = 2 a → 5. Now the spoiler switches and makes a move 5 a → 8, which can not be answered by the duplicator.

In our case a corresponding game proceeds as follows: the spoiler chooses j = 0 and p 0 = χ {4} . Now the duplicator takes x 1 and can for instance answer with p 1 = χ {5} , which leads to

F p 0 (α(x 0 )) = {(a, 0), (a, 1)} ≤ F {(a, 1)} = F p 1 (α(x 1 ))
(Compare this with the visualization of the order ≤ F on F 2 in Figure 2.) Regardless of how S and D choose states, the next game configuration is [START_REF] Barr | Relational algebras[END_REF][START_REF] Chatzikokolakis | Generalized Bisimulation Metrics[END_REF]. Now the spoiler is not forced to switch, but can choose j = 0 (i.e. 4) and can play basically any predicate p 0 , which leads to either F p 0 (α(4)) = {(b, 1)} or F p 0 (α(4)) = {(b, 0)}. D has no answering move, since F p 1 (α(5)) will always contain tuples with a and b, which are not in ≤ F -relation with the move of S (see also Figure 2, which depicts F 2 and its order).

The game characterizes bisimulation for functors that are weak pullback preserving and for which the lifted order ≤ F is anti-symmetric. Then it holds that x 0 ∼ x 1 if and only if D has a winning strategy from the initial configuration (x 0 , x 1 ). As already shown in [START_REF] König | Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras[END_REF], in the case of two non-bisimilar states x 0 x 1 we can convert a modal formula ϕ distinguishing x 0 , x 1 , i.e., x 0 |= ϕ and x 1 |= ϕ, into a winning strategy for the spoiler. Furthermore we can extract the winning strategy for the duplicator from the bisimulation relation.

However, in [START_REF] König | Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras[END_REF] we did not yet show how to directly derive the winning strategy of both players or how to construct a distinguishing formula ϕ.

Computation of Winning Strategies

In the rest of the paper we will fix a coalgebra α : X → F X with finite X for a weak pullback preserving endofunctor F : Set → Set. Furthermore we assume that F has a separating set of monotone predicate liftings, which implies that ≤ F , the lifted order on 2, is anti-symmetric, hence a partial order.

We first present a simple but generic partition refinement algorithm to derive the winning strategy for the spoiler (S) and duplicator (D) for a given coalgebra α : X → F X. This is based on a fixpoint iteration that determines those pairs of states (x 0 , x 1 ) ∈ X × X for which D has a winning strategy, i.e. x 0 ∼ x 1 . In particular we consider the relation W α , which -as we will show -is the greatest fixpoint of the following monotone function F α : Eq(X) → Eq(X) on equivalence relations:

F α (R) = {(x 0 , x 1 ) ∈ R | ∀P ∈ E(R) : F χ P (α(x 0 )) = F χ P (α(x 1 ))} W α = {(x 0 , x 1 ) ∈ X × X |
there exists a winning strategy of D for (x 0 , x 1 )} Theorem 6 ( [START_REF] König | Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras[END_REF]). Assume that F preserves weak pullbacks and has a separating set of monotone evaluation maps. Then x 0 ∼ x 1 iff D has a winning strategy for the initial configuration (x 0 , x 1 ).

In the following, we will prove that the greatest fixpoint of F α (i.e. νF α ) coincides with W α and hence gives us bisimilarity. Note that F α splits classes with respect to only a single equivalence class P . This is different from other coalgebraic partition refinement algorithms where the current equivalence relation is represented by a surjection e with domain X and we separate x 0 , x 1 whenever F e(α(x 0 )) = F e(α(x 1 )), which intuitively means that we split with respect to all equivalence classes at once. Hence we will need to impose extra requirements on the functor, spelled out below, in order to obtain this result.

One direction of the proof deals with deriving a winning strategy for S for each pair (x 0 , x 1 ) / ∈ νF α . In order to explicitly extract such a winning strategy for S -which will also be important later when we construct the distinguishing formula -we will slightly adapt the algorithm based on fixpoint iteration. Before we come to this, we formally define and explain the strategies of D and S.

We start with the winning strategy of the duplicator in the case where the two given states are bisimilar. This strategy has already been presented in [START_REF] König | Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras[END_REF], but we describe it here again explicitly. The duplicator only has to know a suitable coalgebra homomorphism.

Proposition 7 (Strategy of the duplicator, [START_REF] König | Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras[END_REF]). Let α : X → F X be a coalgebra. Assume that D, S play the game on an initial configuration (x 0 , x 1 ) with x 0 ∼ x 1 . This means that there exists a coalgebra homomorphism f :

X → Z from α to a coalgebra β : Z → F Z such that f (x 0 ) = f (x 1 ).
Assume that in Step 2 D answers with p 1-j = [p j ] ker (f ) , i.e., p 1-j is the ker (f )-closure4 of the predicate p j . (In other words:

p 1-j (s) = 1 iff there exists t ∈ X such that f (s) = f (t) and p j (t) = 1.)
Then the condition of Step 2 is satisfied and in Step 4 D is always able to pick a state

x 1-with p 1-(x 1-) = 1 and f (x ) = f (x 1-).
We argue why this strategy is actually winning: Since f is a coalgebra homomorphism we have

F f (α(x 0 )) = β(f (x 0 )) = β(f (x 1 )) = F f (α(x 1 )). By construc- tion, p 1-j factors through f , that is p 1-j = p j • f for some p j : Z → 2. This im- plies F p 1-j (α(x j )) = F p j (F f (α(x j ))) = F p j (F f (α(x 1-j ))) = F p 1-j (α(x 1-j )).
Since p j ≤ p 1-j it follows from monotonicity (Lemma 1) that F p j (α(x j )) ≤ F F p 1-j (α(x j )) = F p 1-j (α(x 1-j )). Hence p 1-j satisfies the conditions of Step 2. Furthermore if the spoiler picks a state x in p j in Step 3, the duplicator can pick the same state in p 1-j in Step 4. If instead the spoiler picks a state x in p 1-j , the duplicator can, due to the closure, at least pick a state x 1-in p j which satisfies f (x 1-) = f (x ), which means that the game can continue.

We now switch to the spoiler strategy that can be used to explain why the states are not bisimilar. A strategy for the spoiler is given by a pair of functions

I : X × X → N 0 ∪ {∞} and T : (X × X)\νF α → X × PX.
Here, I(x 0 , x 1 ) denotes the first index where x 0 , x 1 are separated in the fixpoint iteration of F α . The second component T tells the spoiler what to play in Step 1.

In particular whenever T (x 0 , x 1 ) = (x j , P ), S will play j (uniquely determined by x j unless x 0 = x 1 , in which case S does not win) and p j = χ P .

In the case I(x 0 , x 1 ) < ∞ such a winning strategy for S can be computed during fixpoint iteration, see Algorithm 1. Assume that the algorithm terminates after n steps and returns R n . It is easy to see that R n coincides with νF α : as usual for partition refinement, we start with the coarsest relation R 0 = X × X. Since ≤ F is, by assumption, anti-symmetric F χ P (α(x 0 )) ≤ F F χ P (α(x 1 )) and

F χ P (α(x 1 )) ≤ F F χ P (α(x 0 )) are equivalent to F χ P (α(x 0 )) = F χ P (α(x 1 )
) and the algorithm removes a pair (x 0 , x 1 ) from the relation iff this condition does not hold. In addition, T (x 0 , x 1 ) and I(x 0 , x 1 ) are updated, where we distinguish whether F p(α(x 0 ))

F F p(α(x 1 )) or F p(α(x 0 )) F F p(α(x 1 )) hold.
Every relation R i is finer than its predecessor R i-1 and, since F α preserves equivalences, each R i is an equivalence relation. Since we are assuming a finite set X of states, the algorithm will eventually terminate.

We will now show that Algorithm 1 indeed computes a winning strategy for the spoiler.

Algorithm 1 Computation of νF α and the winning strategy of the spoiler 1: procedure Compute greatest fixpoint of Fα and winning moves for S 2:

for all (x0, x1) ∈ X × X do 3:

I(x0, x1) ← ∞ 4: i ← 0, R0 ← X × X 5: repeat 6: i ← i + 1, Ri ← Ri-1 7:
for all (x0, x1) ∈ Ri-1 do 8:

for all P ∈ E(Ri-1) do 9: if F χP (α(x0)) F F χP (α(x1)) then 10: T (x0, x1) ← (x0, P ), I(x0, x1) ← i, Ri ← Ri \ {(x0, x1)} 11: else 12: if F χP (α(x1)) F F χP (α(x0)) then 13: T (x0, x1) ← (x1, P ), I(x0, x1) ← i, Ri ← Ri \ {(x0, x1)} 14:
until Ri-1 = Ri 15: return Ri, T, I Proposition 8. Assume that R n = νF α , T, I have been computed by Algorithm 1. Furthermore let (x 0 , x 1 ) / ∈ R n , which means that I(x 0 , x 1 ) < ∞ and T (x 0 , x 1 ) is defined. Then the following constitutes a winning strategy for the spoiler:

-Let T (x 0 , x 1 ) = (x j , P ). Then in Step 1 S plays j ∈ {0, 1} and the predicate p j = χ P . -Assume that in Step 2, D answers with a state x 1-j and a predicate p 1-j such that F p j (α(x j )) ≤ F F p 1-j (α(x 1-j )). -Then, in Step 3 there exists a state x 1-j ∈ X such that p 1-j (x 1-j ) = 1 and I(x j , x 1-j ) < I(x 0 , x 1 ) for all x j ∈ X with p j (x j ) = 1. S will hence select = 1 -j, i.e. p 1-j , and this state x 1-j . -In Step 4, D selects some x j with p j (x j ) = 1 and the game continues with (x 0 , x 1 ) where (x 0 , x 1 ) ∈ R n and I(x 0 , x 1 ) < I(x 0 , x 1 ).

Finally, we show that νF α coincides with W α and therefore also with behavioural equivalence ∼ (see [START_REF] König | Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras[END_REF]). For this purpose, we need one further requirement on the functor: Definition 9. Let F : Set → Set be an endofunctor on Set. Given a set X, F is separable by singletons on X if the following holds: for all t 0 = t 1 with t 0 , t 1 ∈ F X, there exists p : X → 2 where p(x) = 1 for exactly one x ∈ X (i.e., p is a singleton) and F p(t 0 ) = F p(t 1 ). Moreover, F is separable by singletons if F is separable by singletons on all sets X.

It is obvious that separability by singletons implies the existence of a separating set of predicate liftings, however the reverse implication does not hold as the following example shows.

Example 10. A functor that does not have this property, but does have a separating set of predicate liftings, is the monotone neighbourhood functor M with MX = {Y ∈ QQX | Y upwards-closed} (see e.g. [START_REF] Hansen | A coalgebraic perspective on monotone modal logic[END_REF]), where Q is the contravariant powerset functor. Consider X = {a, b, c, d} and t 0 , t 1 ∈ MX where t 0 = ↑ {{a, b}, {c, d}}, t 1 = ↑ {{a, b, c}, {a, b, d}, {c, d}}. That is, the only difference is that t 0 contains the two-element set {a, b} and t 1 does not. For any singleton predicate p, the image of Qp : P2 → PX does not contain a twoelement set, hence Mp(t 0 ) = Mp(t 1 ) -since t 1 and t 2 agree on subsets of X of cardinality different from 2 -and t 0 , t 1 cannot be distinguished. By contrast, both the finite powerset functor P f and the finitely supported probability distribution functor D (which are both ω-accessible and hence yield a logic with only finite formulas) are separable by singletons.

As announced, separability by singletons implies that the fixpoint νF α coincides with behavioural equivalence: Theorem 11. Let F be separable by singletons, and let α : X → F X be an Fcoalgebra. Then νF α = W α , i.e., νF α contains exactly the pairs (x 0 , x 1 ) ∈ X ×X for which the duplicator has a winning strategy.

Example 12. We revisit Example 5 and explain the execution of Algorithm 1.

In the first iteration we only have to consider one predicate χ X , and for all separated pairs of states (s, t) we set I(s, t) = 1 where the second component of T (s, t) is X. That is, the states are simply divided into equivalence classes according to their outgoing transitions. More concretely, we obtain the separation of {1, 2, 3} (with value {(a, 1)}) from {4} (with value {(b, 1)}), {5} (with value {(a, 1), (b, 1)} and {6, 7, 8, 9} (with value ∅). In the second iteration the predicate χ {4} is employed to separate {1} (with value {(a, 0), (a, 1)}) from {2} (with value {(a, 0)}) and we get I(1, 2) = 2 with T (1, 2) = (1, {4}), which also determines the strategy of the spoiler explained above. Similarly {3} can be separated from both {1} and {2} with the predicate χ {6,7,8,9} .

The notion of separability by singletons is needed because the partition refinement algorithm we are using separates two states based on a single equivalence class of their successors, whereas other partition refinement algorithms (e.g. [START_REF] König | A Generalized Partition Refinement Algorithm, Instantiated to Language Equivalence Checking for Weighted Automata[END_REF]) consider all equivalence classes. As shown in Example 10, this is indeed a restriction, however such additional assumptions seem necessary if we want to adapt efficient bisimulation checking algorithms such as the ones by Kanellakis/Smolka [START_REF] Kanellakis | CCS Expressions, Finite State Processes, and Three Problems of Equivalence[END_REF] or Paige/Tarjan [START_REF] Paige | Three Partition Refinement Algorithms[END_REF] to the coalgebraic setting. In fact, the Paige/Tarjan algorithm already has a coalgebraic version [START_REF] Dorsch | Efficient Coalgebraic Partition Refinement[END_REF] which operates under the assumption that the functor is zippable. Here we show that the related notion of m-zippability is very similar to separability by singletons. (The zippability of [START_REF] Dorsch | Efficient Coalgebraic Partition Refinement[END_REF] is in fact 2-zippability, which is strictly weaker than 3-zippability [START_REF] Wißmann | Personal communication 30[END_REF]30].) Definition 13 (zippability). A functor F is m-zippable if the map

F (A 1 + • • • + A m ) F (f1),...,F (fm) -----------→ F (A 1 + 1) × • • • × F (A m + 1)
is injective for all sets A 1 , . . . , A m , where

f i = id Ai + ! : A 1 + • • • + A m → A i + 1, with ! : A 1 +• • •+A i-1 +A i+1 +• • •+A m → 1,
is the function mapping all elements of A i to themselves and all other elements to • (assuming that 1 = {•}). Lemma 14. If a functor F is separable by singletons, then F is m-zippable for all m. Conversely, if F is m-zippable, then F is separable by singletons on all sets X with |X| ≤ m.

Runtime Analysis

We assume that X is finite and that the inequalities in Algorithm 1 (with respect to ≤ F ) are decidable in polynomial time. Then our algorithm terminates and has polynomial runtime.

In fact, if |X| = n, the algorithm runs through at most n iterations, since there can be at most n splits of equivalence classes. In each iteration we consider up to n 2 pairs of states, and in order to decide whether a pair can be separated, we have to consider up to n equivalence classes, which results in O(n 4 ) steps (not counting the steps required to decide the inequalities).

For a finite label set A, the inequalities are decidable in linear time for the functors in our examples (F = P f (A × (-)) and F = (D(-) + 1) A ). We expect that we can exploit optimizations based on [START_REF] Kanellakis | CCS Expressions, Finite State Processes, and Three Problems of Equivalence[END_REF][START_REF] Paige | Three Partition Refinement Algorithms[END_REF]. In particular one could incorporate the generalization of the Paige-Tarjan algorithm to the coalgebraic setting [START_REF] Dorsch | Efficient Coalgebraic Partition Refinement[END_REF].

Construction of Distinguishing Formulas

Next we illustrate how to derive a distinguishing modal formula from the winning strategy of S computed by Algorithm 1. The other direction (obtaining the winning strategy from a distinguishing formula) has been covered in [START_REF] König | Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras[END_REF].

Cone Modalities

We focus on an on-the-fly extraction of relevant modalities, to our knowledge a new contribution, and discuss the connection to other -given -sets of separating predicate liftings.

One way of enabling the construction of formulas is to specify the separating set of predicate liftings Λ in advance. But this set might be infinite and hard to represent. Instead here we generate the modalities while constructing the formula. We focus in particular on what we call cone modalities: given v ∈ F 2 we take the upward-closure of v as a modality.

We also explain how logical formulas with cone modalities can be translated into other separating sets of modalities.

Definition 15 (Cone modalities). Let v ∈ F 2. A cone modality [↑ v] is given by the following evaluation map

↑ v : F 2 → 2: ↑ v(u) = λ(u) = 1, if v ≤ F u 0, otherwise
Under our running assumptions, these evaluation maps yield a separating set of predicate liftings: Since F has a separating set of monotone predicate liftings, it suffices to show that the evaluation maps are jointly injective on F 2. Now if v 0 = v 1 for v 0 , v 1 ∈ F 2, then w.l.o.g. v 0 F v 1 , since we require that the lifted order is anti-symmetric. Hence, ↑ v 0 (v 0 ) = 1 and ↑ v 0 (v 1 ) = 0.

Example 16. We discuss modalities respectively evaluation maps in more detail for the functor F = P f (A×(-)) (see also Example 5). In our example, A = {a, b}. The set F 2 with order ≤ F is depicted as a Hasse diagram in Figure 2. For every element there is a cone modality, 16 modalities in total. It is known from the Hennessy-Milner theorem [START_REF] Hennessy | Algebraic Laws for Nondeterminism and Concurrency[END_REF] that two modalities are enough: either 2 a , 2 b (box modalities) or 3 a , 3 b (diamond modalities), where for v ∈ F 2,

2 a (v) = 1 if (a, 0) / ∈ v 0 otherwise 3 a (v) = 1 if (a, 1) ∈ v 0 otherwise.
In Figure 2, 2 a respectively 3 a are represented by the elements above the two lines (solid respectively dashed). Fig. 2: The set F 2 = P f ({a, b} × 2) with the order ≤ F (for labelled transition systems). The modality 2 a (3 a ) is given by the elements above the solid (dashed) line.

Example 17. As a second example we discuss the functor F = (D(-) + 1) A , specifying probabilistic transition systems. The singleton set 1 = {•} denotes termination. Again we set A = {a, b}. Since D2 is isomorphic to the interval [0, 1], we can simply represent any distribution d : 2 → [0, 1] by d(1). Hence F 2 ∼ = ([0, 1] + 1) A . The partial order is componentwise and is depicted in Figure 3: it decomposes into four disjoint partial orders, depending on which of a, b are mapped to •. The right-hand part of this partial order consists of function [0, 1] A with the pointwise order.

We will also abbreviate a map [a → p, b → q] by a p , b q .

[a → •, b → •] [a → 0, b → •] . . . [a → 1, b → •] [a → •, b → 0] . . . [a → •, b → 1] [a → 0, b → 0] . . . . . . . . . . . . [a → 1, b → 1]
Fig. 3: F 2 ∼ = ([0, 1] + 1) A with order ≤ F (for probabilistic transition systems).

From Winning Strategies to Distinguishing Formulas

We will now show how a winning strategy of S can be transformed into a distinguishing formula, based on cone modalities, including some examples. The basic idea behind the construction in Definition 18 is the following: Let (x 0 , x 1 ) be a pair of states separated in the i-th iteration of the partition refinement algorithm (Algorithm 1). This means that we have the following situation: F χ P (α(x 0 )) F F χ P (α(x 1 )) (or vice versa) for some equivalence class P of R i-1 . Based on v = F χ P (α(x 0 )) we define a cone modality λ = ↑ v. Now, if we can characterize P by some formula ψ, i.e., ψ = χ P (we will later show that this is always possible), we can define the formula ϕ = [λ]ψ. Then it holds that:

ϕ (x 0 ) = λ(F ψ (α(x 0 ))) = ↑ v(F χ P (α(x 0 ))) = 1 ϕ (x 1 ) = λ(F ψ (α(x 1 ))) = ↑ v(F χ P (α(x 1 ))) = 0
That is we have x 0 |= ϕ and x 1 |= ϕ, which means that we have constructed a distinguishing formula for x 0 , x 1 .

First, we describe how a winning strategy for the spoiler for a pair (x 0 , x 1 ) is converted into a formula and then prove that this formula distinguishes x 0 , x 1 . Definition 18. Let x 0

x 1 (equivalently (x 0 , x 1 ) / ∈ R n ), and let (T, I) be the winning strategy for the spoiler computed by Algorithm 1. We construct a formula ϕ x0,x1 as follows: assume that T (x 0 , x 1 ) = (s, P ) where s = x 0 . Then set v = F χ P (α(x 0 )), λ = ↑ v and ϕ x0,x1 = [λ]ϕ, where ϕ is constructed by recursion as follows:

-I(x 0 , x 1 ) = 1: ϕ = tt -I(x 0 , x 1 ) > 1: ϕ = x 0 ∈P x 1 ∈ X\P ϕ x 0 ,x 1 If s = x 1 , then we set v = F χ P (α(x 1 )) and ϕ x0,x1 = ¬[λ]ϕ instead.
The recursion terminates because I(x 0 , x 1 ) < I(x 0 , x 1 ) (since P is an equivalence class of R i-1 where i = I(x 0 , x 1 )).

Proposition 19. Let α : X → F X be a coalgebra and assume that we have computed R n , T, I with Algorithm 1. Then, given (x 0 , x 1 ) / ∈ R n , the construction in Definition 18 yields a formula ϕ x0,x1 ∈ L κ (Λ) such that x 0 ϕ x0,x1 and x 1 ϕ x0,x1 .

We next present an optimization of the construction in Definition 18, inspired by [START_REF] Cleaveland | On Automatically Explaining Bisimulation Inequivalence[END_REF]. In the case I(x 0 , x 1 ) > 1 one can pick an arbitrary x 0 ∈ P and keep only one element of the disjunction.

In order to show that this simplification is permissible, we need the following lemma.

Lemma 20. Given two states (x 0 , x 1 ) / ∈ R n and a distinguishing formula ϕ x0,x1 based on Definition 18. Let (x 0 , x 1 ) be given such that I(x 0 , x 1 ) > I(x 0 , x 1 ). Then x 0 ϕ x0,x1 if and only if x 1 ϕ x0,x1 . Now we can show that we can replace the formula ϕ from Definition 18 by a simpler formula ϕ .

Lemma 21. Let (x 0 , x 1 ) / ∈ R i and let P be an equivalence class of R i-1 . Furthermore let ϕ =

x 1 ∈ X\P ϕ x 0 ,x 1
for some x 0 ∈ P . Then ϕ = χ P .

Finally, we can simplify our construction described in Definition 18 to only one inner conjunction.

Corollary 22. We use the construction of ϕ x0,x1 as described in Definition 18 with the only modification that for I(x 0 , x 1 ) > 1 the formula ϕ is replaced by

ϕ = x 1 ∈ X\P ϕ x 0 ,x 1
for some x 0 ∈ P . Then this yields a formula ϕ x0,x1 such that x 0 ϕ x0,x1 and x 1 ϕ x0,x1 .

A further optimization takes only one representative x 1 from every equivalence class different from P . We now explore two slightly more complex examples.

Example 23. Take the coalgebra for the functor F = (D(-) + 1) A depicted in Figure 4, with A = {a, b} and set X = {1, . . . , 5} of states. For instance,

α(3) = [a → δ 3 , b → •]
where δ 3 is the Dirac distribution. This is visualized by drawing an arrow labelled a, 1 from 3 to 3 and omitting b-labelled arrows. We explain only selected steps of the construction: In the first step, the partition refinement algorithm (Algorithm 1) separates 1 from 3 (among other separations), where the spoiler strategy is given by T (1, 3) = (1, X). In order to obtain a distinguishing formula, we determine v = F χ X (α(1)) = a 1 , b 1 (using the abbreviations explained in Example 17) and obtain ϕ 1,3 = [↑ a 1 , b 1 ]tt. In fact, this formula also distinguishes 1 from 4, hence ϕ 1,3 = ϕ 1,4 . If, on the other hand, we want to distinguish 3, 4, we obtain

ϕ 3,4 = [↑ a 1 , b • ]tt.
After the first iteration, we obtain the partition {1, 2, 5}, {3}, {4}. Now we consider states 1, 2 which can be separated by playing T (2, 1) = (2, {1, 2, 5}), since 5 behaves differently from 3. Again we compute v = F χ P (α(2)) = a 1 , b 0.8 (for P = {1, 2, 5}) and obtain ϕ 2,1 = [↑ a 1 , b 0.8 ](ϕ 1,3 ∧ ϕ 1,4 ). Here we picked 1 as the representative of its equivalence class.

In summary we obtain

ϕ 2,1 = [↑ a 1 , b 0.8 ][↑ a 1 , b 1 ]
tt, which is satisfied by 2 but not by 1. Example 24. We will now give an example where conjunction is required to obtain the distinguishing formula. We work with the coalgebra for the functor F = P f (A × (-)) depicted in Figure 5, with A = {a, b, c, d, e, f } and set X = {1, . . . , 9} of states. We explain only selected steps: In the first step, the partition refinement separates 6 from 7 (among other separations), where the spoiler strategy is given by T (6, 7) = (6, X). As explained above, we determine v = F χ X (α(6)) = {(e, 1)} and obtain ϕ 6,7 = [↑ {(e, 1)}]tt. In fact, this formula also distinguishes 6 from all other states, so we denote it by ϕ 6, * .

Next, we consider the states 3, 4, where the possible moves of 3 are a proper subset of the moves of 4. Hence the spoiler strategy is T (3, 4) = (4, {6}), i.e., the spoiler has to move to state 6, which is not reachable from 3. Again we compute v = F χ P (α(4)) = {(b, 1), (b, 0)} (for P = {6}) and obtain ϕ 3,4 = ¬[↑ {(b, 1), (b, 0)}]ϕ 6, * . Note that this time we have to use negation, since the spoiler moves from the second state in the pair.

Finally, we consider the states 1, 2, where the spoiler strategy is

T (1, 2) = (1, {3}). We compute v = F χ P (α(1)) = {(a, 1)} (for P = {3}) and obtain ϕ 1,2 = [↑ {(a, 1)}] x∈{1,2,4,...,9} ϕ 3,x .
In fact, here it is sufficient to consider x = 4 and x = 5, resulting in the following distinguishing formula:

[↑ {(a, 1)}] ¬[↑ {(b, 0), (b, 1)}][↑ {(e, 1)}]tt ∧ ¬[↑ {(b, 0), (b, 1)}][↑ {(f, 1)}]tt .

Recoding Modalities

Finally, we will show under which conditions one can encode cone modalities into given generic modalities, determined by a separating set of predicate liftings Λ, not necessarily monotone. We first need the notion of strong separation. Definition 25. Let Λ be a separating set of predicate liftings of the form λ : F 2 → 2. We call Λ strongly separating if for every t 0 = t 1 with t 0 , t 1 ∈ F 2 there exists λ ∈ Λ such that λ(t 0 ) = λ(t 1 ). We can generate a set of strongly separating predicate liftings from every separating set of predicate liftings.

Lemma 26. Let Λ be a separating set of predicate liftings. Furthermore we denote the four functions on 2 by id 2 , one (constant 1-function), zero (constant 0-function) and neg (neg(0) = 1, neg(1) = 0).

Then Λ = {λ, λ • F one, λ • F zero, λ • F neg | λ ∈ Λ}
is a set of strongly separating predicate liftings. Furthermore for every formula ϕ we have that

[λ • F one]ϕ ≡ [λ]tt [λ • F zero]ϕ ≡ [λ]ff [λ • F neg]ϕ ≡ [λ](¬ϕ)
This means that we can still express the new modalities with the previous ones.

Λ is just an auxiliary construct that helps us to state the following proposition. The construction of Λ from Λ was already considered in [26, Definition 24], where it is called closure.

Proposition 27. Suppose that F 2 is finite, and let Λ be a strongly separating set of predicate liftings. Moreover, let v ∈ F 2, and let ϕ be a formula. For u ∈ F 2, we write

Λ u = {λ ∈ Λ | λ(u) = 1}. Then [↑ v]ϕ ≡ v≤ F u λ∈Λu [λ]ϕ ∧ λ / ∈Λu ¬[λ]ϕ .
By performing this encoding inductively, we can transform a formula with cone modalities into a formula with modalities in Λ. The encoding preserves negation and conjunction, only the modalities are transformed.

Example 28. We come back to labelled transition systems and the functor F = P f (A × (-)), with A = {a, b}. In this case the set {2 a , 2 b , 3 a , 3 b } of predicate liftings is strongly separating. Now let v = {(a, 0), (b, 1)} ∈ P f (A × 2). We show how to encode the corresponding cone modality using only box and diamond:

[↑ v]ϕ ≡ (¬2 a ϕ ∧ 2 b ϕ ∧ ¬3 a ϕ ∧ 3 b ϕ) ∨ (¬2 a ϕ ∧ 2 b ϕ ∧ 3 a ϕ ∧ 3 b ϕ) ∨ (2 a ϕ ∧ 2 b ϕ ∧ 3 a ϕ ∧ 3 b ϕ)
The first term describes {(a, 0), (b, 1)}, the second {(a, 0), (a, 1), (b, 1)} and the third {(a, 1), (b, 1)}.

Note that we cannot directly generalize Proposition 27 to the case where F 2 is infinite. The reason for this is that the disjunction over all u ∈ F 2 such that v ≤ F u might violate the cardinality constraints of the logic. Hence we will consider an alternative, where the re-coding works only under certain assumptions. We will start with the following example.

Example 29. Consider the functor F = (D(-)+1) A (see also Example 17) and the corresponding (countable) separating set of (monotone) predicate liftings

Λ = {λ (a,q) : F 2 → 2 | a ∈ A, q ∈ [0, 1] ∩ Q} ∪ {λ (a,•) | a ∈ A} where λ (a,q) (v) = 1 if v(a) ∈ R and v(a) ≥ q and λ (a,•) = 1 if v(a) = •.
Here, [λ (a,q) ]ϕ indicates that we do not terminate with a, and the probability of reaching a state satisfying ϕ under an a-transition is at least q, and a modality [λ (a,•) ] ignores its argument formula, and tells us that we terminate with a.

The disjunction v≤ F u in the construction of [↑ v]ϕ in Proposition 27 is in general uncountable and may hence fail to satisfy the cardinality constraints of the logic. However, we can exploit certain properties of this set of predicate liftings, in order to re-code modalities.

Lemma 30. Let F be the functor with F = (D(-) + 1) A and let Λ be the separating set of predicate liftings from Example 29. Then

↑ v = λ∈Λ,λ(v)=1
λ for all v ∈ F 2.

(1)

Note that this property does not hold for the 2 and 3 modalities for the functor

F = P f (A × (-)
). This can be seen via Figure 2, where the upward closure of {(b, 0)} contains three elements. However, {(b, 0)} is only contained in the modality 2 a (and no other modality), which does not coincide with the upwardclosure of {(b, 0)}.

The following proposition, which relates to the well-known fact that predicate liftings are closed under infinitary Boolean combinations (e.g. [START_REF] Schröder | Expressivity of coalgebraic modal logic: The limits and beyond[END_REF]), provides a recipe for transforming cone modalities ↑ v into given modalities Λ satisfying (1) as in Lemma 30: Proposition 31. Given a set Λ ⊆ Λ of predicate liftings, understood as subsets of F 2, we have

[ λ∈Λ λ]ϕ ≡ λ∈Λ [λ]ϕ.
Note that this construction might again violate the cardinality constraints of the logic. In particular, for the probabilistic case (Example 17) we have finite formulas, but countably many modalities. However, if we assume that the set of labels A is finite and restrict the coefficients in the coalgebra to rational numbers, every cone modality can be represented as the intersection of only finitely many minimal given modalities and so the encoding preserves finiteness.

5 T-Beg: A Generic Tool for Games and the Construction of Distinguishing Formulas

Overview

A tool for playing bisimulation games is useful for teaching, for illustrating examples in talks, for case studies and in general for interaction with the user.

There are already available tools, providing visual feedback to help the user understand why two states are (not) bisimilar, such as The Bisimulation Game Game5 or Bisimulation Games Tools6 [START_REF] De Frutosescrig | Games for Bisimulations and Abstraction[END_REF]. Both games are designed for labelled transition systems and [START_REF] De Frutosescrig | Games for Bisimulations and Abstraction[END_REF] also covers branching bisimulation. Our tool T-Beg goes beyond labelled transition system and allows to treat coalgebras in general (under the restrictions that we impose), that is, we exploit the categorical view to create a generic tool. As shown earlier in Sections 3 and 4, the coalgebraic game defined in Definition 2 provides us with a generic algorithm to compute the winning strategies and distinguishing formulas.

The user can either take on the role of the spoiler or of the duplicator, playing on some coalgebra against the computer. The tool computes the winning strategy (if any) and follows this winning strategy if possible. We have also implemented the construction of the distinguishing formula for two non-bisimilar states.

The genericity over the functor is in practice achieved as follows: The user either selects an existing functor F (e.g. the running examples of the paper), or implements his/her own functor by providing the code of one class with nine methods (explained below). Everything else, such as embedding the functor into the game and the visualization are automatically handled by T-Beg. In the case of weighted systems, T-Beg even handles the graphical representation.

Then, he/she enters or loads a coalgebra α : X → F X (with X finite), stored as csv (comma separated value) file. Now the user can switch to the game view and start the game by choosing one of the two roles (spoiler or duplicator) and selecting a pair of states (x 0 , x 1 ), based on the visual graph representation. Next, Fig. 6: Screenshot of the graphical user interface with a game being played. the computer takes over the remaining role and the game starts: In the game overview, the user is guided through the steps by using two colors to indicate whether it is spoiler's (violet) or duplicator's (cyan) turn (see Figure 6).

In the case of two non-bisimular states, the tool will display a distinguishing formula at the end of the game.

Design

We now give an overview over the design and the relevant methods within the tool. We will also explain what has to be done in order to integrate a new functor.

T-Beg is a Windows tool offering a complete graphical interface, developed in Microsoft's Visual Studio using C#, especially Generics. It uses a graph library 7 , which in turn provides a GraphEditor that allows for storing graphs as MSAGL files or as png and jpg files.

The program is divided into five components: Model, View, Controller, Game and Functor. We have chosen MVC (Model View Controller) as a modular pattern, so modules can be exchanged. Here we have several Model T managed by the Controller , where the functor in the sense of a Functor class, which always implements the Functor Interface, is indicated by the parameter T .

While the tool supports more general functors, there is specific support for functors F with F = V G(-) where V specifies a semiring and G preserves finite sets. That is, F describes the branching type of a weighted transition system, where for instance G = A × (-) + 1 (introducing finitely many labels and termination). Coalgebras are of the form X → V GX or -via currying -of the form X × GX → V , which means that they can be represented by X × GX-matrices (matrices with index sets X, GX). In the implementation V is the generic data type of the matrix entries. In the case of the powerset functor we simply have V = 2 and G = Id .

If the branching type of the system can not simply be modelled as a matrix, there is an optional field that can be used to specify the system, since Model T calls the user-implemented method to initialize the F -coalgebra instance. The implementation of Algorithm 1 can be found in Game T, V , representing the core of the tool's architecture, whose correctness is only guaranteed for functors that meet our requirements, such as the functors used in the paper.

Functor Interface As mentioned previously, the user has to provide nine methods in order to implement the functor in the context of T-Beg: two are needed for the computation, two for rendering the coalgebra as a graph, one for creating modal formulas, another two for loading and saving, and two more for customizing the visual matrix representation.

We would like to emphasize here that the user is free to formally implement the functor in the sense of the categorical definition as long as the nine methods needed for the game are provided. In particular, we do not need the application of the functor to arrows since we only need to lift predicates p : X → 2.

Within MyFunctor , which implements the interface Functor F , V , the user defines the data structure F for the branching type of the transition system (e.g., a list or bit vector for the powerset functor, or the corresponding function type in the case of the distribution functor). Further, the user specifies the type V that is needed to define the entries of X × GX (e.g. a double value for a weight or 0, 1 to indicate the existence of a transition).

Here we focus on five methods which have to be provided, omitting the remaining four which are less central.

Matrix F , V InitMatrix (. . . ): This method initializes the transition system with the string-based input of the user. The information about the states and the alphabet is provided via an input mask in the form of a matrix. bool CheckDuplicatorsConditionStep2 (. . . ): given two states x 0 , x 1 and two predicates p 0 , p 1 , this method checks whether F p 0 (α(x 0 )) ≤ F F p 1 (α(x 1 )).

This method is used when playing the game (in Step 2) and in the partition refinement algorithm (Algorithm 1) for the case p 0 = p 1 . TSToGraph(. . . ): This method handles the implementation of the graph-based visualization of the transition system. For weighted systems the user can rely on the default implementation included within the Model. In this case, arrows between states and their labels are generated automatically. GraphToTS (. . . ): This method is used for the other direction, i.e. to derive the transition system from a directed graph given by Graph. string GetModalityToString(. . . ): This method is essential for the automatic generation of the modal logical formulas distinguishing two non-bisimilar states as described in Definition 18. In each call, the cone modality that results from F χ P (α(s)) with T (x 0 , x 1 ) = (s, P ) is converted into a string.

The implementation costs arising on the user side can be improved by employing a separate module that automatically generates functors (see [START_REF] Deifel | Generic Partition Refinement and Weighted Tree Automata[END_REF]). But it is not clear whether the lifting of the preorder can be obtained automatically.

Conclusion and Discussion

Our aim in this paper is to give concrete recipes for explaining non-bisimilarity in a coalgebraic setting. This involves the computation of the winning strategy of the spoiler in the bisimulation game, based on a partition refinement algorithm, as well as the generation of distinguishing formulas, following the ideas of [START_REF] Cleaveland | On Automatically Explaining Bisimulation Inequivalence[END_REF]. Furthermore we have presented a tool that implements this functionality in a generic way. Related tools, as mentioned in [START_REF] De Frutosescrig | Games for Bisimulations and Abstraction[END_REF], are limited to labelled transition systems and mainly focus on the spoiler strategy instead of generating distinguishing formulas.

In the future we would like to combine our prototype implementation with an efficient coalgebraic partition refinement algorithm, adapting the ideas of Kanellakis/Smolka [START_REF] Kanellakis | CCS Expressions, Finite State Processes, and Three Problems of Equivalence[END_REF] or Paige/Tarjan [START_REF] Paige | Three Partition Refinement Algorithms[END_REF] or using the existing coalgebraic generalization [START_REF] Dorsch | Efficient Coalgebraic Partition Refinement[END_REF], thus enabling the efficient computation of winning strategies and distinguishing formulae.

For the generation of distinguishing formulas, an option would be to fix the modalities a priori and to use them in the game, similar to the notion of λbisimulation [START_REF] Gorín | Simulations and Bisimulations for Coalgebraic Modal Logics[END_REF][START_REF] König | Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras[END_REF]. However, there might be infinitely many modalities and the partition refinement algorithm can not iterate over all of them. A possible solution would be to find a way to check the conditions symbolically in order to obtain suitable modalities.

Of course we are also interested in whether we can lift the extra assumptions that were necessary in order to re-code modalities in Section 4.3. We also expect that the bisimulation game can be extended to polyadic predicate liftings.

An interesting further idea is to translate the coalgebra into multi-neighbourhood frames [START_REF] Hansen | Monotonic Modal Logics[END_REF][START_REF] Kracht | Normal Monomodal Logics Can Simulate All Others[END_REF], based on the predicate liftings, and to derive a λbisimulation game as in [START_REF] König | Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras[END_REF][START_REF] Gorín | Simulations and Bisimulations for Coalgebraic Modal Logics[END_REF] from there. (The λ-bisimulation game does not require weak pullback preservation and extends the class of admissible functors, but requires us to fix the modalities rather than generate them.) One could go on and translate these multi-neighbourhood frames into Kripke frames, but this step unfortunately does not preserve bisimilarity.

We also plan to study applications where we can exploit the fact that the distinguishing formula witnesses non-bisimilarity. For instance, we see interesting uses in the area of differential privacy [START_REF] Chatzikokolakis | Generalized Bisimulation Metrics[END_REF], for which we would need to generalize the theory to a quantitative setting. That is, we would like to construct distinguishing formulas in the setting of quantitative coalgebraic logics, which characterize behavioural distances.

Fig. 5 :

 5 Fig. 4: Probabilistic transition system

Available at: https://www.uni-due.de/theoinf/research/tools tbeg.php

For a function f : X → Y , ker (f ) = {(x0, x1) | x0, x1 ∈ X, f (x0) = f (x1)} ⊆ X × X.

http://www.brics.dk/bisim/

https://www.jeroenkeiren.nl/blog/on-games-and-simulations/

Acknowledgements We would like to thank the reviewers for the careful reading of the paper and their valuable comments. Furthermore we thank Thorsten Wißmann and Sebastian Küpper for inspiring discussions on (efficient) coalgebraic partition refinement and zippability.

Work by the first two authors supported by the DFG project BEMEGA (KO 2185/7-2). Work by the third author forms part of the DFG project ProbDL2 (SCHR 1118/6-2)