Event
MBSE Colloquium: Marta Kwiakowska, University of Oxford
Monday, October 24, 2016
11:00 a.m.
1146 AV Williams Building
Model checking and strategy synthesis for mobile autonomy: from theory to practice
Marta Kwiakowska
Professor of Computing Systems and Fellow of Trinity College
University of Oxford
Abstract
Design of autonomous systems is facilitated by automatic verification and synthesis of controllers from temporal logic objectives. If components that cannot be controlled are present in the environment, it is natural to view such systems as games between the controllable computer system (Player 1) and its (uncontrollable) environment (Player 2). When, additionally, stochastic uncertainty is present, e.g., due to unreliable communication media or faulty components, we need to consider stochastic games. Examples of such systems appear in many domains, from robotics and autonomous transport, to networked and distributed systems. To specify objectives, we work with probabilistic extensions of temporal logic, which can reason about the probability or expectation of an event. Given a stochastic game and a probabilistic temporal logic property, verification and strategy synthesis problems, respectively, focus on the existence and construction of a winning strategy for Player 1 that guarantees satisfaction of the property against all strategies of Player 2.
This lecture will give a high-level overview of recent advances in verification and strategy synthesis for turn-based stochastic games with single and multiple objectives implemented in PRISM-games, an extension of the PRISM model checker. The techniques will be illustrated with examples drawn from autonomous driving and smartgrid protocols.
Biography
Marta Kwiatkowska is Professor of Computing Systems and Fellow of Trinity College, University of Oxford. She led the development of the PRISM model checker (www.prismmodelchecker.org), the leading software tool in the area, winner of the HVC Award 2016, and widely used for research and teaching. Applications of probabilistic model checking have spanned communication and security protocols, nanotechnology designs, power management, game theory, planning and systems biology, with genuine flaws found and corrected in real-world protocols. Kwiatkowska gave the Milner Lecture in 2012 in recognition of "excellent and original theoretical work which has a perceived significance for practical computing" and was awarded an honorary doctorate from KTH Royal Institute of Technology in Stockholm in 2014. Her research is supported by the ERC Advanced Grant VERIWARE "From software verification to everyware verification" and the EPSRC Programme Grant in Mobile Autonomy.
