Verification and control of turn-based probabilistic real-time games
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, reliabilit...
| Main Authors: | , , |
|---|---|
| Format: | Conference item |
| Published: |
Springer Verlag
2019
|
| _version_ | 1826257764121313280 |
|---|---|
| author | Kwiatkowska, M Norman, G Parker, D |
| author_facet | Kwiatkowska, M Norman, G Parker, D |
| author_sort | Kwiatkowska, M |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-06T18:23:20Z |
| format | Conference item |
| id | oxford-uuid:071082e8-71d7-4e4b-81ef-73f36e56fa82 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T18:23:20Z |
| publishDate | 2019 |
| publisher | Springer Verlag |
| record_format | dspace |
| spelling | oxford-uuid:071082e8-71d7-4e4b-81ef-73f36e56fa822022-03-26T09:05:41ZVerification and control of turn-based probabilistic real-time gamesConference itemhttp://purl.org/coar/resource_type/c_5794uuid:071082e8-71d7-4e4b-81ef-73f36e56fa82Symplectic Elements at OxfordSpringer Verlag2019Kwiatkowska, MNorman, GParker, DQuantitative 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. |
| spellingShingle | Kwiatkowska, M Norman, G Parker, D Verification and control of turn-based probabilistic real-time games |
| title | Verification and control of turn-based probabilistic real-time games |
| title_full | Verification and control of turn-based probabilistic real-time games |
| title_fullStr | Verification and control of turn-based probabilistic real-time games |
| title_full_unstemmed | Verification and control of turn-based probabilistic real-time games |
| title_short | Verification and control of turn-based probabilistic real-time games |
| title_sort | verification and control of turn based probabilistic real time games |
| work_keys_str_mv | AT kwiatkowskam verificationandcontrolofturnbasedprobabilisticrealtimegames AT normang verificationandcontrolofturnbasedprobabilisticrealtimegames AT parkerd verificationandcontrolofturnbasedprobabilisticrealtimegames |