Game Constructions that Are Safe for Bisimulation

Marc Pauly March 31, 1999

Abstract

The notion of bisimulation is extended to Game Logic (GL), a logic for reasoning about winning strategies in 2-player games. We show that all game constructions of GL are safe for bisimulation, i.e. that an atomic bisimulation can be lifted to non-atomic games constructed by the operations of GL. As a consequence, bisimilar states satisfy the same GL-formulas.

Contents

1 Introduction 2 2 Playing Games in Kripke Models 2 3 Generalizing Bisimulation for Games 4 4 Safety & Invariance for Bisimulation 5

1 Introduction

While the work of Johan van Benthem covers many areas related to logic, it seems fair to say that the topic of bisimulation can be identified as one of his long-standing interests. Starting with his Ph.D. thesis [vB76] where he identified the modal fragment of first-order logic as the bisimulation-invariant fragment, his interest in questions related to bisimulation continues to the present day, as witnessed e.g. by [vB97, vB96]. Furthermore, he has managed to convey his enthusiasm for this topic (as for many others) to a number of his Ph.D. students including the present author, resulting in theses such as [d’A98] and [Hol98].

The current paper seems appropriate for this Liber Amicorum not only because it is yet another chapter in the great book on bisimulation, but also because it is inspired directly by a paper of Johan van Benthem entitled Program Constructions that Are Safe for Bisimulation [vB93]. In that paper, van Benthem shows that (1) programs constructed from atomic relations and tests by means of composition, union and negation are safe for bisimulation and that conversely (2) all first-order definable relations which are safe for bisimulation can be constructed in this way. This result can be seen as an expressivecompleteness result: Given that we want to treat bisimilar models/processes as the same, we want our program operations to be safe for bisimulation, i.e. they should in some sense preserve the bisimulation. If we accept that any program construction we may want to define has to satisfy this condition, van Benthem’s result says that the operations of composition, union and negation are sufficient to construct any new program operation one may think of, provided it is first-order definable.

As the title of this contribution suggests, the aim of this paper is to extend van Benthem’s line of investigation from programs to games. From a game perspective, one can see programs as special kinds of games, namely games where one player (the computer) makes all the moves. From this angle, it is natural to ask what happens if one adds game constructions which allow the other player to make moves as well. A propositional logic of games which extends Propositional Dynamic Logic (PDL, [Har84, KT90]) with such interaction is Game Logic (GL), introduced in [Par85]. After giving a short introduction to GL (section 2), we shall show that the notion of bisimulation-safety can be extended to game constructions, and that the game constructions of GL are indeed safe for bisimulation. Note that this only establishes one half of the game version of van Benthem’s result, the less challenging half to be sure. Still, it should suffice to show that (and how) van Benthem’s approach can be lifted to a more general modal logic. The more challenging question as to whether one can similarly find an analogous converse result will be left for some other occasion...

2 Playing Games in Kripke Models

GL is a logic to reason about winning strategies in strictly competitive games between two players who we shall call Angel and Demon. The underlying semantic model in which games are played is a Kripke model. (This is more restrictive than in the original paper [Par85] but yields a simpler exposition.) An atomic game g played at state s consists of Angel choosing one of the gsuccessors of s; Angel looses if s has no such successors. A test game φ? consists of checking through a neutral arbiter whether proposition φ holds at that state. If it does, nothing happens (i.e. another game can be played) and otherwise, Demon wins. As for the game operations, π_{1} ∪ π_{2} denotes the game where first Angel chooses which of the two subgames to play and then that game is played. The sequential composition π_{1}; π_{2} of two games consists of first playing π_{1} and then π_{2}, and the iterated game π^{∗} has Angel choose how many π games (possibly none) she wants to play.

Reading the informal explanation of these games carefully, one can notice that Angel makes all the choices/moves in these games. In fact, the game operations described so far do not go beyond the program operations known in PDL. In order to introduce interaction between the players, GL adds an operator dual for role interchange: Playing the dual game π^{d} is the same as playing π with the roles of the players reversed, i.e. any choice made by Angel in π will be made by Demon in π^{d} and vice versa.

Playing a game consists of moving through the states of the model based on the choices the players make. After a game is played, a certain final state of the game (i.e. state of the model) is reached. We want ⟨π⟩φ to express that Angel can play π such that in the resulting state φ holds. In more game-theoretic terminology, Angel has a winning strategy for φ in π, a strategy which brings about φ. Similarly, [π]φ denotes the existence of such a winning strategy for Demon.

After having provided some first intuitions for GL, we shall define the syntax and semantics of GL formally. The language of GL consists of two sorts, games and propositions. Given a set of atomic games Π_{0} and a set of atomic propositions Φ_{0}, games π and propositions φ can have the following syntactic forms, yielding the set of games Π and the set of propositions/formulas Φ:

\begin{matrix}π := & g | φ? | π; π | π ∪ π | π^{∗} | π^{d} \\ φ := & ⊥ | p | ¬φ | φ ∨ φ | ⟨π⟩φ \end{matrix}

where p ∈ Φ_{0} and g ∈ Π_{0}. As usual, we define ⊤ := ¬⊥, [π]φ := ¬⟨π⟩¬φ, φ ∧ ψ := ¬(¬φ ∨ ¬ψ) and φ → ψ := ¬φ ∨ ψ.

As for the semantics, a Kripke model I = (S, {r_{a}|a ∈ Π_{0}}, V), consists of a set of states S, a valuation for the propositional letters V such that for all p ∈ Φ_{0} we have V (p) ⊆ S, and a set of relations r_{a} ⊆ S × S. Given such a model, we can define inductively when a formula φ is true in I at state s, denoted as I, s ⊧ φ:

I, s |̸= ⊥
I, s ⊧ p  iff p ∈ Φ_{0} and s ∈ V (p)
I, s ⊧ ¬φ  iff I, s |̸= φ
I, s ⊧ φ ∨ ψ iff I, s ⊧ φ or I, s ⊧ ψ
I, s ⊧ ⟨π⟩φ iff s ∈ R_{π}(φ^{I})

where φ^{I} := {s ∈ S|I, s ⊧ φ}. The modal clause of the definition makes use of the function R_{π} : P(S) → P(S). Given a set of states X, R_{π}(X) denotes the set of states from which Angel has a strategy in π to bring about X. The function is defined by induction on π for any Y ⊆ S:

\begin{aligned}R_{g}(Y) & = \{s ∈ S|∃t : sr_{g}t & t ∈ Y \} for g ∈ Π_{0} \\ R_{α;β}(Y) & = R_{α}(R_{β}(Y)) \\ R_{α∪β}(Y) & = R_{α}(Y) ∪ R_{β}(Y) \\ R_{φ?}(Y) & = φ^{I} ∩ Y \\ R_{α^{d}}(Y) & = \overline{R_{α}(\overline{Y})} \\ R_{α^{∗}}(Y) & = μX.(Y ∪ R_{α}(X) ⊆ X) \end{aligned}

In this definition, μX.f(X) denotes the smallest set X satisfying f(X). Note that in order to guarantee the existence of this least fixpoint, R_{π} should be monotonic for every game π, i.e. if X ⊆ Y then R_{π}(X) ⊆ R_{π}(Y). We shall not carry out the proof that this is indeed the case, but only remark that the monotonicity requirement is a natural one given our interpretation in terms of strategies: If Angel has a strategy to bring about a state in X, then that strategy trivially brings about a state in Y for every Y ⊇ X.

3 Generalizing Bisimulation for Games

Bisimulation provides an answer to the question: when should two models or processes be considered the same? Different criteria may come to mind depending on what aspects of models one is interested in. If only interested in observable properties of processes, one may choose for finite-trace equivalence, but if interested in mathematical structure, one may choose isomorphism. These equivalence notions (see e.g. [vBB93] for an overview) partition the class of models into equivalence classes, and one may order equivalence notions according to how fine-grained the partition is which they induce. While finite-trace equivalence is often considered as too coarse and isomorphism as too fine, bisimulation is situated between these two extremes.

Definition 1 (Bisimulation) Let I = (S, {r_{a}|a ∈ Π_{0}}, V) and I′ = (S′, {r′_{a}|a ∈ Π_{0}}, V′) be two Kripke models. Then ∼ ⊆ S × S′ is a bisimulation between I and I′ iff for any s ∼ s′ we have

1. I, s ⊧ p iff I′, s′ ⊧ p for all p ∈ Φ_{0}.

2. For all g ∈ Π_{0}: If sr_{g}t, then there is a t′ ∈ S′ such that s′r′_{g}t′ and t ∼ t′.

3. For all g ∈ Π_{0}: If s′r′_{g}t′, then there is a t ∈ S such that sr_{g}t and t ∼ t′.

Two states are bisimilar iff there is a bisimulation ∼ such that s ∼ s′. ⊲

One of the basic results on bisimulation in the context of modal logic states that bisimilar states make exactly the same modal formulas true. In order to extend this result to a logic like PDL, one shows that the three clauses in the definition of bisimulation can be generalized from atomic formulas and atomic games/programs to arbitrary formulas and games/programs. When we say that an operation is safe for bisimulation, we mean exactly this, namely that clauses (2.) and (3.) can be generalized to games containing that operation.

Striving towards such a safety result for GL, we face the problem that for non-atomic games π, we have no r_{π} relation but only a R_{π} function. In order to circumvent this problem, we propose here an alternative version of bisimulation which is expressed in terms of the R_{g} functions. Incidentally, the following definition has been proposed in [vBvES93] as a notion of bisimulation for Concurrent Propositional Dynamic Logic.

Definition 2 (Bisimulation) As in definition 1, but replacing the last two clauses by

2. For all g ∈ Π_{0}: If s ∈ R_{g}(X) then ∃X′ ⊆ S′ such that s′ ∈ R′_{g}(X′) and ∀x′ ∈ X′ ∃x ∈ X : x ∼ x′.

3. For all g ∈ Π_{0}: If s′ ∈ R′_{g}(X) then ∃X ⊆ S such that s ∈ R_{g}(X) and ∀x ∈ X ∃x′ ∈ X′ : x ∼ x′. ⊲

It remains to show that these two definitions really amount to the same thing. Having shown this, we can turn towards the main topic of this paper, safety for bisimulation.

Theorem 1 A relation is a bisimulation in the sense of definition 1 iff it is a bisimulation in the sense of definition 2.

Proof. Suppose a relation ∼ is a bisimulation in the sense of definition 1, and assume that s ∼ s′ and s ∈ R_{g}(X), i.e. for some state t we have sr_{g}t and t ∈ X. Hence there is some t′ such that s′r′_{g}t′ and t ∼ t′. But then s′ ∈ R′_{g}({t′}), so ∼ is also a bisimulation according to definition 2.

Conversely, suppose a relation ∼ is a bisimulation in the sense of definition 2, and assume that s ∼ s′ and sr_{g}t. Then s ∈ R_{g}({t}) and so there is some X′ such that s′ ∈ R′_{g}(X′) and ∀x′ ∈ X′ : t ∼ x′. Hence, there is some t′ such that s′r′_{g}t′ and t′ ∈ X′ and thus t ∼ t′.

□

4 Safety & Invariance for Bisimulation

With the reformulation of bisimulation which definition 2 provides, we can now prove that in Game Logic, bisimilar states satisfy the same formulas. As mentioned before, the crucial part of the proof consists of showing that all the game constructions of GL are safe for bisimulation, i.e. that clauses (2.) and (3.) of definition 2 can be generalized to non-atomic games.

Theorem 2 Let I = (S, {r_{a}|a ∈ Π_{0}}, V) and I′ = (S′, {r′_{a}|a ∈ Π_{0}}, V′) be two Kripke models such that s ∈ S and s′ ∈ S′ are bisimilar. Then 1. For all φ ∈ Φ: I, s ⊧ φ iff I′, s′ ⊧ φ

2. For all π ∈ Π: If s ∈ R_{π}(X) then ∃X′ ⊆ S′ such that s′ ∈ R′_{π}(X′) and ∀x′ ∈ X′ ∃x ∈ X : x ∼ x′.

3. For all π ∈ Π: If s′ ∈ R′_{π}(X) then ∃X ⊆ S such that s ∈ R_{π}(X) and ∀x ∈ X ∃x′ ∈ X′ : x ∼ x′.

Proof. For atomic games and formulas, the claims hold by bisimilarity. For non-atomic formulas, the boolean cases are immediate and we shall only show one direction of (1.) for ⟨π⟩φ. If I, s ⊧ ⟨π⟩φ, s ∈ R_{π}(φ^{I}) and so (by induction hypothesis (2.) for π) there is some X′ such that s′ ∈ R′_{π}(X′) and for all x′ ∈ X′ there is some x ∈ φ^{I} such that x ∼ x′. By induction hypothesis (1.) for φ, this means that X′ ⊆ φ^{I′}, and so by monotonicity, s′ ∈ R′_{π}(φ^{I′}), which establishes that I′, s′ ⊧ ⟨π⟩φ.

As for proving that the game constructions of GL are safe for bisimulation, we shall prove (2.) for non-atomic games. Consider first the case of test φ?: If s ∈ R_{φ?}(X) = φ^{I} ∩ X, let X′ := {x′|∃x ∈ X : x ∼ x′}, where ∼ denotes the bisimulation as usual. Then s′ ∈ R′_{φ?}(X′) by induction hypothesis (1.) for φ, and for all x′ ∈ X′ there is some x ∈ X such that x ∼ x′, simply by definition of X′.

For union, if s ∈ R_{α∪β}(X) we can assume w.l.o.g. that s ∈ R_{α}(X) and apply the induction hypothesis, i.e. for some X′, we have s′ ∈ R′_{α}(X′) and hence also s′ ∈ R′_{α∪β}(X′).

For composition, suppose that s ∈ R_{α}(R_{β}(X)). Using the induction hypothesis for α, there is some Y′ such that s′ ∈ R′_{α}(Y′) and for all y′ ∈ Y′ there is a u ∈ R_{β}(X) such that u ∼ y′. Now let X′ := {x′|∃x ∈ X : x ∼ x′}. We must show that s′ ∈ R′_{α}(R′_{β}(X′)). For this, it suffices by monotonicity to show that Y′ ⊆ R′_{β}(X′). So suppose that y′ ∈ Y′, i.e. for some u ∈ R_{β}(X) we have u ∼ y′. Using the induction hypothesis for β, there is some V′ such that y′ ∈ R′_{β}(V′) and for all v′ ∈ V′ there is some x ∈ X such that x ∼ v′. Hence V′ ⊆ X′ and so by monotonicity, y′ ∈ R′_{β}(X′)

Dual: Suppose s ∈ R_{α^{d}}(X), i.e. s ∉ R_{α}(\overline{X}). Again, let X′ := \{x′|∃x ∈ X : x ∼ x′\}. It is sufficient to show that s′ ∉ R′_{α}(\overline{X′}). Suppose by reductio the contrary. Then there is some Z with s ∈ R_{α}(Z) and for all z ∈ Z there is some x′ ∉ X′ such that z ∼ x′. From this it follows that Z ⊆ \overline{X}, so by monotonicity s ∈ R_{α}(\overline{X}), a contradiction.

Iteration: Let X′ := {x′|∃x ∈ X : x ∼ x′} and Z := {z|∀z′ : z ∼ z′ ⇒ z′ ∈ R′_{α^{∗}}(X′)}. Now it is sufficient to show that R_{α^{∗}}(X) ⊆ Z, and given the definition of R_{α^{∗}}(X) as a least fixpoint, it suffices to show that Z is a fixpoint, i.e. that X ∪ R_{α}(Z) ⊆ Z. Supposing that x ∈ X and for some x′ we have x ∼ x′, we have x′ ∈ X′ ⊆ R′_{α^{∗}}(X′). On the other hand, suppose that x ∈ R_{α}(Z) and x ∼ x′. Then by induction hypothesis, there is some Z′ such that x′ ∈ R′_{α}(Z′) and for all z′ ∈ Z′ there is some z ∈ Z such that z ∼ z′. But then Z′ ⊆ R′_{α^{∗}}(X′), and so by monotonicity x′ ∈ R′_{α}(R′_{α^{∗}}(X′)) ⊆ R′_{α^{∗}}(X′) which completes the proof.

□

References

[d’A98] Giovanna d’Agostino. Modal Logic and Non-Well-founded Set Theory: bisimulation, translation, and interpolation. PhD thesis, University of Amsterdam, 1998.

[vB76] Johan van Benthem. Modal Correspondence Theory. PhD thesis, University of Amsterdam, 1976.

[vB93] Johan van Benthem. Program constructions that are safe for bisimulation. Report CSLI-93-179, CSLI, 1993.

[vB96] Johan van Benthem. Bisimulation: The never-ending story. In J. Tromp, editor, A Dynamic and Quick Intellect. Liber Amicorum Paul Vitány, pages 23–27. CWI, 1996.

[vB97] Johan van Benthem. Modality, bisimulation and interpolation in infinitary logic. Report ML-97-06, Institute for Logic, Language and Computation, University of Amsterdam, 1997.

[vBB93] Johan van Benthem and Jan Bergstra. Logic of transition systems. ILLC Prepublication Series CT-93-03, University of Amsterdam, 1993.

[vBvES93] J. van Benthem, J. van Eijck, and V. Stebletsova. Modal logic, transition systems and processes. Computer Science Report CS-R9321, CWI, 1993.

[Har84] David Harel. Dynamic logic. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume II. D. Reidel Publishing Company, 1984.

[Hol98] Marco Hollenberg. Logic and Bisimulation. PhD thesis, University of Utrecht, 1998.

[KT90] Dexter Kozen and Jerzy Tiuryn. Logics of programs. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B. MIT Press, 1990.

[Par85] Rohit Parikh. The logic of games and its applications. In Marek Karpinski and Jan van Leeuwen, editors, Topics in the Theory of Computation, volume 24 of Annals of Discrete Mathematics. Elsevier, 1985.