Book section
Verification and control of turn-based probabilistic real-time games
- Abstract:
- 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.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Accepted manuscript, pdf, 826.9KB, Terms of use)
-
- Publisher copy:
- 10.1007/978-3-030-31175-9_22
Authors
Contributors
+ Alvim, MS
- Role:
- Editor
+ Chatzikokolakis, K
- Role:
- Editor
+ Olarte, C
- Role:
- Editor
+ Valencia, F
- Role:
- Editor
+ Engineering and Physical Sciences Research Council
More from this funder
- Funder identifier:
- https://ror.org/0439y7842
- Grant:
- EP/M019918/1
- Publisher:
- Springer Verlag
- Host title:
- The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday
- Pages:
- 379-396
- Series:
- Lecture Notes in Computer Science
- Series number:
- 11760
- Publication date:
- 2019-11-04
- Acceptance date:
- 2019-06-12
- DOI:
- EISSN:
-
1611-3349
- ISSN:
-
0302-9743
- EISBN:
- 9783030311759
- ISBN:
- 9783030311742
- Language:
-
English
- Pubs id:
-
pubs:1031914
- UUID:
-
uuid:071082e8-71d7-4e4b-81ef-73f36e56fa82
- Local pid:
-
pubs:1031914
- Source identifiers:
-
1031914
- Deposit date:
-
2019-07-28
Terms of use
- Copyright holder:
- Springer Nature Switzerland AG
- Copyright date:
- 2019
- Rights statement:
- © Springer Nature Switzerland AG 2019
- Notes:
- This is the accepted manuscript version of the chapter. The final version is available online from Springer Verlag at https://dx.doi.org/10.1007/978-3-030-31175-9_22
If you are the owner of this record, you can report an update to it here: Report update to this record