# Permissive Controller Synthesis for Probabilistic Systems

arXiv: https://arxiv.org/abs/1504.04662 · HTML: https://mlsanity.com/paper/1504.04662/

## Key facts

- Cited by 17 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 18 Apr 2015.

## Built on by (most cited first, 17 of 17)

- [Safe Reinforcement Learning via Shielding under Partial Observability](https://mlsanity.com/paper/2204.00755/) (2022)
- [COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking](https://mlsanity.com/paper/2209.07133/) (2022)
- [Targeted Adversarial Attacks on Deep Reinforcement Learning Policies via Model Checking](https://mlsanity.com/paper/2212.05337/) (2022)
- [Probabilistic Model Checking of Stochastic Reinforcement Learning Policies](https://mlsanity.com/paper/2403.18725/) (2024)
- [Shielding in Resource-Constrained Goal POMDPs](https://mlsanity.com/paper/2211.15349/) (2022)
- [Formally Verifying and Explaining Sepsis Treatment Policies with COOL-MC](https://mlsanity.com/paper/2602.14505/) (2026)
- [Co-Activation Graph Analysis of Safety-Verified and Explainable Deep Reinforcement Learning Policies](https://mlsanity.com/paper/2501.03142/) (2025)
- [Compositional shield synthesis for safe reinforcement learning in partial observability](https://mlsanity.com/paper/2509.12085/) (2025)
- [Robust Probabilistic Shielding for Safe Offline Reinforcement Learning](https://mlsanity.com/paper/2605.10293/) (2026)
- [Shields to Guarantee Probabilistic Safety in MDPs](https://mlsanity.com/paper/2605.10888/) (2026)
- [Multi-Objective Controller Synthesis with Uncertain Human Preferences](https://mlsanity.com/paper/2105.04662/) (2021)
- [Deductive Controller Synthesis for Probabilistic Hyperproperties](https://mlsanity.com/paper/2307.04503/) (2023)
- [Formal Verification of Noisy Quantum Reinforcement Learning Policies](https://mlsanity.com/paper/2512.01502/) (2025)
- [Translating the Rashomon Effect to Sequential Decision-Making Tasks](https://mlsanity.com/paper/2512.17470/) (2025)
- [COOL-MC: Verifying and Explaining RL Policies for Platelet Inventory Management](https://mlsanity.com/paper/2603.02396/) (2026)
- [COOL-MC: Verifying and Explaining RL Policies for Multi-bridge Network Maintenance](https://mlsanity.com/paper/2603.07546/) (2026)
- [Sample-Efficient Learning of Probabilistic Causes for Reachability in Markov Decision Processes with Probabilistic Guarantees](https://mlsanity.com/paper/2606.29681/) (2026)

## Abstract (arXiv)

We propose novel controller synthesis techniques for probabilistic systems modelled using stochastic two-player games: one player acts as a controller, the second represents its environment, and probability is used to capture uncertainty arising due to, for example, unreliable sensors or faulty system components. Our aim is to generate robust controllers that are resilient to unexpected system changes at runtime, and flexible enough to be adapted if additional constraints need to be imposed. We develop a permissive controller synthesis framework, which generates multi-strategies for the controller, offering a choice of control actions to take at each time step. We formalise the notion of permissivity using penalties, which are incurred each time a possible control action is disallowed by a multi-strategy. Permissive controller synthesis aims to generate a multi-strategy that minimises these penalties, whilst guaranteeing the satisfaction of a specified system property. We establish several key results about the optimality of multi-strategies and the complexity of synthesising them. Then, we develop methods to perform permissive controller synthesis using mixed integer linear programming and illustrate their effectiveness on a selection of case studies.