Automatic verification of competitive stochastic systems

Thesis

In this thesis we present a framework for automatic formal analysis of competitive stochastic systems, such as sensor networks, decentralised resource management schemes or distributed user-centric environments. We model such systems as stochastic multi-player games, which are turn-based models where an action in each state is chosen by one of the players or according to a probability distribution. The specifications, such as “sensors 1 and 2 can collaborate to detect the target with proba...

Expand abstract

Authors: Simaitis, A

• Publication date: 2014
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: stochastic games; probabilistic logic; Markov chains
• Subjects: Mathematical logic and foundations; Computer science (mathematics); Game theory,economics,social and behavioral sciences (mathematics)