Clark School Home UMD

ISR Events Calendar

Event Information

MBSE Colloquium: Marta Kwiakowska, University of Oxford
Monday, October 24, 2016
11:00 a.m.
1146 AV Williams Building
For More Information:

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

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.

Marta Kwiatkowska is Professor of Computing Systems and Fellow of Trinity College, University of Oxford. She led the development of the PRISM model checker (, 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.

This Event is For: Graduate • Undergraduate • Faculty • Post-Docs • Alumni

Browse Events By Calendar

Calendar Home

« Previous Month    Next Month »

September 2017
1 2 w
3 4 5 6 7 8 9 w
10 11 12 13 14 15 16 w
17 18 19 20 21 22 23 w
24 25 26 27 28 29 30 w

Search Events

ISR lecture and seminar series

Distinguished Lecturer Series
Intelligent Automation Inc. Colloquia Series
Microsystems Seminar Series
Lockheed Martin Robotics Seminar Series
Advanced Networks Colloquia Series
Model-Based Systems Engineering Colloquia Series

Submit an event to the ISR calendar Click here

News links

Current news
Search news
News archives