David Parker

AAAI Conference 2026 Conference Paper

Efficient Solution and Learning of Robust Factored MDPs

• Yannik Schnitzer
• Alessandro Abate
• David Parker

Robust Markov decision processes (r-MDPs) extend MDPs by explicitly modelling epistemic uncertainty about transition dynamics. Learning r-MDPs from interactions with an unknown environment enables the synthesis of robust policies with provable (PAC) guarantees on performance, but this can require a large number of sample interactions. We propose novel methods for solving and learning r-MDPs based on factored state-space representations that leverage the independence between model uncertainty across system components. Although policy synthesis for factored r-MDPs leads to hard, non-convex optimisation problems, we show how to reformulate these into tractable linear programs. Building on these, we also propose methods to learn factored model representations directly. Our experimental results show that exploiting factored structure can yield dimensional gains in sample efficiency, producing more effective robust policies with tighter performance guarantees than state-of-the-art methods.

TACAS Conference 2026 Conference Paper

Robust Verification of Concurrent Stochastic Games

• Angel Y. He
• David Parker

TAAS Journal 2024 Journal Article

A Framework for Simultaneous Task Allocation and Planning under Uncertainty

• Fatma Faruq
• Bruno Lacerda
• Nick Hawes
• David Parker

We present novel techniques for simultaneous task allocation and planning in multi-robot systems operating under uncertainty. By performing task allocation and planning simultaneously, allocations are informed by individual robot behaviour, creating more efficient team behaviour. We go beyond existing work by planning for task reallocation across the team given a model of partial task satisfaction under potential robot failures and uncertain action outcomes. We model the problem using Markov decision processes, with tasks encoded in co-safe linear temporal logic, and optimise for the expected number of tasks completed by the team. To avoid the inherent complexity of joint models, we propose an alternative model that simultaneously considers task allocation and planning, but in a sequential fashion. We then build a joint policy from the sequential policy obtained from our model, thus allowing for concurrent policy execution. Furthermore, to enable adaptation in the case of robot failures, we consider replanning from failure states and propose an approach to preemptively replan in an anytime fashion, replanning for more probable failure states first. Our method also allows us to quantify the performance of the team by providing an analysis of properties, such as the expected number of completed tasks under concurrent policy execution. We implement and extensively evaluate our approach on a range of scenarios. We compare its performance to a state-of-the-art baseline in decoupled task allocation and planning: sequential single-item auctions. Our approach outperforms the baseline in terms of computation time and the number of times replanning is required on robot failure.

I&C Journal 2024 Journal Article

Strategy synthesis for zero-sum neuro-symbolic concurrent stochastic games

• Rui Yan
• Gabriel Santos
• Gethin Norman
• David Parker
• Marta Kwiatkowska

Neuro-symbolic approaches to artificial intelligence, which combine neural networks with classical symbolic techniques, are growing in prominence, necessitating formal approaches to reason about their correctness. We propose a novel modelling formalism called neuro-symbolic concurrent stochastic games (NS-CSGs), which comprise two probabilistic finite-state agents interacting in a shared continuous-state environment. Each agent observes the environment using a neural perception mechanism, which converts inputs such as images into symbolic percepts, and makes decisions symbolically. We focus on the class of NS-CSGs with Borel state spaces and prove the existence and measurability of the value function for zero-sum discounted cumulative rewards under piecewise-constant restrictions. To compute values and synthesise strategies, we first introduce a Borel measurable piecewise-constant (B-PWC) representation of value functions and propose a B-PWC value iteration. Second, we introduce two novel representations for the value functions and strategies, and propose a minimax-action-free policy iteration based on alternating player choices.

JAIR Journal 2023 Journal Article

Robust Control for Dynamical Systems with Non-Gaussian Noise via Formal Abstractions

• Thom Badings
• Licio Romao
• Alessandro Abate
• David Parker
• Hasan A. Poonawala
• Marielle Stoelinga
• Nils Jansen

Controllers for dynamical systems that operate in safety-critical settings must account for stochastic disturbances. Such disturbances are often modeled as process noise in a dynamical system, and common assumptions are that the underlying distributions are known and/or Gaussian. In practice, however, these assumptions may be unrealistic and can lead to poor approximations of the true noise distribution. We present a novel controller synthesis method that does not rely on any explicit representation of the noise distributions. In particular, we address the problem of computing a controller that provides probabilistic guarantees on safely reaching a target, while also avoiding unsafe regions of the state space. First, we abstract the continuous control system into a finite-state model that captures noise by probabilistic transitions between discrete states. As a key contribution, we adapt tools from the scenario approach to compute probably approximately correct (PAC) bounds on these transition probabilities, based on a finite number of samples of the noise. We capture these bounds in the transition probability intervals of a so-called interval Markov decision process (iMDP). This iMDP is, with a user-specified confidence probability, robust against uncertainty in the transition probabilities, and the tightness of the probability intervals can be controlled through the number of samples. We use state-of-the-art verification techniques to provide guarantees on the iMDP and compute a controller for which these guarantees carry over to the original control system. In addition, we develop a tailored computational scheme that reduces the complexity of the synthesis of these guarantees on the iMDP. Benchmarks on realistic control systems show the practical applicability of our method, even when the iMDP has hundreds of millions of transitions.

NeurIPS Conference 2022 Conference Paper

Robust Anytime Learning of Markov Decision Processes

• Marnix Suilen
• Thiago D. Simão
• David Parker
• Nils Jansen

Markov decision processes (MDPs) are formal models commonly used in sequential decision-making. MDPs capture the stochasticity that may arise, for instance, from imprecise actuators via probabilities in the transition function. However, in data-driven applications, deriving precise probabilities from (limited) data introduces statistical errors that may lead to unexpected or undesirable outcomes. Uncertain MDPs (uMDPs) do not require precise probabilities but instead use so-called uncertainty sets in the transitions, accounting for such limited data. Tools from the formal verification community efficiently compute robust policies that provably adhere to formal specifications, like safety constraints, under the worst-case instance in the uncertainty set. We continuously learn the transition probabilities of an MDP in a robust anytime-learning approach that combines a dedicated Bayesian inference scheme with the computation of robust policies. In particular, our method (1) approximates probabilities as intervals, (2) adapts to new data that may be inconsistent with an intermediate model, and (3) may be stopped at any time to compute a robust policy on the uMDP that faithfully captures the data so far. Furthermore, our method is capable of adapting to changes in the environment. We show the effectiveness of our approach and compare it to robust policies computed on uMDPs learned by the UCRL2 reinforcement learning algorithm in an experimental evaluation on several benchmarks.

AAAI Conference 2022 Conference Paper

Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise

• Thom S. Badings
• Alessandro Abate
• Nils Jansen
• David Parker
• Hasan A. Poonawala
• Marielle Stoelinga

Controllers for autonomous systems that operate in safetycritical settings must account for stochastic disturbances. Such disturbances are often modeled as process noise, and common assumptions are that the underlying distributions are known and/or Gaussian. In practice, however, these assumptions may be unrealistic and can lead to poor approximations of the true noise distribution. We present a novel planning method that does not rely on any explicit representation of the noise distributions. In particular, we address the problem of computing a controller that provides probabilistic guarantees on safely reaching a target. First, we abstract the continuous system into a discrete-state model that captures noise by probabilistic transitions between states. As a key contribution, we adapt tools from the scenario approach to compute probably approximately correct (PAC) bounds on these transition probabilities, based on a finite number of samples of the noise. We capture these bounds in the transition probability intervals of a socalled interval Markov decision process (iMDP). This iMDP is robust against uncertainty in the transition probabilities, and the tightness of the probability intervals can be controlled through the number of samples. We use state-of-the-art verification techniques to provide guarantees on the iMDP, and compute a controller for which these guarantees carry over to the autonomous system. Realistic benchmarks show the practical applicability of our method, even when the iMDP has millions of states or transitions.

IJCAI Conference 2021 Conference Paper

Verifying Reinforcement Learning up to Infinity

• Edoardo Bacci
• Mirco Giacobbe
• David Parker

Formally verifying that reinforcement learning systems act safely is increasingly important, but existing methods only verify over finite time. This is of limited use for dynamical systems that run indefinitely. We introduce the first method for verifying the time-unbounded safety of neural networks controlling dynamical systems. We develop a novel abstract interpretation method which, by constructing adaptable template-based polyhedra using MILP and interval arithmetic, yields sound---safe and invariant---overapproximations of the reach set. This provides stronger safety guarantees than previous time-bounded methods and shows whether the agent has generalised beyond the length of its training episodes. Our method supports ReLU activation functions and systems with linear, piecewise linear and non-linear dynamics defined with polynomial and transcendental functions. We demonstrate its efficacy on a range of benchmark control problems.

Highlights Conference 2018 Conference Abstract

Probabilistic Model Checking: Advances and Applications

• David Parker

ABSTRACT. Probabilistic model checking is a technique for formally verifying quantitative properties of systems that exhibit stochastic behavior. It can provide formal guarantees on a wide range of system properties, such as safety, reliability, energy efficiency or security, and can be used to investigate trade-offs between them. This talk will give an overview of the probabilistic model checking tool PRISM, and describe some of the current advances being made in its development. This includes techniques for controller synthesis and multi-objective verification, as well as support for new probabilistic models such as stochastic games and partially observable Markov decision processes. These will be illustrated with applications from various domains including robotics, energy management and task scheduling.

IJCAI Conference 2015 Conference Paper

Optimal Policy Generation for Partially Satisfiable Co-Safe LTL Specifications

• Bruno Lacerda
• David Parker
• Nick Hawes

We present a method to calculate cost-optimal policies for task specifications in co-safe linear temporal logic over a Markov decision process model of a stochastic system. Our key contribution is to address scenarios in which the task may not be achievable with probability one. We formalise a task progression metric and, using multi-objective probabilistic model checking, generate policies that are formally guaranteed to, in decreasing order of priority: maximise the probability of finishing the task; maximise progress towards completion, if this is not possible; and minimise the expected time or cost required. We illustrate and evaluate our approach in a robot task planning scenario, where the task is to visit a set of rooms that may be inaccessible during execution.

TCS Journal 2014 Journal Article

Local abstraction refinement for probabilistic timed programs

• Klaus Dräger
• Marta Kwiatkowska
• David Parker
• Hongyang Qu

We consider models of programs that incorporate probability, dense real-time and data. We present a new abstraction refinement method for computing minimum and maximum reachability probabilities for such models. Our approach uses strictly local refinement steps to reduce both the size of abstractions generated and the complexity of operations needed, in comparison to previous approaches of this kind. We implement the techniques and evaluate them on a selection of large case studies, including some infinite-state probabilistic real-time models, demonstrating improvements over existing tools in several cases.

I&C Journal 2013 Journal Article

Compositional probabilistic verification through multi-objective model checking

• Marta Kwiatkowska
• Gethin Norman
• David Parker
• Hongyang Qu

Compositional approaches to verification offer a powerful means to address the challenge of scalability. In this paper, we develop techniques for compositional verification of probabilistic systems based on the assume-guarantee paradigm. We target systems that exhibit both nondeterministic and stochastic behaviour, modelled as probabilistic automata, and augment these models with costs or rewards to reason about, for example, energy usage or performance metrics. Despite significant theoretical advances in compositional reasoning for probabilistic automata, there has been a distinct lack of practical progress regarding automated verification. We propose a new assume-guarantee framework based on multi-objective probabilistic model checking which supports compositional verification for a range of quantitative properties, including probabilistic ω-regular specifications and expected total cost or reward measures. We present a wide selection of assume-guarantee proof rules, including asymmetric, circular and asynchronous variants, and also show how to obtain numerical results in a compositional fashion. Given appropriate assumptions to be used in the proof rules, our compositional verification methods are, in contrast to previously proposed approaches, efficient and fully automated. Experimental results demonstrate their practical applicability on several large case studies, including instances where conventional probabilistic verification is infeasible.

TCS Journal 2009 Journal Article

Probabilistic Mobile Ambients

• Marta Kwiatkowska
• Gethin Norman
• David Parker
• Maria Grazia Vigliotti

The calculus of Mobile Ambients has been introduced for expressing mobility and mobile computation. In this paper we present a probabilistic version of Mobile Ambients by augmenting the syntax of the original Ambient Calculus with a (guarded) probabilistic choice operator. To allow for the representation of both the probabilistic behaviour introduced through the new probabilistic choice operator and the nondeterminism present in the original Ambient Calculus we use probabilistic automata as the underpinning semantic model. The Ambient logic is a logic for Mobile Ambients that contains a novel treatment of both locations and hidden names. For specifying properties of Probabilistic Mobile Ambients, we extend this logic to specify probabilistic behaviour. In addition, to show the utility of our approach we present an example of a virus infecting a network.

TCS Journal 2008 Journal Article

Probabilistic model checking of complex biological pathways

• John Heath
• Marta Kwiatkowska
• Gethin Norman
• David Parker
• Oksana Tymchyshyn

Probabilistic model checking is a formal verification technique that has been successfully applied to the analysis of systems from a broad range of domains, including security and communication protocols, distributed algorithms and power management. In this paper we illustrate its applicability to a complex biological system: the FGF (Fibroblast Growth Factor) signalling pathway. We give a detailed description of how this case study can be modelled in the probabilistic model checker PRISM, discussing some of the issues that arise in doing so, and show how we can thus examine a rich selection of quantitative properties of this model. We present experimental results for the case study under several different scenarios and provide a detailed analysis, illustrating how this approach can be used to yield a better understanding of the dynamics of the pathway. Finally, we outline a number of exact and approximate techniques to enable the verification of larger and more complex pathways and apply several of them to the FGF case study.

NeurIPS Conference 1988 Conference Paper

Learning with Temporal Derivatives in Pulse-Coded Neuronal Systems

• David Parker
• Mark Gluck
• Eric Reifsnider

A number of learning models have recently been proposed which involve calculations of temporal differences (or derivatives in continuous-time models). These models. like most adaptive network models. are formulated in tenns of frequency (or activation), a useful abstraction of neuronal firing rates. To more precisely evaluate the implications of a neuronal model. it may be preferable to develop a model which transmits discrete pulse-coded information. We point out that many functions and properties of neuronal processing and learning may depend. in subtle ways. on the pulse-coded nature of the informa(cid: 173) tion coding and transmission properties of neuron systems. When com(cid: 173) pared to formulations in terms of activation. computing with temporal derivatives (or differences) as proposed by Kosko (1986). Klopf (1988). and Sutton (1988). is both more stable and easier when refor(cid: 173) mulated for a more neuronally realistic pulse-coded system. In refor(cid: 173) mulating these models in terms of pulse-coding. our motivation has been to enable us to draw further parallels and connections between real-time behavioral models of learning and biological circuit models of the substrates underlying learning and memory.