Automaton-Supervised Neural Policy Shield

1. Integration point: insert the shield between the neural policy head and the environment or decoder sampler. Maintain one automaton state per agent, together with shared-resource automata for occupancy, capacity, collision, battery, and workflow constraints. The network outputs logits over discrete events; the shield sets disabled-event logits to negative infinity. For stronger planning, enumerate admissible event sequences of length H with beam search, or solve a small MILP when the event space is modest. 2. Pseudocode: initialize x; at each step compute logits = policy(observation); compute mask = supervisor.enabled(x); set logits[e] = -infinity for masked events; for each remaining candidate e simulate x_next = (A x) elementwise-multiplied by (B one_hot(e)); score logits[e] + gamma times value(observation_next, x_next) - lambda times cost(x_next,e); execute the best event; update x = x_next. 3. Compute A, B, C and the supervisor transition table from explicit task and resource rules. Estimate the value term and costs using the neural model or logged rollouts. Verify determinism offline by checking (A B^T) elementwise-multiplied by C = C, and provide a recovery event for every reachable state with an otherwise empty enabled set. 4. First experiment: train PPO on a two-agent grid-world pickup-and-delivery task with corridor collisions, battery limits, charging stations, and mutually exclusive locations. Compare an unshielded MLP, static action masking, and masking plus H=3 beam planning. Measure forbidden transitions, completion, return, and intervention rate. The quantitative prediction is zero forbidden transitions for the exact shield at every policy quality; any nonzero rate exposes an automaton or state-tracking error. Completion should increase or plateau with H, while unshielded violations should increase sharply as shared-resource occupancy approaches capacity.