petri_net_nn.bisimulation

bisimulation

Strong and weak bisimulation for bounded Petri nets.

Implements §7.3 of the architecture spec — a structural check that two Petri nets exhibit the same observable behaviour from their initial markings, where "observable" means the labels on their transitions. The strong checker (are_bisimilar) matches each transition exactly; the weak checker (are_weakly_bisimilar) collapses transitions marked silent=True so refactorings that add or remove internal steps (logging, no-op gates, internal handoffs) don't break the equivalence.

Algorithm: reachability-graph + partition refinement. Each net's labelled transition system is computed by BFS over markings from M_0; the two LTSs are combined and refined into bisimulation equivalence classes; the nets are bisimilar iff their initial markings end up in the same class.

For weak bisimulation, the LTS is saturated first: silent transitions are relabelled to a τ sentinel, the τ-edges are closed reflexive-transitively (every state gains a τ self-loop; τ-paths become direct τ-edges), and each visible-action edge is extended with τ-prefix and τ-suffix detours into all τ-reachable neighbours. Strong bisimulation over the saturated LTS gives weak bisimulation over the original.

Scope: bounded Petri nets only. The BFS terminates exactly when the reachable state space is finite, which is the case for every 1-bounded workflow net produced by parse_bpmn today. A max_states cap raises clearly if a caller feeds in something unbounded.

LTS dataclass

LTS(initial, states, transitions)

Labelled transition system view of a Petri net's reachable markings. The initial field is the canonical frozenset representation of M_0; states contains every reachable marking; transitions records every (from, label, to) edge in the reachability graph.

reachability_graph

reachability_graph(net, *, max_states=10000)

Compute the reachable LTS of net from its initial marking.

Each LTS state is a frozenset of (place, token-count) pairs; this canonical form lets bisimulation refinement use markings as dict keys. max_states guards against accidentally fed unbounded nets — it raises ValueError if the frontier grows past the cap.

Silent transitions appear with their declared label, exactly as visible transitions do; the strong checker treats them as ordinary edges. Use _reachability_graph_with_tau (the weak checker calls it) to relabel silent transitions to TAU.

Source code in petri_net_nn/bisimulation.py

def reachability_graph(net: PetriNet, *, max_states: int = 10_000) -> LTS:
    """Compute the reachable LTS of ``net`` from its initial marking.

    Each LTS state is a frozenset of (place, token-count) pairs;
    this canonical form lets bisimulation refinement use markings
    as dict keys. ``max_states`` guards against accidentally fed
    unbounded nets — it raises ``ValueError`` if the frontier grows
    past the cap.

    Silent transitions appear with their declared label, exactly
    as visible transitions do; the strong checker treats them as
    ordinary edges. Use ``_reachability_graph_with_tau`` (the weak
    checker calls it) to relabel silent transitions to ``TAU``.
    """
    return _lts(net, silent_as_tau=False, max_states=max_states)

bisimulation_equivalence_classes

bisimulation_equivalence_classes(net)

Return the partition of net's reachable markings into bisimulation equivalence classes — markings from which the net exhibits the same labelled future behaviour.

Source code in petri_net_nn/bisimulation.py

def bisimulation_equivalence_classes(net: PetriNet) -> list[frozenset[Marking]]:
    """Return the partition of ``net``'s reachable markings into
    bisimulation equivalence classes — markings from which the net
    exhibits the same labelled future behaviour."""
    lts = reachability_graph(net)
    return _refine_partition(lts.states, lts.transitions)

are_bisimilar

are_bisimilar(net1, net2)

Strong-bisimilarity check between the initial markings of two Petri nets.

The two nets are bisimilar iff their initial markings fall into the same equivalence class of the combined LTS — that is, every labelled successor of one can be matched exactly by a labelled successor of the other, recursively. "Exactly" includes silent transitions, which behave like any other labelled edge here; use :func:are_weakly_bisimilar if you want silent transitions collapsed.

Source code in petri_net_nn/bisimulation.py

def are_bisimilar(net1: PetriNet, net2: PetriNet) -> bool:
    """Strong-bisimilarity check between the initial markings of two
    Petri nets.

    The two nets are bisimilar iff their initial markings fall into
    the same equivalence class of the combined LTS — that is, every
    labelled successor of one can be matched exactly by a labelled
    successor of the other, recursively. "Exactly" includes silent
    transitions, which behave like any other labelled edge here; use
    :func:`are_weakly_bisimilar` if you want silent transitions
    collapsed.
    """
    # Two separate LTSs that we'll combine. Tagging the states keeps
    # net1's and net2's markings disjoint in the combined LTS, so
    # that an accidental marking-collision between the two nets
    # doesn't pre-merge their state spaces.
    lts1 = reachability_graph(net1)
    lts2 = reachability_graph(net2)
    return _initials_in_same_class(lts1, lts2, saturate=False)

are_weakly_bisimilar

are_weakly_bisimilar(net1, net2)

Weak-bisimilarity check between the initial markings of two Petri nets.

Weak bisimulation differs from strong bisimulation in one important way: transitions marked silent=True are treated as invisible internal steps that can be inserted or removed without changing the observable behaviour. A refactoring that adds an internal logging transition, a no-op routing gate, or any other structural artefact whose label nobody cares about will be strongly bisimilar-rejected but weakly bisimilar-accepted — which is what makes the cost-ranked refactoring story actually work for real-world redesigns.

Internally the LTS for each net is built with silent transitions relabelled to the :data:TAU sentinel; both LTSs are then saturated (see :func:_saturate for the algorithm); strong bisimulation over the saturated combined LTS is weak bisimulation over the originals.

Source code in petri_net_nn/bisimulation.py

def are_weakly_bisimilar(net1: PetriNet, net2: PetriNet) -> bool:
    """Weak-bisimilarity check between the initial markings of two
    Petri nets.

    Weak bisimulation differs from strong bisimulation in one
    important way: transitions marked ``silent=True`` are treated as
    invisible internal steps that can be inserted or removed without
    changing the observable behaviour. A refactoring that adds an
    internal logging transition, a no-op routing gate, or any other
    structural artefact whose label nobody cares about will be
    *strongly* bisimilar-rejected but *weakly* bisimilar-accepted —
    which is what makes the cost-ranked refactoring story actually
    work for real-world redesigns.

    Internally the LTS for each net is built with silent transitions
    relabelled to the :data:`TAU` sentinel; both LTSs are then
    saturated (see :func:`_saturate` for the algorithm); strong
    bisimulation over the saturated combined LTS is weak bisimulation
    over the originals.
    """
    # Build each net's LTS with silent transitions collapsed to τ.
    # The strong-bisimulation public API does not relabel — silent
    # is purely a weak-bisimulation concept.
    lts1 = _lts(net1, silent_as_tau=True, max_states=10_000)
    lts2 = _lts(net2, silent_as_tau=True, max_states=10_000)
    return _initials_in_same_class(lts1, lts2, saturate=True)

weak_bisimulation_equivalence_classes

weak_bisimulation_equivalence_classes(net)

The partition of net's reachable markings into weak bisimulation equivalence classes.

Same idea as :func:bisimulation_equivalence_classes, but two markings are in the same class if they exhibit the same visible-action behaviour up to silent τ-detours. Useful for asking "how many distinguishable observable states does this net have?", which collapses transient internal states into the equivalence class of whatever they τ-reach.

Source code in petri_net_nn/bisimulation.py

def weak_bisimulation_equivalence_classes(
    net: PetriNet,
) -> list[frozenset[Marking]]:
    """The partition of ``net``'s reachable markings into **weak**
    bisimulation equivalence classes.

    Same idea as :func:`bisimulation_equivalence_classes`, but two
    markings are in the same class if they exhibit the same
    visible-action behaviour up to silent τ-detours. Useful for
    asking "how many distinguishable observable states does this
    net have?", which collapses transient internal states into
    the equivalence class of whatever they τ-reach.
    """
    lts = _lts(net, silent_as_tau=True, max_states=10_000)
    saturated = _saturate(lts)
    return _refine_partition(saturated.states, saturated.transitions)