Verification and control of turn-based probabilistic real-time games

Marta Kwiatkowska, Gethin Norman, David Parker

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)
167 Downloads (Pure)


Quantitative verification techniques have been developed for the formal analysis of a variety of probabilistic models, such as Markov chains, Markov decision process and their variants. They can be used to produce guarantees on quantitative aspects of system behaviour, for example safety, reliability and performance, or to help synthesise controllers that ensure such guarantees are met.We propose the model of turn-based probabilistic timed multi-player games, which incorporates probabilistic choice, real-time clocks and nondeterministic behaviour across multiple players. Building on the digital clocks approach for the simpler model of probabilistic timed automata, we show how to compute the key measures that underlie quantitative verification, namely the probability and expected cumulative price to reach a target. We illustrate this on case studies from computer security and task scheduling.
Original languageEnglish
Title of host publicationThe Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy
Subtitle of host publicationEssays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday
EditorsM. Alvim, K. Chatzikokolakis, C. Olarte, F. Valencia
Number of pages16
ISBN (Electronic)9783030311759
ISBN (Print)9783030311742
Publication statusPublished - 4 Nov 2019

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Verification and control of turn-based probabilistic real-time games'. Together they form a unique fingerprint.

Cite this