Function 2021

Preliminary Program (all times CEST)

Titles and abstracts

Matthijs Spaan

Safety in Online and Offline Reinforcement Learning

Abstract: Safety is a paramount issue for the application of reinforcement learning algorithms in the real world. We investigate safety from two perspectives, one where a reasonable performance must be ensured and another where safety constraints cannot be violated. In the first, the reinforcement learning agent only has access to a fix dataset of past trajectories and does not interact directly with the environment. Assuming the behavior policy that collected the data is available, the challenge is to compute a policy that outperforms the behavior policy. In this setting, we develop sample-efficient algorithms by exploiting the structure of the problem. In the second, the agent is trained by interacting directly with the environment, however there are safety constraints. Therefore, the agent cannot perform random exploration, which is typical in online reinforcement learning algorithms. Assuming the agent has access to an abstraction of the safety dynamics, we develop algorithms that can safely explore the environment and eventually converge to an optimal policy.

Wolfram Wiesemann

Optimal Hospital Care Scheduling During the SARS-CoV-2 Pandemic

Abstract: The COVID-19 pandemic has seen dramatic demand surges for hospital care that have placed a severe strain on health systems worldwide. As a result, policy makers are faced with the challenge of managing scarce hospital capacity so as to reduce the backlog of non-COVID patients whilst maintaining the ability to respond to any potential future increases in demand for COVID care. In this talk, we propose a nation-wide prioritization scheme that models each individual patient as a dynamic program whose states encode the patient’s health and treatment condition, whose actions describe the available treatment options, whose transition probabilities characterize the stochastic evolution of the patient’s health and whose rewards encode the contribution to the overall objectives of the health system. The individual patients’ dynamic programs are coupled through constraints on the available resources, such as hospital beds, doctors and nurses. We show that near-optimal solutions to the emerging weakly coupled counting dynamic program can be found through a fluid approximation that gives rise to a linear program whose size grows gracefully in the problem dimensions. Our case study for the National Health Service in England shows how years of life can be gained and costs reduced by prioritizing specific disease types over COVID patients, such as injury & poisoning, diseases of the respiratory system, diseases of the circulatory system, diseases of the digestive system and cancer.

Bruno Lacerda

Mission Planning for Robots in Partially Unknown Environments

Abstract: Robust mission planning algorithms for autonomous robots typically require explicit reasoning about the inherent uncertainty of environmental features. For example, service robots need to consider the behaviour of humans around them; autonomous underwater vehicles require models of underwater currents; and robots in a multi-robot system need to reason about how interaction with other robots can affect their performance. Oftentimes, these environmental features cannot be fully modelled before the system is deployed, and an open challenge in robotics is finding principled solutions that allow for robust deployments in such partially unknown environments. In this talk, I will describe our recent work on robust planning via regret minimisation of uncertain Markov decision processes (MDPs), an extension of MDPs where the transition and reward functions are not fully known. Then, assuming the robot is equipped with a sensor that can provide observations of the a priori unknown environmental features, I will describe our work on incorporating Gaussian processes with online MDP planning to enable robot deployments in partially unknown environments.

Ahmadreza Marandi

Disjoint Bilinear Optimization: A Two-stage Robust Optimization Perspective

Abstract: In this talk, we focus on a subclass of quadratic optimization problems, that is, disjoint bilinear optimization problems. We first show that disjoint bilinear optimization problems can be cast as two-stage robust linear optimization problems with fixed-recourse and right-hand-side uncertainty, which enables us to apply robust optimization techniques to solve the resulting problems. To this end, a solution scheme based on a blending of three popular robust optimization techniques is proposed. For disjoint bilinear optimization problems with a polyhedral feasible region and a general convex feasible region, we show that under mild regularity conditions, the convex relaxations of the original bilinear formulation and its two-stage robust reformulation obtained from a reformulation-linearization based technique and linear decision rules, respectively, are equivalent. For generic bilinear optimization problems, the convex relaxations from the reformulation-linearization based technique are generally tighter than the one from linear decision rules. Numerical experiments on bimatrix games and synthetic disjoint bilinear problem instances show the efficiency and effectiveness of the proposed solution scheme.

Radu Calinescu

Probabilistic model checking: Where do the transition probabilities and rates of Markov models come from?

Abstract: Probabilistic model checking is a powerful tool for establishing performance, dependability and other key properties of systems during design, verification, and at runtime. However, the usefulness of this tool depends on the accuracy of the Markov models being verified. In this talk, I will describe recent advances in exploiting data (available from offline testing, system logs, or runtime monitoring) to ensure that these models and their verification results are sufficiently accurate to support correct decision-making under epistemic uncertainty.

Rayna Dimitrova

Probabilistic Hyperproperties of Markov Decision Processes

Abstract: Trace properties, which are sets of execution traces, have been extensively used for specifying and reasoning about the correctness of systems. Trace properties, however, cannot describe information-flow security requirements, like noninterference, or important requirements relevant in the presence of uncertainty, like partial observation and robustness. Hyperproperties generalize trace properties and are capable of describing requirements that relate multiple system executions. Over the past decade, a rich set of temporal logics for the specification of hyperproperties and techniques for reasoning about them have been developed. In this talk I will present a recently introduced temporal logic for the specification of hyperproperties of Markov decision processes (MDPs), called Probabilistic Hyper Logic (PHL). PHL extends classic probabilistic logics with quantification over schedulers and traces. It can express a wide range of hyperproperties for probabilistic systems, including both classical applications, such as probabilistic noninterference and differential privacy, as well as novel applications in areas such as planning. A consequence of the generality of the logic is that the model checking problem for PHL is undecidable. I will present methods both for proving and for refuting formulas from a fragment of the logic that includes many probabilistic hyperproperties of interest. I will discuss how probabilistic hyperproperties can be used to specify and reason about the effects of uncertainty. This talk is based on joint work with Bernd Finkbeiner and Hazem Torfah.

Rob Basten

Achieving low downtime of high-tech systems with uncertain failure behaviour

Abstract: High-tech systems, such as wafer steppers, baggage handling systems or industrial printers, are expensive and complex. This means that their users do not typically invest in redundancy and thus require low downtime and high reliability. At the same time, it is very hard to predict when something in the system may fail, and what will fail. This means that it is hard to determine when to perform preventive maintenance to prevent failures from occurring, and which spare parts to stock to quickly perform corrective maintenance after a failure has occurred. We will discuss the challenges in maintenance optimization and spare parts inventory control and we will see how the research in operations management and industrial engineering is moving from assuming known failure behaviour to acknowledging that it may not even be clear what type of distribution fits the failure behaviour of the components in the system. It will become clear that if we want to increase our impact in practice, much (joint) research is required from researchers in operations management, industrial engineering, and computer science.

Tim Quatmann

Markov Models with Multiple Long-run Average and Total Reward Objectives

Abstract: We present an efficient procedure for multi-objective model checking of long-run average (LRA) reward and total reward objectives as well as their combination. We consider this for Markov automata (MAs), a compositional model that captures both traditional Markov decision processes (MDPs) as well as a continuous-time variant thereof. Our approach thus allows us to study tradeoffs between potentially conflicting objectives of systems involving controlled- and randomized decisions as well as random timings given by exponential distributions.

Marcell Vazquez-Chanlatte, Sebastian Junges, Daniel J. Fremont and Sanjit A. Seshia

Entropy-Guided Control Improvisation

Abstract: High level declarative constraints provide a powerful (and popular) way to define and construct control policies; however, most synthesis algorithms do not support specifying the degree of randomness (unpredictability) of the resulting controller. In many contexts, e.g., patrolling, testing, behavior prediction,and planning on idealized models, predictable or biased controllers are undesirable. To address these concerns, we introduce the Entropic Reactive Control Improvisation (ERCI) framework and algorithm which supports synthesizing control policies for stochastic games that are declaratively specified by (i) a \emph{hard constraint} specifying what must occur, (ii) a \emph{soft constraint} specifying what typically occurs, and (iii) a randomization constraint specifying the unpredictability and variety of the controller, as quantified using causal entropy. This framework, extends the state of the art by supporting arbitrary combinations of adversarial and probabilistic uncertainty in the environment. ERCI enables a flexible modeling formalism which we argue, theoretically and empirically, remains tractable.

Marnix Suilen

Robust Policies for Uncertain POMDPs

Abstract: We study the problem of computing robust finite-memory policies for uncertain partially observable Markov decision processes (POMDPs). Uncertain POMDPs (uPOMDPs) form an extension of the standard POMDP model where the transition or observation probabilities are not exactly known, but given by an uncertainty set, like intervals of probabilities or likelihood functions. Such uncertainty sets can, for instance, account for sensor imprecisions or human behavior. We include such uncertainties in the decision-making by computing finite-memory policies that satisfy a reachability or expected reward specification under the worst-case instance of the uncertainty in the model. Experiments show that our method based on convex optimization is feasible for uPOMDPs of several hundreds of thousands of states. We show the applicability of our approach on the example case study of spacecraft motion planning.

Rania Taleb, Raphael Khoury and Sylvain Hallé

Runtime Verification Under Access Control Restrictions

Abstract: We define a logical framework that permits runtime verification to take place when a monitor has incomplete or uncertain information about the underlying trace. Uncertainty is modeled as a stateful access control proxy that has the capacity to turn events into sets of possible events, resulting in what we call a “multi-trace”. We describe a model of both proxy and monitor as extensions of Mealy machines, and provide an algorithm to lift a classical monitor into a sound, loss-tolerant monitor. Experiments on various scenarios show that the approach can account for various types of data degradation and access limitations, provides a tighter verdict than existing works in some cases.

Morteza Lahijanian

Data-driven Synthesis for Partially-known Stochastic Systems

Abstract: Cyber-physical systems (CPS) are widely used in our society, from smart grids to autonomous cars. They are rapidly gaining more capabilities via AI components and serving in ever more safety-critical roles. However, as their complexities grow, the more uncertain their models become, and hence, the more difficult it becomes to provide safety guarantees for their performance. In this talk, I argue that formal methods combined with machine learning techniques can form powerful tools to address this problem. To this end, I present a data-driven framework for correct-by-construction control synthesis for partially-known stochastic CPS. The framework takes a set of input-output data and a temporal logic specification as input and returns a control strategy under which the system is guaranteed to satisfy the specification. Underlying this approach is a finite abstraction paradigm that leverages Gaussian process regression and uncertain Markov processes. The abstraction accounts for both the stochastic behavior of the system and the uncertainty in the regression step. Then, using automaton-based reasoning and optimization techniques, a control strategy is synthesized that maximizes the satisfaction probability of the specification and is robust against all the uncertainties in the abstraction. I show that this strategy is near-optimal and provide a bound on its distance (error) to the optimal controller. I also present a series of case studies, including both (unknown) linear and non-linear switched stochastic systems, which validate the theoretical results.

Ransalu Senanayake

Knowing the unknown unknowns in learning-based systems

Abstract: Autonomous agents have already gained the capability to perform individual tasks such as object detection and lane following, especially in simple, static environments. However, for robots to safely operate in the real-world, it is vital for them to quantify the uncertainty around them. In this talk, I will talk about how we can leverage tools from approximate Bayesian inference to estimate multimodal aleatoric and epistemic uncertainty in various learning-based systems with applications to robot perception and autonomous driving.
Bio: Ransalu Senanayake is a postdoctoral research scholar in Artificial Intelligence at the Stanford Intelligent Systems Laboratory, Stanford University. He is also a member of the Stanford Center for AI Safety and the SAIL-Toyota Center for AI Research. Prior to joining Stanford, Ransalu obtained a PhD in Computer Science from the University of Sydney in 2019, an MPhil in Industrial Engineering and Decision Analytics from the Hong Kong University of Science and Technology in 2013, and a BEng Honours in Electronic Engineering from the Sheffield Hallam University in 2011. He is an Associate Editor for the IEEE International Conference on Intelligent Robots and Systems (IROS) in 2021.