Informace o publikaci
Automatic Verification of Competitive Stochastic Systems
Autoři | |
---|---|
Rok publikování | 2012 |
Druh | Článek ve sborníku |
Konference | Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference |
Fakulta / Pracoviště MU | |
Citace | |
www | http://www.prismmodelchecker.org/papers/tacas12.pdf |
Doi | http://dx.doi.org/10.1007/978-3-642-28756-5_22 |
Obor | Informatika |
Klíčová slova | stochastic games; branching time logics; multi-agent systems |
Popis | 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. |
Související projekty: |