agenticraft_foundation.algebra.equivalence

Process equivalence checking — trace equivalence, strong/weak bisimulation, and failures equivalence.

Process equivalence checking for CSP.

This module provides: - Trace equivalence: P =_T Q iff traces(P) = traces(Q) - Strong bisimulation: P ∼ Q (finest equivalence) - Weak bisimulation: P ≈ Q (observational equivalence) - Failures equivalence: P =_F Q (CSP standard)

Equivalence hierarchy (finest to coarsest)::

Strong bisimulation (∼)
    ⊂ Weak bisimulation (≈)
        ⊂ Failures equivalence (=_F)
            ⊂ Trace equivalence (=_T)

EquivalenceResult dataclass

Result of an equivalence check.

Failure dataclass

A failure: (trace, refusal set).

trace_equivalent(p, q, max_trace_length=100)

Check trace equivalence: traces(P) = traces(Q).

Two processes are trace equivalent if they can perform exactly the same sequences of visible events.

PARAMETER	DESCRIPTION
p	First process or LTS TYPE: Process | LTS
q	Second process or LTS TYPE: Process | LTS
max_trace_length	Maximum trace length to consider TYPE: int DEFAULT: 100

RETURNS	DESCRIPTION
EquivalenceResult	EquivalenceResult with equivalence status

strong_bisimilar(p, q)

Check strong bisimulation: P ∼ Q.

Strong bisimulation is the finest process equivalence. P ∼ Q iff there exists a relation R such that: - (P, Q) ∈ R - If (P', Q') ∈ R and P' ─a→ P'', then Q' ─a→ Q'' and (P'', Q'') ∈ R - Symmetrically for Q'

PARAMETER	DESCRIPTION
p	First process or LTS TYPE: Process | LTS
q	Second process or LTS TYPE: Process | LTS

RETURNS	DESCRIPTION
EquivalenceResult	EquivalenceResult with bisimulation relation if equivalent

weak_bisimilar(p, q)

Check weak bisimulation: P ≈ Q.

Weak bisimulation ignores τ (internal) actions. P ≈ Q iff there exists a relation R such that: - (P, Q) ∈ R - If (P', Q') ∈ R and P' ─a→ P'', then Q' ═a⇒ Q'' and (P'', Q'') ∈ R where ═a⇒ means τ·a·τ (zero or more τ, then a, then zero or more τ) - Symmetrically for Q'

PARAMETER	DESCRIPTION
p	First process or LTS TYPE: Process | LTS
q	Second process or LTS TYPE: Process | LTS

RETURNS	DESCRIPTION
EquivalenceResult	EquivalenceResult with bisimulation relation if equivalent

failures(lts, max_trace_length=50)

Generate failures of an LTS.

A failure is a pair (s, X) where: - s is a trace the process can perform - X is a set of events the process can refuse after s

PARAMETER	DESCRIPTION
lts	The LTS to analyze TYPE: LTS
max_trace_length	Maximum trace length TYPE: int DEFAULT: 50

YIELDS	DESCRIPTION
Failure	Failure objects

failures_equivalent(p, q, max_trace_length=50)

Check failures equivalence: P =_F Q.

Two processes are failures equivalent if they have exactly the same failures.

PARAMETER	DESCRIPTION
p	First process or LTS TYPE: Process | LTS
q	Second process or LTS TYPE: Process | LTS
max_trace_length	Maximum trace length TYPE: int DEFAULT: 50

RETURNS	DESCRIPTION
EquivalenceResult	EquivalenceResult with equivalence status

are_equivalent(p, q, equivalence='trace')

Check if two processes are equivalent.

PARAMETER	DESCRIPTION
p	First process TYPE: Process
q	Second process TYPE: Process
equivalence	Type of equivalence: - "trace": Trace equivalence - "strong": Strong bisimulation - "weak": Weak bisimulation - "failures": Failures equivalence TYPE: str DEFAULT: 'trace'

RETURNS	DESCRIPTION
bool	True if processes are equivalent