Automatic Verification of Competitive Stochastic Systems.
We present automatic verification techniques for the modelling and analysis of probabilistic systems that incorporate competitive behaviour. These systems are modelled as turn-based stochastic multi-player games, in which the players can either collaborate or compete in order to achieve a particular...
| Main Authors: | , , , , |
|---|---|
| Other Authors: | |
| Format: | Journal article |
| Language: | English |
| Published: |
Springer
2012
|
| _version_ | 1826304633847414784 |
|---|---|
| author | Chen, T Forejt, V Kwiatkowska, M Parker, D Simaitis, A |
| author2 | Flanagan, C |
| author_facet | Flanagan, C Chen, T Forejt, V Kwiatkowska, M Parker, D Simaitis, A |
| author_sort | Chen, T |
| collection | OXFORD |
| description | We present automatic verification techniques for the modelling and analysis of probabilistic systems that incorporate competitive behaviour. These systems are modelled as turn-based stochastic multi-player games, in which the players can either collaborate or compete in order to achieve a particular goal. We define a temporal logic called rPATL for expressing quantitative properties of stochastic multi-player games. This logic allows us to reason about the collective ability of a set of players to achieve a goal relating to the probability of an event's occurrence or the expected amount of cost/reward accumulated. We give a model checking algorithm for verifying properties expressed in this logic and implement the techniques in a probabilistic model checker, based on the PRISM tool. We demonstrate the applicability and efficiency of our methods by deploying them to analyse and detect potential weaknesses in a variety of large case studies, including algorithms for energy management and collective decision making for autonomous systems. © 2012 Springer-Verlag Berlin Heidelberg. |
| first_indexed | 2024-03-07T06:20:46Z |
| format | Journal article |
| id | oxford-uuid:f2a4233a-2ac2-4f63-a3d4-102e6e135efc |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T06:20:46Z |
| publishDate | 2012 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:f2a4233a-2ac2-4f63-a3d4-102e6e135efc2022-03-27T12:05:28ZAutomatic Verification of Competitive Stochastic Systems.Journal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:f2a4233a-2ac2-4f63-a3d4-102e6e135efcEnglishSymplectic Elements at OxfordSpringer2012Chen, TForejt, VKwiatkowska, MParker, DSimaitis, AFlanagan, CKönig, BWe present automatic verification techniques for the modelling and analysis of probabilistic systems that incorporate competitive behaviour. These systems are modelled as turn-based stochastic multi-player games, in which the players can either collaborate or compete in order to achieve a particular goal. We define a temporal logic called rPATL for expressing quantitative properties of stochastic multi-player games. This logic allows us to reason about the collective ability of a set of players to achieve a goal relating to the probability of an event's occurrence or the expected amount of cost/reward accumulated. We give a model checking algorithm for verifying properties expressed in this logic and implement the techniques in a probabilistic model checker, based on the PRISM tool. We demonstrate the applicability and efficiency of our methods by deploying them to analyse and detect potential weaknesses in a variety of large case studies, including algorithms for energy management and collective decision making for autonomous systems. © 2012 Springer-Verlag Berlin Heidelberg. |
| spellingShingle | Chen, T Forejt, V Kwiatkowska, M Parker, D Simaitis, A Automatic Verification of Competitive Stochastic Systems. |
| title | Automatic Verification of Competitive Stochastic Systems. |
| title_full | Automatic Verification of Competitive Stochastic Systems. |
| title_fullStr | Automatic Verification of Competitive Stochastic Systems. |
| title_full_unstemmed | Automatic Verification of Competitive Stochastic Systems. |
| title_short | Automatic Verification of Competitive Stochastic Systems. |
| title_sort | automatic verification of competitive stochastic systems |
| work_keys_str_mv | AT chent automaticverificationofcompetitivestochasticsystems AT forejtv automaticverificationofcompetitivestochasticsystems AT kwiatkowskam automaticverificationofcompetitivestochasticsystems AT parkerd automaticverificationofcompetitivestochasticsystems AT simaitisa automaticverificationofcompetitivestochasticsystems |