petri_net_nn.coverability

coverability

Karp-Miller coverability analysis for unbounded Petri nets.

The bisimulation and soundness checkers in PETRA assume the net is bounded — that the reachable marking space is finite, so BFS terminates and partition refinement applies. Most well-designed business processes are bounded by construction, but some are not, and a process that quietly accumulates work at one place is a production-incident waiting to surface. This module answers the prior question: is this net bounded at all, and if not, which places are the ones blowing up?

The algorithm is the classical Karp-Miller construction. Starting from the initial marking, every reachable marking is generated by BFS. When a newly-generated marking M' strictly covers an ancestor M on its path from the root — meaning M' >= M componentwise and M' != M — each place where M' exceeds M is replaced with the sentinel ω ("arbitrarily many"). The tree is finite by Dickson's lemma: there is no infinite antichain on N^k, and once a place is ω-marked, subsequent firings can only leave it ω or remove tokens it never runs out of, so branching is contained.

A place is unbounded iff some node in the coverability tree carries ω at it. The :class:CoverabilityReport returned by :func:coverability_graph pins exactly which places those are, the per-place upper bound for the bounded ones, and a list of ω-marking witnesses.

Scope and limits

• Plain Petri nets, arc weights, multi-token markings: fully decidable. The Karp-Miller algorithm gives the exact answer.

• Inhibitor arcs: handled conservatively. An ω-marked inhibitor place is treated as non-empty, so the inhibitor arc blocks the transition. This is sound (no real firings are missed) but may overreport unboundedness in some pathological cases. The reason is fundamental, not a tool limitation: inhibitor-arc Petri nets are Turing-complete (Minsky 1967), so exact coverability would solve the halting problem. The BUSINESS_ANALYST_GUIDE §17 has a long-form treatment of why this boundary is mathematical rather than a missing feature.

• Coloured tokens, durations, rates, guards: these Phase 9 extensions affect the trained network and the coloured token-game; coverability operates on the raw discrete structural net (places, transitions, flow, arc weights, inhibitors) and ignores them. A coloured net that is unbounded structurally will still be reported as unbounded; a net whose unboundedness depends on coloured-token routing logic may not be analysable here.

The max_nodes guard (default 10,000) raises ValueError if the coverability tree exceeds the cap. Karp-Miller terminates in principle for every Petri net, but a degenerate net with many places and frequent ω introductions can still produce a large tree.

CoverabilityReport dataclass

CoverabilityReport(is_bounded, unbounded_places=list(), place_bounds=dict(), omega_markings=list())

Outcome of a Karp-Miller coverability analysis.

The headline field is :attr:is_bounded; the rest pin which places are unbounded, how high the bounded ones can go, and which specific markings witness the unboundedness.

Attributes

is_bounded True iff no place in any node of the coverability tree carries ω. A bounded net has a finite reachable marking space — exactly the precondition the rest of PETRA's verification checks assume. unbounded_places Names of the places that can hold arbitrarily many tokens. Sorted alphabetically. Empty iff the net is bounded. place_bounds Per-place upper bound on the token count across the coverability tree. OMEGA for unbounded places, an integer for bounded ones. The integer bound is attained — some reachable marking actually puts that many tokens at the place. Every place declared on the net appears here (with bound 0 if no reachable marking ever puts a token on it — those places would be flagged by the soundness checker's dead-transition pass too). omega_markings Coverability nodes that carry ω at one or more places. These are the witnesses for unboundedness: each one records "the net can reach a state where these places hold arbitrarily many tokens." Sorted for deterministic output. Empty iff the net is bounded.

summary

summary()

One-line human-readable digest. "bounded" on a bounded net; "unbounded at N place(s): p1, p2, ..." on an unbounded one. Useful for log lines and assertion messages.

Source code in petri_net_nn/coverability.py

def summary(self) -> str:
    """One-line human-readable digest. ``"bounded"`` on a
    bounded net; ``"unbounded at N place(s): p1, p2, ..."`` on
    an unbounded one. Useful for log lines and assertion
    messages."""
    if self.is_bounded:
        return "bounded"
    return (
        f"unbounded at {len(self.unbounded_places)} place(s): "
        f"{', '.join(self.unbounded_places)}"
    )

coverability_graph

coverability_graph(net, *, max_nodes=10000)

Compute the Karp-Miller coverability tree of net and return a :class:CoverabilityReport.

Identifies which places (if any) can hold arbitrarily many tokens — i.e., are unbounded. Sound and exact on nets without inhibitor arcs; conservative (may overreport unboundedness) on nets that use them. See the module-level docstring for the reasoning behind the conservative treatment.

Parameters

net The PetriNet to analyse. Doesn't need to be bounded — that's the whole point. The initial marking provides the root of the coverability tree. max_nodes Tree-size cap; raises ValueError if the visited set exceeds it. Defensive guard: Karp-Miller terminates in principle, but degenerate inputs can still produce large trees.

Returns

CoverabilityReport is_bounded flag, list of unbounded place names, the per-place bounds, and the ω-marking witnesses for any unboundedness.

Source code in petri_net_nn/coverability.py

def coverability_graph(
    net: PetriNet, *, max_nodes: int = 10_000
) -> CoverabilityReport:
    """Compute the Karp-Miller coverability tree of ``net`` and
    return a :class:`CoverabilityReport`.

    Identifies which places (if any) can hold arbitrarily many
    tokens — i.e., are *unbounded*. Sound and exact on nets
    without inhibitor arcs; conservative (may overreport
    unboundedness) on nets that use them. See the module-level
    docstring for the reasoning behind the conservative
    treatment.

    Parameters
    ----------
    net
        The PetriNet to analyse. Doesn't need to be bounded —
        that's the whole point. The initial marking provides the
        root of the coverability tree.
    max_nodes
        Tree-size cap; raises ``ValueError`` if the visited set
        exceeds it. Defensive guard: Karp-Miller terminates in
        principle, but degenerate inputs can still produce large
        trees.

    Returns
    -------
    CoverabilityReport
        ``is_bounded`` flag, list of unbounded place names, the
        per-place bounds, and the ω-marking witnesses for any
        unboundedness.
    """
    root_dict: dict[str, "int | float"] = {
        p: c for p, c in net.initial_marking.items() if c > 0
    }
    root = _dict_to_marking(root_dict)

    # Tree-shaped exploration: each visited marking remembers its
    # parent so we can walk back to the root and apply
    # omega-introduction against every ancestor on the path.
    parent: dict[OmegaMarking, OmegaMarking | None] = {root: None}
    visited: set[OmegaMarking] = {root}
    queue: deque[OmegaMarking] = deque([root])

    while queue:
        m = queue.popleft()
        m_dict = dict(m)

        # Sorted iteration over transitions keeps the visited set
        # deterministic across runs, which makes the omega_markings
        # list deterministic too.
        for t in sorted(net.transitions):
            if not _is_enabled_omega(net, t, m_dict):
                continue
            m_next_dict = _fire_omega(net, t, m_dict)

            # Karp-Miller omega-introduction: walk every ancestor
            # from m back to the root. If m_next strictly covers an
            # ancestor a, promote every place where m_next exceeds
            # a to ω. The promotion is monotone — once a place is
            # ω, subsequent ancestor checks leave it that way — so
            # the order of ancestor visits does not matter.
            ancestor: OmegaMarking | None = m
            while ancestor is not None:
                a_dict = dict(ancestor)
                if _strictly_covers(m_next_dict, a_dict):
                    # list() snapshot because we mutate m_next_dict
                    # during iteration (assigning to existing keys
                    # would be safe, but a snapshot keeps the
                    # intent explicit).
                    for p in list(m_next_dict.keys()):
                        if m_next_dict[p] > a_dict.get(p, 0):
                            m_next_dict[p] = OMEGA
                ancestor = parent[ancestor]

            m_next = _dict_to_marking(m_next_dict)

            if m_next in visited:
                # Already explored from another path; no new
                # information to gain by re-expanding.
                continue
            if len(visited) >= max_nodes:
                raise ValueError(
                    f"coverability tree exceeded {max_nodes} nodes; "
                    f"this is unusual for Karp-Miller — raise the cap "
                    f"with max_nodes= or simplify the net"
                )
            visited.add(m_next)
            parent[m_next] = m
            queue.append(m_next)

    # Tally: which places carry ω anywhere in the tree, what the
    # maximum integer value reached at each bounded place is, and
    # which specific nodes witness the unboundedness.
    unbounded: set[str] = set()
    bounds: dict[str, "int | float"] = {p: 0 for p in net.places}
    omega_witnesses: list[OmegaMarking] = []

    for node in visited:
        has_omega = False
        for p, c in node:
            if c == OMEGA:
                unbounded.add(p)
                bounds[p] = OMEGA
                has_omega = True
            elif bounds.get(p, 0) != OMEGA:
                # Track the integer bound only if the place hasn't
                # already been flagged as unbounded elsewhere in
                # the tree.
                bounds[p] = max(bounds[p], int(c))
        if has_omega:
            omega_witnesses.append(node)

    # Sort the witnesses by their sorted-place-tuple representation
    # so the output is deterministic. The lexicographic order over
    # tuples sorts ω after every finite integer (inf > any int),
    # which is the natural reading.
    omega_witnesses.sort(key=lambda m: sorted(m, key=lambda x: x[0]))

    return CoverabilityReport(
        is_bounded=not unbounded,
        unbounded_places=sorted(unbounded),
        place_bounds=bounds,
        omega_markings=omega_witnesses,
    )

is_bounded

is_bounded(net, *, max_nodes=10000)

Convenience wrapper: True iff every place in net is bounded. Equivalent to coverability_graph(net).is_bounded but spelled at the use-site as a one-liner question.

Useful as a precondition guard before calling any of the other verification checks (bisimulation, soundness, CTL) that assume the reachable state space is finite — those checks raise ValueError from the max_states guard rather than silently going wrong, but is_bounded lets the caller catch the case explicitly.

Source code in petri_net_nn/coverability.py

def is_bounded(net: PetriNet, *, max_nodes: int = 10_000) -> bool:
    """Convenience wrapper: ``True`` iff every place in ``net`` is
    bounded. Equivalent to ``coverability_graph(net).is_bounded``
    but spelled at the use-site as a one-liner question.

    Useful as a precondition guard before calling any of the other
    verification checks (bisimulation, soundness, CTL) that assume
    the reachable state space is finite — those checks raise
    ``ValueError`` from the ``max_states`` guard rather than
    silently going wrong, but ``is_bounded`` lets the caller catch
    the case explicitly."""
    return coverability_graph(net, max_nodes=max_nodes).is_bounded