Source-linked AI summary
Safety-Constrained Reinforcement Learning for MDPs
Sebastian Junges, Nils Jansen, Christian Dehnert, Ufuk Topcu, Joost-Pieter Katoen
TL;DR
Unknown action costs make safe controller synthesis difficult because costs are learned through exploration, which must avoid unsafe behavior. The paper iteratively computes safe permissive schedulers and uses reinforcement learning within them; the approach is shown correct and complete and works on practical benchmarks with high nondeterminism.
Problem
Action costs are unknown until exploration, but ordinary learning does not ensure that unsafe actions are avoided during exploration.
Source: §1 · p. 2Method
The method iteratively computes safe permissive schedulers, learns within their allowed behavior, and excludes previously considered schedulers as it searches.
Source: §4 · p. 11Results
The prototype works on practical benchmarks involving a high degree of nondeterminism, and the method is shown sound and complete.
Source: §4.1 · p. 12, §6 · p. 15Takeaways & Limitations
The approach provides a route to safe and optimal strategies for stochastic systems with unknown costs.
Source: §1 · p. 3, §6 · p. 15The SMT encoding does not ensure any particular degree of permissiveness in the computed scheduler.
Source: §4.1 · p. 12
Abstract
from arXiv · showhide
We consider controller synthesis for stochastic and partially unknown environments in which safety is essential. Specifically, we abstract the problem as a Markov decision process in which the expected performance is measured using a cost function that is unknown prior to run-time exploration of the state space. Standard learning approaches synthesize cost-optimal strategies without guaranteeing safety properties. To remedy this, we first compute safe, permissive strategies. Then, exploration is constrained to these strategies and thereby meets the imposed safety requirements. Exploiting an iterative learning procedure, the resulting policy is safety-constrained and optimal. We show correctness and completeness of the method and discuss the use of several heuristics to increase its scalability. Finally, we demonstrate the applicability by means of a prototype implementation.
1 Introduction
The paper addresses controller synthesis when action costs are learned during exploration but unsafe behavior must be excluded beforehand. It proposes computing safe permissive schedulers and using iterative reinforcement learning within them to seek an optimal policy.
1 Introduction
- The robot must learn action costs through execution while avoiding unsafe behavior, so it needs a safe strategy that also minimizes cost.The motivation includes robot motion planning with randomly moving hazards and costs that depend on the surface.Source: §1 · p. 2
- Safe permissive schedulers allow multiple actions while restricting behavior to safe choices, enabling exploration without first taking unsafe actions.Source: §1 · p. 2
- The iterative procedure computes a safe permissive scheduler, learns its cost-minimal compliant scheduler, excludes previously considered schedulers, and repeats toward global optimality.The stated stopping conditions are satisfaction of the performance criterion or determination of global optimality using lower bounds on costs.Source: §1 · pp. 2–3
- The paper presents an approach to controller synthesis for stochastic systems with known models but unknown costs, jointly addressing safety and performance.Source: §1 · p. 3
- The contributions include heuristics to speed computation and limit iterations, plus a prototype demonstrated on several case studies.Source: §1 · p. 3
2 Preliminaries
The preliminaries define the stochastic decision model, schedulers, and safety and cost specifications used in the synthesis problem. The formal task is to find a scheduler satisfying both constraints, with costs unknown before exploration.
2 Preliminaries
- An MDP has finite states and actions, with probabilistic transitions; its nondeterministic action choices are resolved by schedulers.Source: §2 · p. 4
- Schedulers resolve action nondeterminism, and applying one to an MDP yields an induced Markov chain; the paper restricts to memoryless schedulers.Source: §2 · p. 4
- The specifications bound the probability of reaching bad states and the expected cost of reaching goal states.The stated verification approach assumes all probabilities and costs are known in advance.Source: §2 · p. 5
- The formal setting combines a controllable MDP with an environmental Markov chain and assumes unknown transition costs have known lower and upper bounds.Source: §2 · p. 5
- Synthesis seeks a scheduler satisfying both the safety and performance specifications; optimal synthesis seeks one minimizing expected cost while satisfying safety.Source: §2 · p. 5
3 Permissive schedulers
Permissive schedulers leave multiple action distributions available at each state, enabling exploration within choices that satisfy a safety specification. Because independently safe choices can combine into an unsafe scheduler, the section develops ways to represent and reason about safe permissive schedulers.
3 Permissive schedulers
- A permissive scheduler assigns each state a set of distributions over actions, leaving multiple choices open rather than resolving all nondeterminism.The section considers memoryless schedulers.Source: §3 · pp. 5–6
- A safe permissive scheduler contains only schedulers satisfying the safety property; a maximal one includes every such scheduler.Source: §3 · p. 6
- Combining statewise choices from individually safe schedulers can admit an unsafe scheduler unless choices remain consistent across states.The example's combined permissive scheduler admits the unsafe scheduler even though the included schedulers are safe.Source: §3 · pp. 6–7
- A conflict set is a set of actions jointly selected by a scheduler that violates the property; minimal conflict sets can grow exponentially with the number of states.Source: §3 · p. 7
- Enumerating minimal conflict sets suggests that an exact representation of the maximal permissive scheduler may be infeasible, motivating a more compact representation.The section investigates induced MDPs as such a representation.Source: §3 · pp. 7–8
- An induced MDP encodes each allowed distribution as a new action and nondeterministically chooses among those distributions; with one distribution per state, it reduces to an induced Markov chain.Source: §3 · p. 8
- The example's safe but nonmaximal scheduler induces a sub-MDP with no scheduler violating the reachability property.Source: §3 · p. 9
4 Safety-constrained reinforcement learning
The method searches safe permissive schedulers iteratively, learning unknown costs only within safe behavior and using lower bounds to test optimality. Its correctness rests on covering safe schedulers, while permissive-scheduler computation and learning provide the operational steps.
4 Safety-constrained reinforcement learning
- Testing permissive scheduler sets with reinforcement learning, lower-bound checks, and skipping costlier deployments can reduce the number of safe-scheduler deployments.The naive approach checks safe schedulers one at a time; the optimizations can decide minimality or avoid further exploration.Source: §4 · pp. 9–10
- Each iteration finds a fresh safe permissive scheduler, learns its cost-minimizing compliant scheduler, updates costs, and compares its cost with a lower bound.The search stops when the cost is below κ, global optimality is established, or no further permissive scheduler can be found; in the worst case it enumerates all safe schedulers.Source: §4 · pp. 10–11
- The procedure is sound and complete because it ultimately iterates over all safe permissive schedulers, thereby covering all possible safe schedulers.Source: §4 · p. 11
4.1 Computing permissive schedulers
- The SMT encoding represents allowed actions with Boolean variables and target-reachability probabilities, constraining the initial probability by λ so satisfying assignments induce safe schedulers.Its soundness and completeness are established by matching satisfying assignments with safe deterministic permissive schedulers and vice versa.Source: §4.1 · pp. 11–12
- The Z3 encoding does not maximize permissiveness; MILP alternatives can optimize available choices, but incrementality is crucial, and randomized schedulers require bounding distributions because their possibilities may be infinite.The stated MILP approach cannot be adapted to randomized schedulers because it involves nonlinear constraints.Source: §4.1 · pp. 12–13
4.2 Learning
- Q-learning explores to learn the cost function, using overly optimistic expected rewards to explore broadly while favoring promising regions; exploration and exploitation depend on scheduler construction.Seeking schedulers that retain the currently best-known scheduler may increase exploitation while severely restricting exploration.Source: §4.2 · p. 13
5 Experiments
The prototype was tested on robotic-motion-planning case studies with safety hazards, goals, and substantial nondeterminism. Janitor and FolLine produced tight cost bounds after the first deployment, while the communicating explorer exposed a loose lower bound and solver-performance trade-offs.
Experimental setup
- The prototype used SMT-based permissive-scheduler computation, adding actions successively to seek a locally maximal scheduler across models with many choices and probabilistic branches.The case studies included bad states reachable with some probability and designated goal states.Source: §5 · p. 13
Case studies
- The Janitor task minimizes fuel while avoiding a randomly moving janitor; FolLine trades speed-dependent deviation risk against time or energy.The line-following model must avoid distances from the center exceeding a fixed tolerance.Source: §5 · p. 14
Benchmark results
- Table 1 reports model sizes, safety bounds, optimal performance over safe schedulers, and iteration-by-iteration computation times and cost bounds.The reported model-size measures include states, transitions, and probabilistic branches.Source: §5 · p. 14, Table 1 · p. 15
- Janitor and FolLine yielded tight lower and upper cost bounds after the first deployment, at the cost of higher computational effort.Table 1 reports benchmark results; more elaborate heuristics that limit the search for local maximal permissiveness could reduce per-iteration effort.Source: §5 · pp. 14–15, Table 1 · p. 15
Case studies
- For the communicating explorer, a noncommunicating scheduler produces very low expected costs, leaving a loose lower bound that tighter bounds from multi-objective model checking could improve.The benchmark optimizes circuit energy, including movement and higher communication costs.Source: §5 · pp. 14–15
Lessons learned
- Highly permissive schedulers can select actions in unreachable fragments, producing small reachable state spaces; guidance to ensure reachability drastically decreased solver performance.The authors suggest quantifying permissiveness over actually reachable states.Source: §5 · p. 15
6 Conclusion and future work
The paper presents an iterative approach to synthesizing safe and optimal strategies with random choices, unknown costs, and safety hazards. It reports practical benchmark applicability and identifies earlier optimality proofs and broader stochastic settings as future work.
Conclusion
- The authors present what they describe as the first approach to iteratively computing safe, optimal strategies with random choices, unknown costs, and safety hazards.They report that the method works on practical benchmarks with a high degree of nondeterminism.Source: §6 · p. 15
Future work
- Future work includes using multi-objective model checking to prove optimality at earlier iterations.Source: §6 · p. 16
- Extensions to stochastic two-player games and settings with unknown probability distributions remain prospective directions.Source: §6 · p. 16