This paper is motivated by analysing a Google self-driving car accident, i.e., the car hit a bus, with the framework and the tools of strategic reasoning by model checking. First of all, we find that existing ATL model checking may find a solution to the accident with {\it irrational} joint strategy of the bus and the car. This leads to a restriction of treating both the bus and the car as rational agents, by which their joint strategy is an equilibrium of certain solution concepts. Second, we find that a randomly-selected joint strategy from the set of equilibria may result in the collision of the two agents, i.e., the accident. Based on these, we suggest taking Correlated Equilibrium (CE) as agents' joint stratgey and optimising over the utilitarian value which is the expected sum of the agents' total rewards. The language ATL is extended with two new modalities to express the existence of an CE and a unique CE, respectively. We implement the extension into a software model checker and use the tool to analyse the examples in the paper. We also study the complexity of the model checking problems.

A general game player automatically learns to play arbitrary new games solely by being told their rules. For this purpose games are specified in the game description language GDL, a variant of Datalog with function symbols and a few known keywords. In its latest version GDL allows to describe nondeterministic games with any number of players who may have imperfect, asymmetric information. We analyse the epistemic structure and expressiveness of this language in terms of epistemic modal logic and present two main results:The operational semantics of GDL entails that the situation at any stage of a game can be characterised by a multi-agent epistemic (i.e., S5-) model;(2) GDL is sufficiently expressive to model any situation that can be described by a (finite) multi-agent epistemic model.

The Game Description Language (GDL) is a special purpose declarative language for defining games. GDL is used in the AAAI General Game Playing Competition, which tests the ability of computer programs to play games in general, rather than just the ability to play a specific game. Participants in the competition are provided with a previously unknown game specified in GDL, and are required to dynamically and autonomously determine how best to play this game. Recently, there has been much interest in the use of strategic cooperation logics for reasoning about game-like scenarios—the Alternating-time Temporal Logic (ATL) of Alur, Henzinger, and Kupferman is perhaps the best known example. Such logics are specifically intended to support reasoning about game-theoretic properties of multi-agent systems. In short, the aim of this article is to make a concrete link between ATL and GDL, with the ultimate goal of using ATL to reason about GDL-specified games. We make the following contributions. First, we demonstrate that GDL can be understood as a specification language for ATL models, and prove that the problem of interpreting ATL formulae over propositional GDL descriptions is EXPTIME-complete. Second, we use ATL to characterize a class of ‘fair playability’ conditions, which might or might not hold of various games.

The Sum-and-Product riddle was first published in the reference H. Freudenthal (1969, Nieuw Archief voor Wiskunde 3, 152) [6]. We provide an overview on the history of the dissemination of this riddle through the academic and puzzle-math community. This includes some references to precursors of the riddle, that were previously (as far as we know) unknown. We then model the Sum-and-Product riddle in a modal logic called public announcement logic. This logic contains operators for knowledge, but also operators for the informational consequences of public announcements. The logic is interpreted on multi-agent Kripke models. The information in the riddle can be represented in the traditional way by number pairs, so that Sum knows their sum and Product their product, but also as an interpreted system, so that Sum and Product at least know their local state. We show that the different representations are isomorphic. We also provide characteristic formulas of the initial epistemic state of the riddle. We analyse one of the announcements towards the solution of the riddle as a so-called unsuccessful update: a formula that becomes false because it is announced. The riddle is then implemented and its solution verified in the epistemic model checker DEMO. This can be done, we think, surprisingly elegantly. The results are compared with other work in epistemic model checking and the complexity is experimentally investigated for several representations and parameter settings.