dsh-petrinet

When several agents collaborate on a long-horizon objective, the costliest failure modes are silent deadlocks, lock inversion, and uncontrolled concurrency. Traditional orchestration leans on scattered conditionals and manual token hand-offs that are hard to audit and impossible to verify before a single step runs.

dsh-petrinet models a plan as a Petri net: tokens drift through places, transitions consume and produce them, and one unified firing rule simultaneously expresses concurrency caps, loops, and runtime fan-out. Before a plan is committed to the durable log, a static soundness gate enumerates the reachability graph and either proves van der Aalst's three workflow-net conditions or hands back a concrete deadlock marking as a counterexample. The execution event stream doubles as a process-mining log, so the runtime can score a proposed repair against what actually happened and apply fixes in layers—from free, history-derived parameter tweaks to an LLM-authored replacement spec—each still passing the soundness gate before it ships.

It suits teams running multi-step, multi-agent workflows inside DeepSeek Harness that need provable resource bounds and a failure mode that surfaces at planning time rather than after forty hours of runtime.