Probabilistic Model Checking and Autonomy

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.

Nonzero-Sum Stochastic Games and Mean-Field Games with Impulse Controls

We consider a general class of nonzero-sum N-player stochastic games with impulse controls, where players control the underlying dynamics with discrete interventions. We adopt a verification approach and provide sufficient conditions for the Nash equilibria (NEs) of the game. We then consider the limiting situation when N goes to infinity, that is, a suitable mean-field game (MFG) with impulse controls. We show that under appropriate technical conditions, there exists a unique NE solution to the MFG, which is an ϵ-NE approximation to the N-player game, with [Formula: see text]. As an example, we analyze in detail a class of two-player stochastic games which extends the classical cash management problem to the game setting. In particular, we present numerical analysis for the cases of the single player, the two-player game, and the MFG, showing the impact of competition on the player’s optimal strategy, with sensitivity analysis of the model parameters.

Learning Nash Equilibria in Zero-Sum Stochastic Games via Entropy-Regularized Policy Approximation

We explore the use of policy approximations to reduce the computational cost of learning Nash equilibria in zero-sum stochastic games. We propose a new Q-learning type algorithm that uses a sequence of entropy-regularized soft policies to approximate the Nash policy during the Q-function updates. We prove that under certain conditions, by updating the entropy regularization, the algorithm converges to a Nash equilibrium. We also demonstrate the proposed algorithm's ability to transfer previous training experiences, enabling the agents to adapt quickly to new environments. We provide a dynamic hyper-parameter scheduling scheme to further expedite convergence. Empirical results applied to a number of stochastic games verify that the proposed algorithm converges to the Nash equilibrium, while exhibiting a major speed-up over existing algorithms.