Petri-Net Safety Shield for Neural Policies

First, use this as the final action-selection layer of a discrete-action RL controller, neural task planner, or mixture-of-experts router whose experts correspond to Petri-Net transitions. Maintain the marking \(M\) from the observed Boolean plant state; do not infer it only from the policy hidden state unless a separately verified state estimator is available. Construct places for each Boolean variable and resource token, compile each invariant \(C_j(x)\) into an admissibility check, and precompute reachable markings with breadth-first search for a small prototype. At every environment step, compute policy logits \(z=f_\theta(o)\), enumerate transitions \(t\), evaluate \(enabled(t,M)\), calculate \(M_t=fire(t,M)\), reject \(t\) if any \(C_j(M_t)=0\), and set rejected logits to \(-\infty\). Sample or select from the remaining logits, execute the transition, and update \(M\leftarrow M_t\). If no transition is enabled, emit a distinguished deadlock action and log the violated precondition rather than selecting an unsafe action. Enabledness, firing, invariant satisfaction, and reachability are exact symbolic computations for a finite Boolean net; policy quality, observation errors, and deadlock frequency are measured empirically. For large nets, use bounded search or a conservative reachable-state cache, but retain direct invariant checks. The first experiment should use PPO on a grid-world rover task with battery, antenna, motion, and mutually exclusive mode variables. Compare an unshielded MLP, a penalty-trained policy, and the shielded policy. The quantitative prediction is zero post-shield invariant violations under exact observations across at least 10,000 episodes. Invalid but locally plausible actions whose successors are unreachable must be rejected, and the rejected-action rate should decrease during training. Every deadlock should be exactly reproducible from the same marking.