Dynamic HTN Composition with Formal Verification in Holonic BDI Agents: Extending the MINERVA Runtime

Hierarchical Task Network (HTN) planning in BDI architectures guarantees soundness through pre-verified static plan libraries but halts on unrecognized desires (PLAN_NOT_FOUND). We present Dynamic HTN Composition (DHC), an extension to the MINERVA holonic BDI runtime that resolves this brittleness without sacrificing formal guarantees. DHC contributes: (1) an atomic subtask library where each unit is independently pre-verified, (2) a compositional HTN engine assembling subtasks into DAGs at runtime, and (3) Tribunal judge J6, which verifies cross-preconditions, acyclicity, and invariant preservation before execution. We prove that the five HADD invariants (I1–I5) are preserved under composition, and extend the Learning Boundary Theorem to compositional strategy. Empirical evaluation on the MINERVA v0.2 production deployment (87 agents, 617 tests, 99.4% pass rate) shows J6 verifies an 8-node DAG in 13.6 μs (p99: 15.7 μs, >73,000 verif./s), with zero J6.3 invariant violations and 100% PLAN_NOT_FOUND reduction over the static baseline.