pith. sign in

arxiv: 2606.21450 · v1 · pith:6W23S6ZTnew · submitted 2026-06-19 · 💻 cs.LO

Minimal and Canonical Quotients for Simulation Equivalences

Eduardo Costa Martins , Tim Willemse This is my paper

Pith reviewed 2026-06-26 12:35 UTC · model grok-4.3

classification 💻 cs.LO
keywords weak simulation equivalencecoupled similarityquotientsminimisationlabeled transition systemsNP-completecanonical representativessimulation preorders
0
0 comments X

The pith

Weak simulation equivalence and coupled similarity admit unique canonical quotients along with state- and transition-minimal representatives, and finding the minimal version is NP-complete.

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

The paper extends prior quotient constructions from a few equivalences in the linear time-branching time spectrum to weak simulation equivalence and coupled similarity. It supplies abstract procedures that convert any labeled transition system into a unique representative of its equivalence class and into an equivalent system that uses the fewest states and transitions. These procedures matter because they let analysts replace a system with a smaller, canonical version that preserves exactly the same behaviors under the chosen equivalence. The work further establishes that computing such a minimal system is NP-complete.

Core claim

We extend these results to weak simulation equivalence and coupled similarity. We describe abstract procedures for transforming an LTS into a unique representative of its equivalence class, and for transforming an LTS into an equivalent state- and transition-minimal LTS. Moreover, we show the minimisation problem is NP-complete.

What carries the argument

Abstract procedures that construct a canonical quotient and a state-transition-minimal representative of an LTS under a given simulation equivalence.

If this is right

  • Any LTS can be replaced by a unique canonical form that stands for its entire weak simulation equivalence class.
  • A smaller equivalent LTS can be produced that uses the fewest possible states and transitions while preserving the equivalence.
  • The task of computing such a minimal LTS is NP-complete for these equivalences.
  • The same constructions apply to coupled similarity because it is induced by the same underlying simulation preorder.

Where Pith is reading between the lines

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

  • Implementations of these procedures would let verification tools automatically simplify models before checking properties.
  • The NP-completeness result indicates that practical minimisation will require either heuristics or restrictions to special classes of systems.
  • The uniform applicability of the constructions hints that a single algorithmic framework might cover additional equivalences in the spectrum.

Load-bearing premise

The same abstract quotient constructions that worked for previously studied equivalences also apply without modification to weak simulation equivalence and coupled similarity.

What would settle it

An explicit counterexample LTS on which one of the described abstract procedures fails to output a unique canonical representative under weak simulation equivalence.

Figures

Figures reproduced from arXiv: 2606.21450 by Eduardo Costa Martins, Tim Willemse.

Figure 8
Figure 8. Figure 8: Here, it holds that each si ⊏x u, and consequently we may τ -saturate by adding u τ−→ si . Note that if we add a u τ−→ si transition, then each u α−→ ⊥ transition for which α ∈ Si becomes covered, and therefore may be removed. Since each u α−→ ⊥ transition is such that α is in some Si , we may remove every such transition using τ -saturation [PITH_FULL_IMAGE:figures/full_fig_p010_8.png] view at source ↗
read the original abstract

Quotients have only been studied for a handful of equivalences in the linear time-branching time spectrum, for which there are results pertaining to canonicity and minimality. We extend these results to weak simulation equivalence and coupled similarity, two closely related equivalences induced by simulation preorders. We describe abstract procedures for transforming an LTS into a unique representative of its equivalence class, and for transforming an LTS into an equivalent state- and transition-minimal LTS. Moreover, we show the minimisation problem is NP-complete.

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.

Referee Report

1 major / 2 minor

Summary. The paper extends prior results on canonical quotients and minimal representatives for equivalences in the linear time-branching time spectrum to weak simulation equivalence and coupled similarity. It describes abstract procedures that transform an LTS into a unique representative of its equivalence class and into an equivalent state- and transition-minimal LTS, and proves that the minimisation problem is NP-complete.

Significance. If the constructions are shown to be correct for the weak case, the work supplies missing canonicity and minimality results for two simulation-induced equivalences and adds an NP-completeness result to the complexity picture for minimisation. The abstract procedures, once verified, could serve as a reusable framework.

major comments (1)
  1. [Section describing the abstract procedures for weak simulation equivalence] The central extension rests on the claim that the same abstract quotient constructions carry over unmodified to weak simulation equivalence. Because weak simulation is defined via weak transitions (visible actions possibly interleaved with arbitrary tau sequences), the quotient must explicitly preserve or saturate the weak transition relation; if the procedure in the section describing the weak-simulation quotient is defined exactly as in the strong case without additional tau-closure steps, the uniqueness of the representative and the claimed minimality are not guaranteed.
minor comments (2)
  1. Clarify the precise definition of coupled similarity (including its relation to weak simulation) before the quotient construction is presented.
  2. The NP-completeness reduction should explicitly state the source problem and the polynomial-time mapping used.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their thoughtful review and for highlighting this important point regarding the extension to weak simulation equivalence. We address the concern in detail below.

read point-by-point responses

  1. Referee: [Section describing the abstract procedures for weak simulation equivalence] The central extension rests on the claim that the same abstract quotient constructions carry over unmodified to weak simulation equivalence. Because weak simulation is defined via weak transitions (visible actions possibly interleaved with arbitrary tau sequences), the quotient must explicitly preserve or saturate the weak transition relation; if the procedure in the section describing the weak-simulation quotient is defined exactly as in the strong case without additional tau-closure steps, the uniqueness of the representative and the claimed minimality are not guaranteed.

    Authors: The abstract procedures are defined parametrically over an arbitrary transition relation and the induced equivalence. For weak simulation equivalence we instantiate the construction using the weak transition relation (which is already closed under arbitrary tau sequences by definition of weak transitions). Consequently the same unmodified procedure, when applied to this weak relation, automatically preserves and saturates the relevant transitions; no separate tau-closure step is required inside the procedure itself. The canonicity and minimality proofs therefore carry over directly from the general framework. To forestall any misunderstanding we will insert a short clarifying paragraph immediately after the definition of the weak-simulation quotient. revision: partial

Circularity Check

0 steps flagged

No circularity; extension of abstract quotient procedures is self-contained

full rationale

The paper states it extends prior results on canonicity and minimality for a handful of equivalences in the linear time-branching time spectrum to weak simulation equivalence and coupled similarity, describing abstract procedures for unique representatives and state/transition-minimal LTSs plus an NP-completeness proof. No equations, self-citations, or definitional reductions appear in the abstract or description that would make any claimed prediction or uniqueness result equivalent to its inputs by construction. The derivation relies on standard background in the spectrum rather than load-bearing self-citation chains or ansatzes smuggled from prior author work. This is the normal case of an independent extension.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Based solely on the abstract, the work relies on standard domain assumptions about labeled transition systems and the linear time-branching time spectrum; no free parameters, invented entities, or ad-hoc axioms are mentioned.

axioms (1)
  • domain assumption Labeled transition systems and the linear time-branching time spectrum are standard background structures in process algebra.
    Invoked implicitly when referring to quotients for equivalences in the spectrum.

pith-pipeline@v0.9.1-grok · 5601 in / 1204 out tokens · 20891 ms · 2026-06-26T12:35:50.113888+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

23 extracted references · 1 canonical work pages

  1. [1]

    2 Benjamin Bisping and Luisa Montanari

    URL: https://www.sciencedirect.com/science/article/pii/S0304397513002144, doi:10.1016/j.tcs.2013.03.013. 2 Benjamin Bisping and Luisa Montanari. Coupled similarity and contrasimilarity, and how to compute them.Arch. Formal Proofs, 2023, aug 2023. URL:https://www.isa-afp.org/ entries/Coupledsim_Contrasim.html. 3 Benjamin Bisping and Uwe Nestmann. Computing...

    work page doi:10.1016/j.tcs.2013.03.013 2013

  2. [2]

    Sincep′∈max(Gα(p)), it holds that p′≡x p

    If α=τ, then by Lemma 3.3, it holds thatp′⊑x p. Sincep′∈max(Gα(p)), it holds that p′≡x p. Therefore, sinceq τ =⇒qandq≡x p, the desired result holds

  3. [3]

    Using Lemma 3.4 again, there is somep′′⊒x q′such thatp α =⇒p′′

    If α̸=τ, then by Lemma 3.4, there is someq′⊒x p′such thatq α =⇒q′. Using Lemma 3.4 again, there is somep′′⊒x q′such thatp α =⇒p′′. Sincep′is maximal andp′⊑x q′⊑x p′′, it holds thatp′′⊑x p′. Therefore,q′⊑x p′′⊑x p′, showing thatp′≡x q′as desired. ◀ ▶ Lemma 3.6.Let p∈Sand supposex =CS. Then, for allq∈Ssuch thatp⊑q, and all p′∈min(Gτ(p)), there is someq′∈Ssu...

  4. [4]

    Moreover, it holds that s τ =⇒p τ =⇒p′

    If there exists0≤i<nsuch thatsi τ − →si+1 =p α − →q, thenα=τ. Moreover, it holds that s τ =⇒p τ =⇒p′. Sincesi+1 =q and sn =s′, it holds thats′⊑x q, and hences′⊑x q′. Since s′β − →t′. By Lemma 3.10, it holds thats τ =⇒p′τ − →q′. We distinguish two cases. If alsoβ=τ, then by Lemma 3.3 and because there are no inert transitions, it holds that t′⊏x s′. Thent⊏...

  5. [5]

    Since q⊑x q′and t′= q, it holds that t′⊑x q′

    If s′β − →t′= p α − →q, thens τ =⇒p τ =⇒p′α − →q′. Since q⊑x q′and t′= q, it holds that t′⊑x q′. By Lemma 3.10, we haves τ =⇒p′α − →q′. Suppose for the sake of contradiction that s = p′. Then sinces τ =⇒p τ =⇒p′and there are no inert transitions, it holds that p = p′, which is a contradiction since(p′,q′)̸= (p,q ). Therefore, s β − →t is covered by p′α − ...

  6. [6]

    Since t α =⇒t, the simulation condition is satisfied for this pair

    Suppose α=τ, then by Lemma 3.3, it holds thats′⊑x s, and therefore(s′,t)∈R. Since t α =⇒t, the simulation condition is satisfied for this pair

  7. [7]

    Since s⊑x t, it holds thatt α =⇒t′for somet′∈Ssuch that s′⊑t′

    Suppose instead thatα̸= τ. Since s⊑x t, it holds thatt α =⇒t′for somet′∈Ssuch that s′⊑t′. Therefore,( s′,t′)∈R, and it suffices to show thatt α =⇒t′. Since α̸= τ, by Lemma 3.3 we may assume w.l.o.g. thatt τ =⇒t′′α − →t′. Therefore, there exist states t0,...,tn such thatt 0 τ − →... τ − →tn and(t 0,tn) = (t,t′′). We distinguish two cases. If there does not...

  8. [8]

    Since (s′,t′)∈R, the simulation condition is satisfied for this pair

    Ifs α − →s′, then sinces⊑x t, it holds thatt α =⇒t′for somet′∈Ssuch thats′⊑x t′. Since (s′,t′)∈R, the simulation condition is satisfied for this pair

  9. [9]

    Therefore, s τ − →q α − →s′

    Otherwise, it holds thats =p and s′is such thatq α − →s′. Therefore, s τ − →q α − →s′. By Lemma 3.4, it holds thatt α =⇒t′for somet′∈Ssuch thats′⊑x t′. Since(s′,t′)∈R, the simulation condition is satisfied for this pair. Thus, the simulation condition is satisfied for this pair, andRis a simulation. Coupling.We now show that R is a coupled simulation ifx ...

  10. [10]

    If there does not exist0≤i<nsuch that(ti,ti+1) = (p,q ), thent τ =⇒t′, and therefore the coupling condition is satisfied since(t′,s)∈R

  11. [11]

    We distinguish two cases

    If( ti,ti+1) = ( p,q )for some0 ≤i < n, then note that due to the absence of inert transitions, ti =tj implies i =j, so we do not revisitti on this path. We distinguish two cases. If i + 1 = n, thent0 τ − →... τ − →ti τ − →r. Therefore, t τ =⇒r. By Lemma 3.3, it holds that r⊑x q. Sinceq =t′and t′⊑x s, it holds that(r,s )∈R, and thus the coupling condition...

  12. [12]

    Hence, ifp is a state ofL, we writep′to denote the unique state ofL′such that p≡x p′

    For each statep of L, there is exactly one statep′in L′such thatp≡x p′, and vice-versa. Hence, ifp is a state ofL, we writep′to denote the unique state ofL′such that p≡x p′. Likewise, ifp′is a state ofL′, we writep to denote the unique state ofL such that p≡x p′. 2.u ′b − →s′ i for all1≤i≤m. E. Costa Martins and T.A.C. Willemse 25 3.s ′ i ˆSi −→⊥′for all1...

  13. [13]

    Note thatα∈ˆSi iffα∈ˆSi, so therefore s′ i α − →⊥′

    Suppose u′τ − →s′ i for somes′ i such thatα∈ˆSi or α∈ˆSi. Note thatα∈ˆSi iffα∈ˆSi, so therefore s′ i α − →⊥′. Hence, theu′α − →⊥′transition is covered, meaningL′is not minimal, contradicting our choice ofL′

  14. [14]

    Note that there is at least one ˆSi such that α∈ˆSi and α∈ˆSi, so let ˆSi be such

    Otherwise, it holds thats′= u′, and henceu′α − →⊥′. Note that there is at least one ˆSi such that α∈ˆSi and α∈ˆSi, so let ˆSi be such. Then u′α − → ⊥′and u′ˆα − → ⊥′ are covered inL′∪{(u′,τ,s′ i)}. Thus, by Proposition 5.1 and Lemma 3.10, it holds that L′≡x (L′∪{(u′,τ,s′ i)})\{(u′,α,⊥′), (u′,α,⊥′)}, contradicting our choice ofL′as minimal. Therefore p′̸=⊥...

  15. [15]

    Then it holds thata j∈ˆSk, and thusu′τ − →s′ k aj −→inL′′, meaning theu′α − →⊥′transition is covered

    If α=aj for some1≤j≤n, then letSk∈C\{Si}such thataj∈Sk. Then it holds thata j∈ˆSk, and thusu′τ − →s′ k aj −→inL′′, meaning theu′α − →⊥′transition is covered

  16. [16]

    Then it holds thataj∈ˆSk

    If α= aj for some1 ≤j≤n, thenaj∈Si, so there is someSk∈C\{Si}such that aj∈Sk. Then it holds thataj∈ˆSk. Thus, u′τ − →s′ k aj −→in L′′, meaning theu′α − →⊥′ transition is covered. E. Costa Martins and T.A.C. Willemse 27

  17. [17]

    As shown above, there is somes′ k such thatu′τ − →s′ k β − →⊥′in L′′

    If α=τ, then note thatˆSi\{τ}is non-empty, so there is someβ∈ˆSi\{τ}. As shown above, there is somes′ k such thatu′τ − →s′ k β − →⊥′in L′′. Then, sinceτ∈ˆSk, it holds that u′τ − →s′ k τ − →⊥′inL′′, showing that theu′α − →⊥′transition is covered. Hence, each introduced transition is covered inL′′, so by Lemma 3.10 and Lemma 3.12, these may be removed to ob...

  18. [18]

    Note thatp′̸=p since L has no inert transitions

    If p τ − →p′in L, then we may simply takep′′=p. Note thatp′̸=p since L has no inert transitions. 2.Otherwise, we obtain the result using the induction hypothesis. Likewise, it holds thatp′α =⇒qin L. Therefore, we havep τ − →p′′α =⇒qin L, as required. ◀ ▶ Corollary 5.7.Let L =⟨S,Aτ,→,ι⟩be an LTS such thatL2 and L7 have the same set of states. LetZp ={(p,τ,...

  19. [19]

    We distinguish two cases

  20. [20]

    Therefore, p α − →qis covered by p τ − →p′inL 5∪{(p,τ,p′)}

    If α= τ, then by Lemma 3.3, it holds thatq⊑x p′. Therefore, p α − →qis covered by p τ − →p′inL 5∪{(p,τ,p′)}. Hence,(p,α,q)∈CoverableBy5((p,τ,p′))

  21. [21]

    If α̸= τ, then sincep′in L5 is equivalent top′in L2, there exists some stateq′⊒x q such thatp′ 5 α =⇒q′

  22. [22]

    that p′ 5 τ =⇒p′′ 5 α − →q′ 5 for some statep′′

    By Lemma 3.3 and sinceα̸= τ, we may assume w.l.o.g. that p′ 5 τ =⇒p′′ 5 α − →q′ 5 for some statep′′. In particular,p′′⊑x p′⊏x p holds by Lemma 3.3 and the absence of inert transitions. Therefore,p α − →qis covered byp′′α − →q′inL5∪{(p,τ,p′′)}. Hence,(p,α,q)∈CoverableBy5((p,τ,p′′)). In both cases, we achieve our desired result.◀ ▶ Lemma 5.8.Let L =⟨S,Aτ,→,...

  23. [23]

    τ − →pn α − →q′holds inL, then we have a contradiction sincep α − →qis covered inL, butLhas no covered transitions

    If p0 τ − →... τ − →pn α − →q′holds inL, then we have a contradiction sincep α − →qis covered inL, butLhas no covered transitions. 2.If(p,τ,p′) = (pi,τ,pi+1), thenp′τ =⇒r′α − →q′, as required. 3.Otherwise if(p,τ,p′) = (r′,α,q′), thenα=τandp′=q′, and hencep′α =⇒q′. Since p′⊑x p′′and τ-saturation preserves⊑x, there is someq′′⊒x q′such thatp′′α =⇒q′′ in L. W...