Pith. sign in

REVIEW 3 major objections 4 minor 30 references

One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics

T0 review · 3 major / 4 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper proves that a single eight-dimensional energy game captures every weak behavioral equivalence between branching bisimilarity and weak trace equivalence: an attacker wins with a given energy budget exactly when a distinguishing…

desk verdict A genuinely novel game-forcing characterization of the silent-step spectrum, but the advertised one-game-for-all-equivalences claim rests on coordinate assignments that are largely unproven. read the letter →

arxiv 2411.14584 v1 pith:4EDXC7PH submitted 2024-11-21 cs.LO

Benjamin Bisping (TU Berlin) , David N. Jansen (Institute of Software , Chinese Academy of Sciences) This is my paper · ORCID
classification cs.LO
keywords energygamesweakbehavioralequivalencesbranchingbisimilaritytraceequivalenceHennessy-Milnerlogiclinear-time-branching-timespectrumsilentstepsprocess
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper sets out to turn the silent-step spectrum of process equivalences—the hierarchy of weak behavioral preorders from branching bisimilarity down to weak trace equivalence—into a single algorithmic object. Its central claim is that one eight-dimensional energy game decides all of these equivalences at once. The game is played between an attacker, who tries to distinguish two processes, and a defender, who tries to show they are equivalent; the attacker spends energy in eight dimensions, and each weak equivalence is assigned a coordinate budget. The paper proves that the attacker wins with budget $e$ exactly when some modal formula of expressiveness price at most $e$ distinguishes the processes, so the defender winning with a notion's budget is equivalent to that notion relating the processes. If this is right, a researcher can test a set of processes against the whole spectrum at once and locate exactly which equivalences hold.

What carries the argument

The carrying object is the eight-dimensional energy game $G_\triangle$ together with the price function $\mathit{expr}$ on HMLsrbb formulas. The logic's grammar distinguishes delayed observations $\langle\varepsilon\rangle\chi$ from immediate ones, stable conjunctions that include a $\neg\langle\tau\rangle\top$ conjunct, and branching conjunctions whose positive conjunct is an observation $(\alpha)\phi$. The price function $\mathit{expr}$ maps each formula to a vector in $(\mathbb{N}\cup\{\infty\})^8$ whose components count maximal occurrences of modal observations, branching conjunctions, unstable conjunctions, stable conjunctions, immediate conjunctions, positive-conjunct modal depth, negative-conjunct modal depth, and negation depth. Game moves are designed so that each move consumes the energy corresponding to the production it represents; attacker strategy formulas constructed along winning plays are exactly distinguishing formulas whose price lies below the starting budget. The correctness proof proceeds by mutual induction relating distinguishing formulas to winning budgets in one direction and strategy formulas to distinguishing formulas in the other.

What would settle it

Exhibit two finite processes $p$ and $q$ and an energy vector $e$ such that the attacker wins $G_\triangle$ from $[p,\{q\}]_a$ but no formula $\phi$ in HMLsrbb with $\mathit{expr}(\phi) \leq e$ distinguishes $p$ from $q$, or vice versa; either counterexample would refute Theorem 4.1. A practical version would compare the game's verdict for every named coordinate against an independently implemented standard equivalence checker on a corpus of small transition systems.

Watch

Extended reading notes

Core claim

The central discovery is an exact correspondence between distinguishing modal formulas and winning strategies in a new game. Formulas of the logic HMLsrbb—branching Hennessy-Milner logic with delayed observations, stable conjunctions, and branching conjunctions—are priced by an eight-dimensional vector that counts operator depths along eight expressiveness dimensions, including modal depth, conjunction depths, and negation depth. The corresponding weak spectroscopy energy game $G_\triangle$ is played on attacker positions $[p,Q]_a$, delayed positions $[p,Q]^\varepsilon_a$, and defender conjunction positions; every move consumes or min-selects energy components, mirroring one step of formula construction. Theorem 4.1 states that, for every energy vector $e$, there is a formula of price at most $e$ distinguishing $p$ from every state in $Q$ if and only if the attacker wins $G_\triangle$ from $[p,Q]_a$ with $e$. Since each weak equivalence $N$ is defined by a coordinate $e_N$ in the paper's spectrum figure, the theorem yields $p \preceq_N q$ exactly when the defender wins with $e_N$, so a single game realizes the whole spectrum between stability-respecting branching bisimilarity and weak trace equivalence.

Load-bearing premise

The load-bearing premise is that each named weak equivalence in the spectrum genuinely corresponds to the eight-coordinate energy vector the paper assigns it; the paper defines those equivalences through the coordinates and proves the game theorem for that definition, but it does not fully prove equality to the usual relational or modal characterizations for most of the twenty notions.

Editorial extensions

If this is right

  • A single run of the game computes the pareto frontier of attacker-winning budgets, so all weak equivalences for a pair of processes are decided at once rather than one by one.
  • A set of processes that a user wants equated or distinguished can be tested against the whole spectrum, and the minimal winning budget shows which notions separate them.
  • The game provides decision procedures for stability-respecting and unstable weak equivalences that earlier weak bisimulation games did not cover.
  • The framework is extensible to further notions such as divergence-aware equivalences and to mixed strong-and-weak spectra.
  • On small finite systems the prototype computes answers quickly, with the paper's example taking about 100 ms, making the approach usable for everyday equivalence testing.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Because attacker-winning budgets are upward-closed, the eight-dimensional space defines a continuous scale of expressiveness between the named points, suggesting one could interpolate new 'intermediate' equivalences not listed in the spectrum figure.
  • The minimal budget needed to distinguish two processes could be read as a quantitative distance between them, turning the discrete spectrum into a metric-like measure of behavioral difference.
  • The machine-checked proof covers the game-language correspondence; the human part that still deserves independent scrutiny is the identification of each standard equivalence with its coordinate vector.
  • The exponential complexity on subsets of states suggests the method targets small systems; symbolic or on-the-fly variants would be a natural but untested route to scaling it up.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper introduces an eight-dimensional energy game G△ and a branching Hennessy–Milner logic HMLsrbb with formula prices expr(ϕ). Its main theorem (Theorem 4.1) states that, for every energy vector e, there is a formula of price at most e distinguishing p from a set Q iff the attacker wins the game from [p,Q]a with budget e. The paper then interprets Figure 3, which assigns a coordinate eN to each of 21 weak preorders/equivalences in van Glabbeek's silent-step spectrum, as defining each notion N through the sublanguage {ϕ | expr(ϕ) ≤ eN}. It concludes that one energy game decides the whole spectrum. The authors report an Isabelle/HOL formalization of the correctness proof and a prototype tool (equiv.io, CAAL extension).

Significance. If the coordinate-to-equivalence identifications in Figure 3 are correct, this is a valuable and novel unifying framework: it is the first generalized game characterization of the weak spectrum, and the game-logic correspondence is a genuine intellectual contribution with a machine-checked proof. The design of the game rules around delayed observations, stable conjunctions, and branching conjunctions is careful and well-motivated by the grammar. The paper is also practically useful through the described prototype and the promise of deciding many equivalences at once. However, the advertised external claim that one game decides the standard weak spectrum is only as strong as the unproved identification of Figure 3 coordinates with the usual notions, and that identification is currently asserted rather than established for most entries.

major comments (3)
  1. [Section 2.2, Definition 2.7 and Figure 3] The identification of each named notion N with the coordinate eN is assumed, not proved. Only stability-respecting branching bisimilarity (Lemma 2.1), weak traces (Example 2.4), and weak bisimulation (Example 2.5) receive supporting arguments. For the remaining 18 notions, including readiness, possible futures, impossible futures, contrasimilarity, 2-nested simulation, and the stable variants, no derivation from van Glabbeek's standard characterizations is provided; Definition 2.7 makes 'N' a synonym for the coordinate. Since the paper's headline claim that 'one energy game decides the whole weak spectrum' depends on these coordinates matching the standard notions, a single incorrect coordinate would invalidate the conclusion for that notion even though Theorem 4.1 remains true as a statement about the game. The authors should either supply derivations or formalized correspondences for all coordinates, or explicitly reposition the paper as characterizing only the coordinate-defined relations and discuss agreement with van Glabbeek's notions as an empirical observation.
  2. [Section 4 (Theorem 4.1, Lemmas 4.1–4.3)] The proofs of Theorem 4.1 and its supporting lemmas are deferred to a technical report [6] with only proof sketches in the paper, and the Isabelle/HOL formalization is cited but not described in detail. In particular, it is unclear whether the formalization covers only the game-to-logic direction, the full equivalence in Theorem 4.1, Lemma 2.1 on the modal characterization of stability-respecting branching bisimilarity, or also the coordinate identifications used for the spectrum corollary. Because the formalization is a central piece of evidence for correctness, the paper should include a precise statement of the formalized results and of which parts of the paper's claims are machine-checked.
  3. [Section 3.1, Definition 3.3] The definition of attacker winning budgets as 'defined inductively by the rules' is not a standard inductive definition, because the defender rule quantifies universally over all outgoing moves from a defender position. If the intended object is a least fixpoint over finite winning plays or a greatest fixpoint over infinite plays, that should be stated explicitly; the correctness argument and the termination properties used in Section 5 depend on which fixpoint is meant. The formalization may resolve this, but the paper itself should make the semantics of Definition 3.3 unambiguous.
minor comments (4)
  1. [Section 2.1, Definition 2.2] The grammar uses 'V{ψ, ψ, ...}' and later writes T for the empty conjunction V∅; it would help to introduce the T notation immediately after the grammar rather than in the semantics paragraph.
  2. [Section 3.2, Example 3.2] The text describes a combined 'delay observation' move from [Pτe, {Pτℓ}]a to [Aτe, {Aτℓ, Bτℓ}]a, but Definition 3.4 has separate delay and observation moves; the example should explicitly say that this is a sequence of two moves.
  3. [Section 5, complexity paragraph] The complexity bound contains a typographical error: 'O(| | · |G| ·o)' should include the transition relation symbol in the first factor; please correct the notation.
  4. [Figure 5] The figure is dense and the energy updates are partially omitted; adding arrows for the omitted edges and a legend for the abbreviated labels would improve readability.

Circularity Check

1 steps flagged · score 6.0 of 10

The advertised spectrum result reduces to the coordinate definitions: each named N is defined by its coordinate e_N, and Theorem 4.1 shows the game decides exactly that coordinate-defined preorder.

  1. self definitional [Definition 2.7 (Section 2.2) and Theorem 4.1 (Section 4)]
    "Each notion N named in Figure 3 with coordinate e_N is defined through the language of formulas with prices below, i.e., through O_N = {ϕ | expr(ϕ) ≤ e_N}. Recalling Definition 2.3, that is, p ⪯_N q with respect to notion N, iff no ϕ with expr(ϕ) ≤ e_N distinguishes p from q. So, this paper sees notions of preorder / equivalence to be defined through these coordinates and not through other characterizations."

    The named preorders are stipulated, not derived: N is defined as 'absence of formulas priced at most e_N.' Theorem 4.1 then proves attacker wins with budget e_N exactly when such a formula exists, so defender wins exactly when p ⪯_N q. Thus the headline consequence 'for a notion N with coordinate e_N, p ⪯_N q precisely if the defender wins' is an unfolding of Definition 2.7 combined with the internal game–formula correspondence. It does not establish that the game captures van Glabbeek's standard notion N, because that external identification is only checked for a few entries (e.g., Examples 2.4, 2.5) and asserted for the rest of Figure 3.

full rationale

The core mathematical content—Theorem 4.1 relating attacker-winning energy budgets to distinguishing HMLsrbb formulas, including its Isabelle/HOL formalization—is genuine and not circular. The game and the logic are independently defined, and the equivalence between them is a substantive theorem. However, the advertised claim that 'one energy game decides the whole weak spectrum' depends on Definition 2.7 and Figure 3 identifying each named equivalence N with the coordinate e_N. Since Definition 2.7 explicitly defines N through those coordinates, the subsequent game result for each N is guaranteed by construction once Theorem 4.1 is proved. The paper verifies the coordinate-to-standard correspondence only for weak trace, weak bisimulation, and the stability-respecting branching bisimilarity lemma; the remaining 21 notions are asserted. This is a self-definitional reduction of the spectrum claim, though not of the game-formula theorem itself. Self-citations to prior spectroscopy work are not load-bearing here, and the formalization is independent evidence for Theorem 4.1. Score 6 reflects that the advertised predictions for most named equivalences reduce to the coordinate definitions, while the central internal correspondence still has independent content.

Assumptions & free parameters 1 free parameters · 3 assumptions · 3 invented entities

The central result rests on a hand-assigned coordinate table, on a least-fixed-point reading of winning budgets, and on finite-state assumptions for the decision procedure. The game moves and the logic are newly introduced, and the internal game-to-formula correspondence is the main technical contribution.

free parameters (1)
  • Spectrum coordinates e_N in Figure 3 = e.g. e_T=(∞,0,0,0,0,0,0,0), e_F=(∞,0,1,0,0,0,1,1), with full table in Figure 3
    These eight-dimensional vectors are assigned by hand to each equivalence notion. The paper proves they match standard definitions only for stability-respecting branching bisimilarity and gives examples for weak trace and weak bisimulation; for the rest the correspondence is asserted.
assumptions (3)
  • ad hoc to paper For each notion N, the coordinate e_N in Figure 3 defines N (Definition 2.7).
    The paper explicitly says the notions are defined through these coordinates and not through other characterizations. The external validity of the spectrum claim depends on this identification.
  • domain assumption Winning budgets may be defined by a least fixed point over game graphs that contain cycles.
    Definition 3.3 presents winning budgets inductively, but the game graph has zero-update cycles such as procrastination moves. The paper relies on [5,10] for the semantics without spelling out the fixed point construction.
  • domain assumption The decision procedure assumes finite labeled transition systems.
    Section 5 gives complexity bounds in terms of |P| and |->|, so the Pareto-frontier computation requires finite state spaces, even though the game rules are defined over arbitrary LTSs.
invented entities (3)
  • HMLsrbb logic
    purpose: A modal language whose price-defined sublogics are intended to capture the weak equivalence spectrum.
    New grammar in Definition 2.2, built to match the distinctive powers of the spectrum. Only the characterization of stability-respecting branching bisimilarity is independently validated.
  • Eight-dimensional energy pricing expr
    purpose: Assigns a price vector to every formula, thereby defining sublogics by energy bounds.
    Definition 2.6 chooses eight dimensions and a first-applicable tie-breaking rule by hand; these choices are the currency in which the whole framework is expressed.
  • Weak spectroscopy energy game G△
    purpose: Game whose attacker-winning budgets are claimed to coincide exactly with distinguishing formulas.
    Definitions 3.4 to 3.6 introduce delayed, stable, and branching positions. The correctness theorem is internal to the framework and is not checked against external benchmark semantics for most listed equivalences.

how reviews work

0 comments
Cite this review

Pith. "Pith review of One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics." pith.science (2026). https://pith.science/paper/4EDXC7PH

@misc{pith2026241114584,
  author       = {Pith},
  title        = {Pith review of: One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4EDXC7PH}},
  note         = {Machine review of arXiv:2411.14584}
}
read the original abstract

We provide the first generalized game characterization of van Glabbeek's linear-time--branching-time spectrum with silent steps. Thereby, one multi-dimensional energy game can be used to characterize and decide a wide array of weak behavioral equivalences between stability-respecting branching bisimilarity and weak trace equivalence in one go. To establish correctness, we relate attacker-winning energy budgets and distinguishing sublanguages of Hennessy--Milner logic that we characterize by eight dimensions of formula expressiveness.

Figures

Figures reproduced from arXiv: 2411.14584 by the authors.

Figure 1
Figure 1. How the paper combines the weak spectrum [23] and the spectroscopy approach [5]. [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. A pair of processes Pe and Pℓ together with versions P τ e and P τ ℓ of the two where idle has been abstracted into internal τ-behavior. Example 2.1 [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Hierarchy of weak behavioral equivalences/preorders, becoming finer towards the top. Each [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (5 more)
Figure 3
Figure 3. Figure 3: Accordingly, P τ e is distinguished from P τ ℓ by failure ϕτ ∈ OF, that is, P τ e ̸⪯F P τ ℓ . There neither are strictly-stable nor strictly-positive formulas to distinguish P τ e from P τ ℓ . Therefore, stable bisimula￾tion preorder, P τ e ⪯SB P τ ℓ , and η-simulation…
Figure 4
Figure 4. Figure 4: Schematic spectroscopy game G△ of Definitions 3.4 (the black part), 3.5 (with position (···) s d ), and 3.6 (with positions (···) s d , (···) η d and [···] η a ). Definition 3.4 (Spectroscopy delay game). For a system S = (P,Σ,−→), the spectroscopy delay energy game G …
Figure 5
Figure 5. Figure 5: Spectroscopy delay game Gε from [A τ e ,{A τ ℓ ,B τ ℓ }]a for Example 3.2. Each position names minimal attacker-winning budgets (due to the thick arrows) and corresponding distinguishing formulas (pink). Zeros and 0-updates are omitted for readability. Also, the game g…
Figure 6
Figure 6. Figure 6: Strategy formula constructions for Definition 4.1. [PITH_FULL_IMAGE:figures/full_fig_p013_6.png]
Figure 7
Figure 7. Figure 7: Screenshot of equiv.io solving Example 5.1. Lemma 4.3. If ϕ ∈ Strat([p,Q]a , e), then ϕ distinguishes p from Q. Proof. By induction over the derivation of ··· ∈ Strat(g, e) according to Definition 4.1. Full proof in report [6]. 5 Deciding All Weak Equivalences at Once …

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

30 extracted references · 22 canonical work pages

  1. [6]

    Linear-Time--Branching-Time Spectroscopy Accounting for Silent Steps

    Benjamin Bisping & David N. Jansen (2023): Linear-Time-Branching-Time Spectroscopy Accounting for Silent Steps. arXiv abs/2305.17671. Available at https://doi.org/10.48550/arXiv.2305.17671

    work page Pith review arXiv doi:10.48550/arxiv.2305.17671 2023

  2. [1]

    Andersen, Nicklas Andersen, Søren Enevoldsen, Mathias M

    Jesper R. Andersen, Nicklas Andersen, Søren Enevoldsen, Mathias M. Hansen, Kim G. Larsen, Simon R. Olesen, Jir ´ı Srba & Jacob K. Wortmann (2015): CAAL: Concurrency Workbench, Aalborg Edition . In Martin Leucker, Camilo Rueda & Frank D. Valencia, editors: Theoretical Aspects of Computing – ICTAC 2015, Springer International Publishing, Cham, pp. 573–582. ...

    work page 2015

  3. [2]

    Barwell, Francisco Ferreira & Nobuko Yoshida (2022): CONCUR test-of-time award for the period 1994–97 interview with Uwe Nestmann and Benjamin C

    Adam D. Barwell, Francisco Ferreira & Nobuko Yoshida (2022): CONCUR test-of-time award for the period 1994–97 interview with Uwe Nestmann and Benjamin C. Pierce. Journal of Logical and Algebraic Methods in Programming 125, p. 100744. Available at https://doi.org/10.1016/j.jlamp.2021.100744

    arXiv 2022

  4. [3]

    Bell (2013): Certifiably sound parallelizing transformations

    Christian J. Bell (2013): Certifiably sound parallelizing transformations . In Georges Gonthier & Michael Norrish, editors: Certified Programs and Proofs: CPP , LNCS 8307, Springer, Cham, pp. 227–242, https: //doi.org/10.1007/978-3-319-03545-1_15

    work page doi:10.1007/978-3-319-03545-1_15 2013

  5. [4]

    Harsh Beohar, Sebastian Gurke, Barbara K ¨onig & Karla Messing (2023): Hennessy-Milner Theorems via Galois Connections . In Bartek Klin & Elaine Pimentel, editors: 31st EACSL Annual Conference on Computer Science Logic (CSL 2023) , Leibniz International Proceedings in Informatics (LIPIcs) 252, Schloss Dagstuhl – Leibniz-Zentrum f ¨ur Informatik, Dagstuhl,...

    work page doi:10.4230/lipics.csl.2023.12 2023

  6. [5]

    In Constantin Enea & Akash Lal, editors: Computer Aided Verification, Springer Nature Switzerland, Cham, pp

    Benjamin Bisping (2023): Process Equivalence Problems as Energy Games . In Constantin Enea & Akash Lal, editors: Computer Aided Verification, Springer Nature Switzerland, Cham, pp. 85–106. Available at https://doi.org/10.1007/978-3-031-37706-8_5

    work page doi:10.1007/978-3-031-37706-8_5 2023

  7. [7]

    Jansen & Uwe Nestmann (2022): Deciding All Behavioral Equivalences at Once: A Game for Linear-Time–Branching-Time Spectroscopy

    Benjamin Bisping, David N. Jansen & Uwe Nestmann (2022): Deciding All Behavioral Equivalences at Once: A Game for Linear-Time–Branching-Time Spectroscopy. Logical Methods in Computer Science18(3), pp. 19:1–19:33. Available at https://doi.org/10.46298/lmcs-18(3:19)2022

    work page doi:10.46298/lmcs-18(3:19)2022 2022

  8. [8]

    Benjamin Bisping & Luisa Montanari (2021): A Game Characterization for Contrasimilarity . In Ornela Dardha & Valentina Castiglioni, editors: Proceedings Combined 28th International Workshop on Expres- siveness in Concurrency and 18th Workshop on Structural Operational Semantics, Electronic Proceedings in Theoretical Computer Science 339, Open Publishing A...

    work page doi:10.4204/eptcs.339.5 2021

Show all 30 references
  1. [9]

    Acta Informatica 57(3–5), pp

    Benjamin Bisping, Uwe Nestmann & Kirstin Peters (2020): Coupled similarity: the first 32 years . Acta Informatica 57(3–5), pp. 439–463. Available at https://doi.org/10.1007/s00236-019-00356-4

    2020 doi

  2. [10]

    In Olivier Bournez, Enrico Formenti & Igor Potapov, editors: Reachability Problems, RP 2023, Springer Nature Switzerland, Cham, pp

    Thomas Brihaye & Aline Goeminne (2023): Multi-weighted Reachability Games. In Olivier Bournez, Enrico Formenti & Igor Potapov, editors: Reachability Problems, RP 2023, Springer Nature Switzerland, Cham, pp. 85–97. Available at https://doi.org/10.1007/978-3-031-45286-4_7

    2023 doi

  3. [11]

    Xin Chen & Yuxin Deng (2008): Game Characterizations of Process Equivalences. In G. Ramalingam, edi- tor: Programming Languages and Systems: APLAS , LNCS 5356, Springer, Berlin, pp. 107–121. Available at https://doi.org/10.1007/978-3-540-89330-1_8

    2008 doi

  4. [12]

    Rocco De Nicola & Frits Vaandrager (1995): Three logics for branching bisimulation . J. ACM 42(2), p. 458–487. Available at https://doi.org/10.1145/201019.201032

    1995

  5. [13]

    Larsen & Ji ˇr´ı Srba (2011): Energy Games in Multiweighted Automata

    Uli Fahrenberg, Line Juhl, Kim G. Larsen & Ji ˇr´ı Srba (2011): Energy Games in Multiweighted Automata . In Antonio Cerone & Pekka Pihlajasaari, editors: Theoretical Aspects of Computing – ICTAC 2011, LNCS 6916, Springer, Heidelberg, pp. 95–115. Available athttps://doi.org/10....

    2011 doi

  6. [14]

    Theoreti- cal Computer Science 538, pp

    Uli Fahrenberg & Axel Legay (2014): The quantitative linear-time–branching-time spectrum . Theoreti- cal Computer Science 538, pp. 54–69. Available at https://doi.org/10.1016/j.tcs.2013.07.030. Quantitative Aspects of Programming Languages and Systems (2011-12). B. Bisping & D...

    2014 doi

  7. [15]

    Information and Computation 268, p

    Wan Fokkink, Rob van Glabbeek & Bas Luttik (2019): Divide and congruence III: From decomposition of modal formulas to preservation of stability and divergence . Information and Computation 268, p. 104435. Available at https://doi.org/10.1016/j.ic.2019.104435

    2019

  8. [16]

    In: 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , IEEE, New York, NY , USA, pp

    Chase Ford, Stefan Milius & Lutz Schr ¨oder (2021): Behavioural Preorders via Graded Monads. In: 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , IEEE, New York, NY , USA, pp. 1–13. Available at https://doi.org/10.1109/LICS52264.2021.9470517

    2021

  9. [17]

    Logical Methods in Com- puter Science 9(2:11), pp

    David de Frutos Escrig, Carlos Gregorio Rodr ´ıguez, Miguel Palomino & David Romero Hern ´andez (2013): Unifying the Linear Time-Branching Time Spectrum of Strong Process Semantics. Logical Methods in Com- puter Science 9(2:11), pp. 1–74. Available at https://doi.org/10.2168/L...

    2013 doi

  10. [18]

    David de Frutos Escrig, Jeroen J. A. Keiren & Tim A. C. Willemse (2017): Games for Bisimulations and Abstraction. Logical Methods in Computer Science 13(4:15), pp. 1–40. Available at https://doi.org/ 10.23638/LMCS-13(4:15)2017

    2017 doi

  11. [19]

    Acta Informatica 57(3–5), pp

    Maciej Gazda, Wan Fokkink & Vittorio Massaro (2020): Congruence from the operator’s point of view: Syntactic requirements on modal characterizations . Acta Informatica 57(3–5), pp. 329–351. Available at https://doi.org/10.1007/s00236-019-00355-5

    2020 doi

  12. [20]

    Herman Geuvers (2022): Apartness and distinguishing formulas in Hennessy–Milner Logic. In Nils Jansen, Mari¨elle Stoelinga & Petra van den Bos, editors:A journey from process algebra via timed automata to model learning: essays dedicated to Frits Vaandrager on the occasion of ...

    2022 doi

  13. [21]

    arXiv:2210.07380

    Herman Geuvers & Anton Golov (2023): Positive Hennessy-Milner Logic for Branching Bisimulation . arXiv:2210.07380

    2023

  14. [22]

    Rob van Glabbeek (1990): The linear time–branching time spectrum: extended abstract. In J. C. M. Baeten & J. W. Klop, editors: CONCUR’90, LNCS 458, Springer, Berlin, pp. 278–297. Available at https: //doi.org/10.1007/BFb0039066

    1990 doi

  15. [23]

    In Eike Best, editor: CONCUR’93, LNCS 715, Springer, Berlin, pp

    Rob van Glabbeek (1993): The linear time–branching time spectrum II: The semantics of sequential systems with silent moves; extended abstract . In Eike Best, editor: CONCUR’93, LNCS 715, Springer, Berlin, pp. 66–81. Available at https://doi.org/10.1007/3-540-57208-2_6

    1993 doi

  16. [24]

    Rob van Glabbeek (2001): The Linear Time–Branching Time Spectrum I: The Semantics of Concrete, Se- quential Processes. In J. A. Bergstra, A. Ponse & S. A. Smolka, editors: Handbook of Process Algebra , chapter 1, Elsevier, Amsterdam, pp. 3–99, https://doi.org/10.1016/B978-0444...

    2001 doi

  17. [25]

    Logical Meth- ods in Computer Science 17(2), pp

    Ross Horne & Sjouke Mauw (2021): Discovering ePassport Vulnerabilities using Bisimilarity. Logical Meth- ods in Computer Science 17(2), pp. 24:1–24:52. Available at https://doi.org/10.23638/LMCS-17(2: 24)2021

    2021 doi

  18. [26]

    Orna Kupferman & Naama Shamash Halevy (2022): Energy Games with Resource-Bounded Environments. In Bartek Klin, Sławomir Lasota & Anca Muscholl, editors: 33rd International Conference on Concurrency Theory: CONCUR, LIPIcs 243, Schloss Dagstuhl – Leibniz-Zentrum f¨ur Informatik,...

    2022 doi

  19. [27]

    Jan Martens & Jan Friso Groote (2024): Minimal Depth Distinguishing Formulas Without Until for Branching Bisimulation. In Venanzio Capretta, Robbert Krebbers & Freek Wiedijk, editors:Logics and Type Systems in Theory and Practice: Essays Dedicated to Herman Geuvers on The Occa...

    2024 doi

  20. [28]

    Shukla, Harry B

    Sandeep K. Shukla, Harry B. Hunt III & Daniel J. Rosenkrantz (1996): HORNSAT, Model Checking, Veri- fication and Games: extended abstract . In Rajeev Alur & Thomas A. Henzinger, editors: Computer Aided Verification: CA V, LNCS 1102, Springer, Berlin, pp. 99–110. Available at h...

    1996

  21. [29]

    Li Tan (2002): An Abstract Schema for Equivalence-Checking Games . In Agostino Cortesi, editor: Verifi- cation, Model Checking, and Abstract Interpretation, Third International Workshop, VMCAI 2002, Venice, 88 One Energy Game for the Weak Spectrum Italy, January 21-22, 2002, R...

    2002 doi

  22. [30]

    Thorsten Wißmann, Stefan Milius & Lutz Schr ¨oder (2021): Explaining Behavioural Inequivalence Gener- ically in Quasilinear Time . In Serge Haddad & Daniele Varacca, editors: 32nd International Conference on Concurrency Theory (CONCUR 2021) , Leibniz International Proceedings ...

    2021 doi

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.