Automatic Verification of Competitive Stochastic Systems

Varování

Publikace nespadá pod Ústav výpočetní techniky, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

CHEN Taolue FOREJT Vojtěch KWIATKOWSKA Marta PARKER Dave SIMAITIS Aistis

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

Fakulta informatiky

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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info