Automatic verification of concurrent stochastic systems

Automated verification techniques for stochastic games allow formal reasoning about systems that feature competitive or collaborative behaviour among rational agents in uncertain or probabilistic settings. Existing tools and techniques focus on turn-based games, where each state of the game is controlled by a single player, and on zero-sum properties, where two players or coalitions have directly opposing objectives. In this paper, we present automated verification techniques for concurrent stochastic games (CSGs), which provide a more natural model of concurrent decision making and interaction. We also consider (social welfare) Nash equilibria, to formally identify scenarios where two players or coalitions with distinct goals can collaborate to optimise their joint performance. We propose an extension of the temporal logic rPATL for specifying quantitative properties in this setting and present corresponding algorithms for verification and strategy synthesis for a variant of stopping games. For finite-horizon properties the computation is exact, while for infinite-horizon it is approximate using value iteration. For zero-sum properties it requires solving matrix games via linear programming, and for equilibria-based properties we find social welfare or social cost Nash equilibria of bimatrix games via the method of labelled polytopes through an SMT encoding. We implement this approach in PRISM-games, which required extending the tool’s modelling language for CSGs, and apply it to case studies from domains including robotics, computer security and computer networks, explicitly demonstrating the benefits of both CSGs and equilibria-based properties.

Control-Stopping Games for Market Microstructure and Beyond

In this paper, we present a family of control-stopping games that arise naturally in equilibrium-based models of market microstructure as well as in other models with strategic buyers and sellers. A distinctive feature of this family of games is the fact that the agents do not have any exogenously given fundamental value for the asset, and they deduce the value of their position from the bid and ask prices posted by other agents (i.e., they are pure speculators). As a result, in such a game, the reward function of each agent at the time of stopping depends directly on the controls of other players. The equilibrium problem leads naturally to a system of coupled control-stopping problems (or, equivalently, reflected-backward stochastic differential equations), in which the individual reward functions (or reflecting barriers) depend on the value functions (or solution components) of other agents. The resulting system, in general, presents multiple mathematical challenges because of the nonstandard form of coupling (or reflection). In the present case, this system is also complicated by the fact that the continuous controls of the agents, describing their posted bid and ask prices, are constrained to take values in a discrete grid. The latter feature reflects the presence of a positive tick size in the market, and it creates additional discontinuities in the agents’ reward functions (or reflecting barriers). Herein we prove the existence of a solution to the associated system in a special Markovian framework, provide numerical examples, and discuss the potential applications.

Dynkin games with heterogeneous beliefs

We study zero-sum optimal stopping games (Dynkin games) between two players who disagree about the underlying model. In a Markovian setting, a verification result is established showing that if a pair of functions can be found that satisfies some natural conditions then a Nash equilibrium of stopping times is obtained, with the given functions as the corresponding value functions. In general, however, there is no uniqueness of Nash equilibria, and different equilibria give rise to different value functions. As an example, we provide a thorough study of the game version of the American call option under heterogeneous beliefs. Finally, we also study equilibria in randomized stopping times.