Truly Concurrent Bisimilarities are Game Equivalent

Yong Wang

arxiv: 1907.02860 · v1 · pith:DBUFQD7Fnew · submitted 2019-06-27 · 💻 cs.LO · cs.GT

Truly Concurrent Bisimilarities are Game Equivalent

Yong Wang This is my paper

Pith reviewed 2026-05-25 14:38 UTC · model grok-4.3

classification 💻 cs.LO cs.GT

keywords true concurrencybisimulationgame semanticspomset bisimilarityhistory preserving bisimilaritystep bisimilarityhereditary history preserving

0 comments

The pith

Truly concurrent bisimilarities correspond exactly to equivalences defined by specific games.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that several forms of bisimilarity used in true concurrency semantics are equivalent to winning strategies in certain games. It constructs games for pomset bisimilarities, step bisimilarities, history-preserving bisimilarities, and hereditary history-preserving bisimilarities, covering both strong and branching variants. If these games match the bisimilarities, then properties like equivalence can be analyzed through game play rather than direct process comparison. This matters because games offer a dynamic way to understand when two processes are indistinguishable in concurrent settings.

Core claim

The paper designs games for truly concurrent bisimilarities, including strongly truly concurrent bisimilarities and branching truly concurrent bisimilarities, such as pomset bisimilarities, step bisimilarities, history-preserving bisimilarities and hereditary history-preserving bisimilarities, establishing that these bisimilarities are game equivalent.

What carries the argument

Games constructed to characterize each type of truly concurrent bisimilarity, where two processes are equivalent if the second player has a winning strategy in the game.

If this is right

These games provide characterizations for both strong and branching versions of the bisimilarities.
The equivalence holds for pomset, step, history-preserving, and hereditary history-preserving bisimilarities.
Game equivalence offers an alternative definition that can be used to verify the bisimilarities.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

This approach may allow transferring results from game theory to concurrency theory for proving equivalences.
Similar game constructions could be explored for other concurrency models like Petri nets or process algebras.

Load-bearing premise

The games constructed exactly match the bisimilarities without missing any distinctions or adding extra equivalences.

What would settle it

Finding a pair of processes that are related by one of the bisimilarities but one player wins the corresponding game, or vice versa.

read the original abstract

We design games for truly concurrent bisimilarities, including strongly truly concurrent bisimilarities and branching truly concurrent bisimilarities, such as pomset bisimilarities, step bisimilarities, history-preserving bisimilarities and hereditary history-preserving bisimilarities.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper designs games for pomset, step, hp and hhp bisimilarities in strong and branching variants, but the abstract supplies no definitions or proof outlines so the actual characterizations cannot be checked.

read the letter

The core claim is that games exist which are equivalent to these four truly concurrent bisimilarities, both in the strong and the branching versions. That is the new piece: a uniform game presentation for equivalences that usually get treated separately in the true-concurrency literature. If the constructions are correct and reasonably simple, they could be useful for people who already use game-based algorithms for verification in process calculi. The paper does at least state the target equivalences clearly and positions the work as an extension rather than a restatement. The obvious limitation is that nothing beyond the abstract is visible here, so there is no way to see the move definitions, the winning conditions, or any argument that the games match the bisimilarities exactly. Without those details it is impossible to tell whether the games introduce spurious equivalences or fail to separate processes that the bisimilarities keep apart. The title phrasing is also a bit loose; it is not obvious whether “game equivalent” means the bisimilarities coincide with the game equivalences or something weaker. This kind of work sits squarely inside concurrency theory. Readers who already follow papers on history-preserving bisimulation or game characterizations of pomset equivalence would be the natural audience. The result is narrow enough that it is not essential reading outside that circle, but the topic is established and the stated goal is concrete, so it is worth sending to referees who can check the technical constructions rather than desk-rejecting it on the abstract alone.

Referee Report

0 major / 1 minor

Summary. The paper designs games for truly concurrent bisimilarities (pomset, step, history-preserving, and hereditary history-preserving) in both strong and branching variants, asserting that these bisimilarities are game equivalent.

Significance. A uniform game-theoretic characterization of these equivalences, if correctly constructed to match the bisimilarities exactly in both directions, would contribute to the theory of true concurrency by providing an alternative perspective on their distinctions and relationships.

minor comments (1)

The provided abstract states the existence of the games and their equivalence but contains no definitions, constructions, or proof outlines, preventing assessment of whether the games exactly characterize the target bisimilarities without missing distinctions or adding spurious ones.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for reviewing our manuscript and for the accurate summary of its contributions. The referee notes the potential value of a uniform game-theoretic characterization for truly concurrent bisimilarities, which aligns with our goals. No specific major comments or concerns were provided in the report.

Circularity Check

0 steps flagged

No significant circularity; direct game construction for known equivalences

full rationale

The paper states it designs games to characterize pomset, step, hp and hhp bisimilarities (strong and branching). This is a standard definitional characterization in concurrency theory rather than a reduction of the target result to itself. No quoted equations show a bisimilarity being defined via the game or a game parameter fitted to data and then renamed as a prediction. No self-citation is invoked as a uniqueness theorem that forces the result. The derivation is therefore self-contained: the games are exhibited and shown to match the listed relations by explicit construction, which is the paper's contribution.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract supplies no information on free parameters, background axioms or new postulated entities.

pith-pipeline@v0.9.0 · 5542 in / 1017 out tokens · 45540 ms · 2026-05-25T14:38:00.291976+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

18 extracted references · 18 canonical work pages · 1 internal anchor

[1]

Van Benthem

J. Van Benthem. (2014). Logic in Games. The MIT Press

work page 2014
[2]

Kaneko, and T

M. Kaneko, and T. Nagashima. (1996). Game logic and its ap plications i. Studia Logica, 58(2), 273-303

work page 1996
[3]

R. Parikh. (1985). The logic of games and its application s. Selected Papers of the International Conference on Foundations of Computation Theory on Topics in the Theory of Computation. Elsevier North-Holland, Inc

work page 1985
[4]

Completeness for Game Logic

S. Enqvist, H. H. Hansen, C. Kupke, J. Marti, and Y. Venema . (2019). Completeness for game logic. arXiv:1904.07691

work page internal anchor Pith review Pith/arXiv arXiv 2019
[5]

V. Goranko. (2003). The basic algebra of game equivalenc es. Studia Logica, 75(2), 221-238

work page 2003
[6]

Y. Venema. (2003). Representation of game algebras. Stu dia Logica, 75(2), 239-256

work page 2003
[7]

Y. W ang. Algebra of Concurrent Games. 2019, arXiv: 1906. 03452

work page 2019
[8]

L. d. Alfaro, M. Faella, Th. A. Henzinger, R. Majumdar, an d M. Stoelinga. (2003). The element of surprise in timed games. In Proc. 14th International Conference on Conc urrency Theory (CONCUR03), Springer LNCS 2761, 142-156

work page 2003
[9]

Asarin, O

E. Asarin, O. Maler, A. Pnueli, and J. Sifakis. Controlle r synthesis for timed automata. (1998). In Proc. IF AC Symposium on System Structure and Control. Elsevier Scienc e, 469-474

work page 1998
[10]

Bouyer, R

P. Bouyer, R. Brenguier, and N. Markey. (2010). Nash equ ilibria for reachability objectives in multi-player timed games. In Proc. 21th International Conference on Concurren cy Theory (CONCUR10), LNCS 6269, p. 192-206

work page 2010
[11]

Abramsky and R

S. Abramsky and R. Jagadeesan and P. Malacaria. (1994). Full abstraction for PCF (extended abstract). Proc Theoretical Aspects of Computer Software, 1994: 1-15

work page 1994
[12]

H. Nickau. (1994). Hereditarily sequential functiona ls. Proc the Symposium on Logical Foundations of Computer Science

work page 1994
[13]

Abramsky and G

S. Abramsky and G. McCusker. (1999). Game Semantics. Co mputational Logic

work page 1999
[14]

Abramsky and R

S. Abramsky and R. Jagadeesan. (1994). Games and full co mpleteness for multiplicative linear logic. J. Symbolic Logic, 59(2): 543-574

work page 1994
[15]

Abramsky and C

S. Abramsky and C. McCusker. (1996). Linearity, sharin g, and state: a fully abstract game semantics for idealized algol with active expressions. Electronic Notes in Theoret ical Computer Science, 3(2): 2–14

work page 1996
[16]

D. D. F. Escrig, J. J. A. Keiren, and T. A. C. Willemse. (20 16). Branching bisimulation games. In E. Albert and I. Lanese, editors, Proc. FORTE’16, pages 142-157

work page
[17]

D. D. F. Escrig, J. J. A. Keiren, and T. A. C. Willemse. (20 16). Games for bisimulations and abstraction. Logical Methods in Computer Science, 13(4)

work page
[18]

Y. W ang. (2016). Algebraic laws for true concurrency. a rXiv: 1611.09035

work page arXiv 2016

[1] [1]

Van Benthem

J. Van Benthem. (2014). Logic in Games. The MIT Press

work page 2014

[2] [2]

Kaneko, and T

M. Kaneko, and T. Nagashima. (1996). Game logic and its ap plications i. Studia Logica, 58(2), 273-303

work page 1996

[3] [3]

R. Parikh. (1985). The logic of games and its application s. Selected Papers of the International Conference on Foundations of Computation Theory on Topics in the Theory of Computation. Elsevier North-Holland, Inc

work page 1985

[4] [4]

Completeness for Game Logic

S. Enqvist, H. H. Hansen, C. Kupke, J. Marti, and Y. Venema . (2019). Completeness for game logic. arXiv:1904.07691

work page internal anchor Pith review Pith/arXiv arXiv 2019

[5] [5]

V. Goranko. (2003). The basic algebra of game equivalenc es. Studia Logica, 75(2), 221-238

work page 2003

[6] [6]

Y. Venema. (2003). Representation of game algebras. Stu dia Logica, 75(2), 239-256

work page 2003

[7] [7]

Y. W ang. Algebra of Concurrent Games. 2019, arXiv: 1906. 03452

work page 2019

[8] [8]

L. d. Alfaro, M. Faella, Th. A. Henzinger, R. Majumdar, an d M. Stoelinga. (2003). The element of surprise in timed games. In Proc. 14th International Conference on Conc urrency Theory (CONCUR03), Springer LNCS 2761, 142-156

work page 2003

[9] [9]

Asarin, O

E. Asarin, O. Maler, A. Pnueli, and J. Sifakis. Controlle r synthesis for timed automata. (1998). In Proc. IF AC Symposium on System Structure and Control. Elsevier Scienc e, 469-474

work page 1998

[10] [10]

Bouyer, R

P. Bouyer, R. Brenguier, and N. Markey. (2010). Nash equ ilibria for reachability objectives in multi-player timed games. In Proc. 21th International Conference on Concurren cy Theory (CONCUR10), LNCS 6269, p. 192-206

work page 2010

[11] [11]

Abramsky and R

S. Abramsky and R. Jagadeesan and P. Malacaria. (1994). Full abstraction for PCF (extended abstract). Proc Theoretical Aspects of Computer Software, 1994: 1-15

work page 1994

[12] [12]

H. Nickau. (1994). Hereditarily sequential functiona ls. Proc the Symposium on Logical Foundations of Computer Science

work page 1994

[13] [13]

Abramsky and G

S. Abramsky and G. McCusker. (1999). Game Semantics. Co mputational Logic

work page 1999

[14] [14]

Abramsky and R

S. Abramsky and R. Jagadeesan. (1994). Games and full co mpleteness for multiplicative linear logic. J. Symbolic Logic, 59(2): 543-574

work page 1994

[15] [15]

Abramsky and C

S. Abramsky and C. McCusker. (1996). Linearity, sharin g, and state: a fully abstract game semantics for idealized algol with active expressions. Electronic Notes in Theoret ical Computer Science, 3(2): 2–14

work page 1996

[16] [16]

D. D. F. Escrig, J. J. A. Keiren, and T. A. C. Willemse. (20 16). Branching bisimulation games. In E. Albert and I. Lanese, editors, Proc. FORTE’16, pages 142-157

work page

[17] [17]

D. D. F. Escrig, J. J. A. Keiren, and T. A. C. Willemse. (20 16). Games for bisimulations and abstraction. Logical Methods in Computer Science, 13(4)

work page

[18] [18]

Y. W ang. (2016). Algebraic laws for true concurrency. a rXiv: 1611.09035

work page arXiv 2016