Model checking and strategy synthesis for mobile autonomy: from theory to practice

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 (http://www.prismmodelchecker.org/games/), an extension of the PRISM model checker. The techniques will be illustrated with examples drawn from autonomous driving and smartgrid protocols.