Room 206 (2nd floor, badged access)
6 July 2023 - 14h00
Causal Temporal Reasoning for Markov Decision Processes
by Nicola Paoletti from King's College London
Abstract: Abstract:
We introduce PCFTL (Probabilistic CounterFactual Temporal Logic), a new probabilistic temporal logic for the verification of Markov Decision Processes (MDP). PCFTL is the first to include operators for causal reasoning, allowing us to express interventional and counterfactual queries. Given a path formula phi, an interventional property is concerned with the satisfaction probability of phi if we apply a particular change I to the MDP (e.g., switching to a different policy); a counterfactual allows us to compute, given an observed MDP path tau, what the outcome of phi would have been had we applied I in the past. For its ability to reason about what-if scenarios involving different configurations of the MDP, our approach represents a departure from existing probabilistic temporal logics that can only reason about a fixed system configuration. From a syntactic viewpoint, we introduce a generalized counterfactual operator that subsumes both interventional and counterfactual probabilities as well as the traditional probabilistic operator found in e.g., PCTL. From a semantics viewpoint, our logic is interpreted over a structural causal model translation of the MDP, which gives us a representation amenable to counterfactual reasoning. We evaluate PCFTL in the context of safe reinforcement learning using a benchmark of grid-world models.
Short bio:
Nicola is a Senior Lecturer in the Department of Informatics at King's College London. In 2018-2022, he has been a Lecturer at the Department of Computer Science at Royal Holloway, University of London. Previously, he has been a post-doc at Stony Brook University (USA) and University of Oxford, after an internship at Microsoft Research Cambridge (UK). He obtained his Ph.D. in Information Sciences and Complex Systems from the Universita' di Camerino (Italy).
Nicola's interests are in safety and security assurance of cyber-physical systems, or CPSs, with an emphasis on biomedical applications. His research aims to develop formal analysis methods (verification, control, and synthesis) to design CPSs that are provably correct. With CPSs increasingly incorporating machine-learning components, his work also focuses on data-driven verification of CPSs, whereby formal analysis and principled learning methods come together to provide correctness guarantees and interpretability.
