ICRL pMDP Specification Decomposition

Context

Neary2022 - Verifiable and Compositional Reinforcement Learning Systems builds an iterative compositional RL (ICRL) loop around a high-level parametric MDP. The pMDP turns subsystem success probabilities into parameters that can be optimized, verified, and refined as low-level RL policies improve.

Formal Statement

Let C={c_1,...,c_k} be a composable collection of partially instantiated subsystems, where each subsystem has entry set I_c, exit set F_c, time horizon T_c, and learned policy pi_c.

For each subsystem define:

$${\sigma }_c^{{\pi }_c}(s)=P_s^{M,{\pi }_c}({◊}_{\le T_c}{F}_c).$$

The subtask specification for parameter p_c requires:

$${\sigma }_c^{{\pi }_c}(s)\ge p_c\text{for every }s\in I_c.$$

The high-level model \tilde M is a pMDP with a success state \tilde s_\checkmark, a failure state \tilde s_\times, and one action per subsystem. Executing subsystem c from a compatible high-level state moves to succ(c) with probability p_c, and to failure with probability 1-p_c.

If each subsystem’s real success probability lower-bounds its parameter, then any high-level policy \tilde\mu induces a meta-policy \mu whose real environment task-success probability is at least the high-level prediction:

$$P_{s_I}^{M,\mu }(◊F_{targ})\ge P_{{\tilde{s}}_I}^{\tilde{M},\tilde{\mu }}(◊{\tilde{s}}_{✓}).$$

Thus, a high-level policy certified to reach \tilde s_\checkmark with probability at least 1-\delta gives a sufficient condition for the composed RL system to satisfy the task specification.

Derivation / Construction

The high-level state abstraction groups environment states by two predicates:

• which subsystem entry sets contain the state;
• whether the state is in the target set.

Composable subsystem interfaces ensure that all states in F_c map to a unique high-level successor succ(c).

The initial task-decomposition problem searches for small subtask thresholds p_c that still permit a high-level policy satisfying the task bound. Neary et al. formulate this with Bellman-flow variables x(\tilde s,c):

$$\min \sum _{c\in C}{p}_c$$

subject to nonnegative flow, 0 <= p_c <= 1, Bellman-flow conservation, and a goal-flow constraint requiring at least 1-\delta probability of reaching the high-level goal. The bilinear terms arise from products of flow variables and pMDP parameters.

After training, each learned subsystem has an empirical performance estimate \hat\sigma_c. ICRL refines the decomposition by:

• minimizing the gap between p_c and \hat\sigma_c;
• constraining p_c >= \hat\sigma_c once a subsystem has already demonstrated that level;
• constraining p_c <= \hat\sigma_c once the subsystem has exhausted its training budget and should no longer be assigned an unrealistic requirement.

The training loop alternates among solving the pMDP parameter problem, selecting the subsystem with a large performance gap, training that subsystem with an RL algorithm such as PPO, estimating subtask success by rollout, and recomputing the high-level meta-policy.

Implications

• The guarantee is compositional but conditional: local subtask-success lower bounds must be trustworthy for the system-level probability lower bound to hold.
• The pMDP separates high-level route choice from low-level control learning, which lets the system stop training irrelevant subsystems.
• Refinement can adapt the meta-policy away from hard subtasks without manually redesigning the decomposition.
• Empirical rollout estimates are a practical weak point; safety-critical use needs statistical confidence bounds, formal verification of subsystem policies, or conservative estimators.

Links

• Source: Neary2022 - Verifiable and Compositional Reinforcement Learning Systems
• Concept: Compositional Reinforcement Learning
• Verification background: Probabilistic Model Checking