Search

The design and control of autonomous systems that operate in uncertain or adversarial environments can be facilitated by formal modeling and analysis. Probabilistic model checking is a technique to automatically verify, for a given temporal logic specification, that a system model satisfies the specification, as well as to synthesize an optimal strategy for its control. This method has recently been extended to multiagent systems that exhibit competitive or cooperative behavior modeled via stochastic games and synthesis of equilibria strategies. In this article, we provide an overview of probabilistic model checking, focusing on models supported by the PRISM and PRISM-games model checkers. This overview includes fully observable and partially observable Markov decision processes, as well as turn-based and concurrent stochastic games, together with associated probabilistic temporal logics. We demonstrate the applicability of the framework through illustrative examples from autonomous systems. Finally, we highlight research challenges and suggest directions for future work in this area. Expected final online publication date for the Annual Review of Control, Robotics, and Autonomous Systems, Volume 5 is May 2022. Please see http://www.annualreviews.org/page/journal/pubdates for revised estimates.

Probabilistic model checking can overcome much of the complexity inherent in balancing games. Game balancing is the careful maintenance of relationships between the ways in which a game can be played, to ensure that no single way is strictly better than all others, and that players are offered a wide variety of ways to play successfully. We introduce a novel approach toward automating game balancing using probabilistic model checking called chained strategy generation (CSG). This involves generating chains of adversarial strategies, which mimic the way players adapt their approach during repeated plays of a game. We use CSG to map out the evolving metagame. The trends identified can allow game developers to identify strategies, which will be too strong, and ways of playing the game, which a player may want to use, but are never viable for successful competitive play. We introduce a case study, a game called RPGLite, and use CSG to compare five candidate configurations for the game. We show how to determine which configurations of RPGLite lead to a more fair and interesting experience for players. We also identify unexpected trends in how the strategies evolve. Our approach introduces a new technique for improving game development and player experience.

Game-theoretic concepts have been extensively studied in economics to provide insight into competitive behaviour and strategic decision making. As computing systems increasingly involve concurrently acting autonomous agents, game-theoretic approaches are becoming widespread in computer science as a faithful modelling abstraction. These techniques can be used to reason about the competitive or collaborative behaviour of multiple rational agents with distinct goals or objectives. This paper provides an overview of recent advances in developing a modelling, verification and strategy synthesis framework for concurrent stochastic games implemented in the probabilistic model checker PRISM-games. This is based on a temporal logic that supports finite- and infinite-horizon temporal properties in both a zero-sum and nonzero-sum setting, the latter using Nash and correlated equilibria with respect to two optimality criteria, social welfare and social fairness. We summarise the key concepts, logics and algorithms and the currently available tool support. Future challenges and recent progress in adapting the framework and algorithmic solutions to continuous environments and neural networks are also outlined., Comment: 22 pages, 7 figures

We report on the automatic verification of timed probabilistic properties of the IEEE 1394 root contention protocol combining two existing tools: the real-time model-checker KRONOS and the probabilistic model-checker PRISM. The system is modelled as a probabilistic timed automaton. We first use KRONOS to perform a symbolic forward reachability analysis to generate the set of states that are reachable with non-zero probability from the initial state, and before the deadline expires. We then encode this information as a Markov decision process to be analyzed with PRISM. We apply this technique to compute the minimal probability of a leader being elected before a deadline, for different deadlines, and study the influence of using a biased coin on this minimal probability.

For use in vehicular networks, IEEE 802.11p has been standardized as the underlying wireless system. The 802.11 standard distinguishes two main methods of operation with respect to channel access, the Distributed Coordination Function (DCF) and the Enhanced Distributed Channel Access (EDCA), where the latter is the mandated method to be used in vehicular networks (in 802.11p). We present validated analytical models for both DCF and EDCA, and compare both methods in the context of beaconing.We will show that, surprisingly,DCF outperforms EDCA under assumptions that are realistic for beaconing in vehicular networks.

This volume contains the proceedings of the Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL 2011), held in Saarbrucken, Germany, April 1--3, 2011. QAPL 2011 is a satellite event of the European Joint Conferences on Theory and Practice of Software (ETAPS 2011). The workshop theme is on quantitative aspects of computation. These aspects are related to the use of physical quantities (storage space, time, bandwidth, etc.) as well as mathematical quantities (e.g. probability and measures for reliability, security and trust), and play an important (sometimes essential) role in characterising the behavior and determining the properties of systems. Such quantities are central to the definition of both the model of systems (architecture, language design, semantics) and the methodologies and tools for the analysis and verification of the systems properties. The aim of this workshop is to discuss the explicit use of quantitative information such as time and probabilities either directly in the model or as a tool for the analysis of systems.

This volume contains the proceedings of the Eighth Workshop on Quantitative Aspects of Programming Languages (QAPL 2010), held in Paphos, Cyprus, on March 27-28, 2010. QAPL 2010 is a satellite event of the European Joint Conferences on Theory and Practice of Software (ETAPS 2010). The workshop theme is on quantitative aspects of computation. These aspects are related to the use of physical quantities (storage space, time, bandwidth, etc.) as well as mathematical quantities (e.g. probability and measures for reliability, security and trust), and play an important (sometimes essential) role in characterising the behavior and determining the properties of systems. Such quantities are central to the definition of both the model of systems (architecture, language design, semantics) and the methodologies and tools for the analysis and verification of the systems properties. The aim of this workshop is to discuss the explicit use of quantitative information such as time and probabilities either directly in the model or as a tool for the analysis of systems.