Compress the Policy, Verify the Loss: dtControl 2+ε Turns Approximation into an Auditable Budget

TL;DR for operators

If a large automated policy contains thousands of state-specific decisions, must every one be preserved exactly before the policy can be reviewed or deployed safely? dtControl 2+$\varepsilon$ starts from a different premise: some decisions can change without materially changing the objective the controller was built to achieve. It uses an explicit objective-level tolerance to determine how much performance loss may be accepted, removes decision detail that does not need to be preserved, and model-checks the resulting controller before accepting it.¹

At $\varepsilon=10^{-2}$, dtControl 2+$\varepsilon$ produced trees with at most 15 nodes on 30 of 38 evaluated benchmarks, including single-node trees on 18. The key distinction is that the tolerance bounds degradation in achieved objective value, not disagreement with one exact optimal action.

For organizations compressing automated policies, this makes approximation an auditable budget rather than an informal shortcut: compression heuristics may propose aggressive simplifications, but the verifier retains final authority over whether the resulting policy stays within the authorized loss. The paper does not establish that small trees are automatically understandable to humans, nor that the same compression ratios transfer beyond the tested MDP and PRISM setting.

Must every optimal decision survive compression?

Suppose an automatically synthesized policy contains thousands—or millions—of state-action entries. If the policy is going to be deployed, reviewed, maintained, or certified, representing every entry exactly appears to be the conservative choice.

That assumption mixes two different requirements. One is reproducing the same action as an optimal controller in every state. The other is preserving the value of the objective the controller was optimized to achieve. Those are not equivalent.

Some states may almost never matter. In others, several actions may lead to the same optimal value. Elsewhere, choosing differently may affect the objective so little that the difference fits inside an explicitly accepted performance tolerance. Exact action imitation can therefore preserve decision detail that contributes little or nothing to achieved performance.

dtControl 2+$\varepsilon$ is built around that separation. Its tolerance is not a decision-tree classification-error rate. A resulting controller $\pi$ is acceptable when its value from the initial state remains within $\varepsilon$ of the optimum:

The budget is expressed in the control objective itself. This makes $\varepsilon$ an auditable policy-design parameter rather than a generic approximation threshold.

Compression begins before the tree is learned

The system does not simply take a weaker deterministic controller and ask a decision tree to imitate it. It starts from optimal information produced through Storm, then changes what the tree is required to represent.

One mechanism is permissiveness. If several actions remain compatible with the required objective value, the training representation can retain those alternatives instead of declaring one particular optimal action uniquely correct. The tree learner consequently has more freedom to merge states that would otherwise require separate branches.

The second mechanism is relevance reduction. Four procedures identify decisions that need not remain explicit:

Agency makes the performance budget especially concrete. For a reachability objective, the paper measures how much controller choice can change the attainable probability from a state:

A state with zero agency cannot change the attainable value through controller choices. Sufficiently low-agency states can be omitted while spending part of the allowed $\varepsilon$ budget under the paper’s reduction argument.

These reductions are not merely tree-learning heuristics. The paper proves that every controller consistent with the dataset produced by its safe construction procedure remains $\varepsilon$-optimal. The compression target has therefore already been narrowed before the decision tree attempts to generalize across states.

Aggressive heuristics are allowed because Storm can reject them

The later stages are deliberately less conservative.

dtControl 2+$\varepsilon$ adds model-derived predicates, state-importance weighting, early stopping, weighted action selection, and greedy pruning. Early stopping and pruning can create smaller trees, but they are not independently covered by the safe-dataset guarantee.

The system-level safeguard is a verification loop. A candidate tree is translated back into a controller and checked with Storm against the requested objective precision. If simplification pushes performance outside the permitted bound, the system backs away from the aggressive optimization.

This allocation of decision rights is central to the architecture. The tree learner proposes simplifications; it does not certify them. Storm decides whether the resulting controller remains acceptable.

For operational systems, that is a more defensible pattern than requiring every compression heuristic to be intrinsically safe. Heuristics can search aggressively when a sufficiently authoritative verifier can evaluate the artifact that will actually be deployed.

The 38 benchmarks show that the discarded detail can be large

The main comparison covers 38 PRISM MDP benchmark/property instances under fixed resource limits. Thirty-four come from a quantitative-verification benchmark collection and four from the earlier dtControl 2 evaluation. The principal outcome is decision-tree node count.

The best dtControl 2+$\varepsilon$ configuration produced smaller trees than dtControl 2 on every benchmark, with reductions exceeding two orders of magnitude on 12.

Increasing the allowed performance deviation produced another clear compression effect. Trees with at most 15 nodes were obtained on:

• 15 of 38 benchmarks at $\varepsilon=0$;
• 28 of 38 at $\varepsilon=10^{-6}$;
• 30 of 38 at $\varepsilon=10^{-2}$.

At $\varepsilon=10^{-2}$, 18 benchmarks produced single-node trees.

The ablations help explain where those reductions come from. Disabling the dataset-reduction machinery more than doubled pre-pruning tree size on average for each initial-dataset family. That experiment is an ablation: its purpose is to establish that relevance filtering contributes materially to compression, not to introduce a separate method.

The pruning experiment serves a similar diagnostic role. Across all evaluated instances, model-checked pruning reduced tree size by roughly 16–58% on average depending on configuration and $\varepsilon$. Among cases where pruning actually changed the tree, reductions were roughly 50–79%. Larger tolerances generally permitted more pruning.

The system also completed all but one benchmark within its 20-minute overall limit. That supports feasibility under the reported experimental conditions, rather than a general scalability claim for arbitrary controller sizes or objectives.

The business pattern is verified simplification

What the paper directly shows: in the evaluated MDP setting, large amounts of state-level controller detail can sometimes be removed while retaining an explicit bound on degradation of the actual control objective. Model-aware filtering, permissive action sets, tree learning, and post-learning verification collectively produce much smaller symbolic controllers.

Cognaptus inference: organizations operating large automated policies could use the same allocation principle when implementation, review, or certification cost grows with policy complexity. The relevant management decision is not merely “how much compression can we tolerate?” It is “which objective degradation are we prepared to authorize, and what independent mechanism can verify that the deployed simplification remains inside that authorization?”

That could shift engineering effort away from exhaustively preserving inconsequential decisions and toward testing the decisions that materially change outcomes.

But two boundaries matter.

First, node count is only a proxy for explainability. A 10-node tree with complicated predicates may be harder to understand than its size suggests. The paper does not include a human interpretability study, and finite-memory LTL controllers introduce additional semantic problems because their memory states can appear as opaque numerical identifiers.

Second, the comparative evidence is concentrated on PRISM models and does not include non-trivial LTL objectives in the 38-benchmark suite. Some $\varepsilon=0$ cases are also affected by numerical inconsistencies in model-checker output, and the CAV15 baseline is necessarily a reimplementation rather than the unavailable original prototype.

These constraints limit claims about general transfer. They do not undermine the narrower architectural result.

Let the compressor propose; let the verifier decide

dtControl 2+$\varepsilon$ changes the unit of fidelity. Instead of asking whether every state reproduces an optimal controller’s exact action, it asks whether the simplified controller still achieves an explicitly acceptable objective value.

That shift permits substantial decision detail to disappear. More importantly, it gives the approximation process a governance structure: relevance analysis determines what may be omitted safely, heuristics search for further simplification, and probabilistic model checking retains the authority to reject a compressed policy that spends too much of the performance budget.

For automated policies whose complexity has become an implementation or assurance problem, that architecture suggests a precise rule: simplify according to consequence, and verify the resulting behavior rather than trusting the simplification procedure itself.

Cognaptus: Automate the Present, Incubate the Future.