Confidence analysis for nuclear arms control: SMT abstractions of Game Theoretic Models

Abstract

We consider the use of game theory in an arms control inspection planning scenario. Speci cally we develop a case study that games the number of inspections available against an ideal treaty length. Normal game theoretic techniques struggle to justify pay-o values to use for certain events, limiting the usefulness of such techniques. In order to improve the value of using game theory for decision making, we introduce a methodology for under-specifying the game theoretic models through a mixture of regression techniques and Satis ability Modulo Theory (SMT) constraint solving programs. Our approach allows a user to under-specify pay-o s in games, and to check, in a manner akin to robust optimisation, for how such under-speci cations a ect the `solution' of a game. We analyse the Nash equilibria and the mixed strategy sets that would lead to such equilibria - and explore how to maximise expected pay-o s and use of individual pure strategies for all possible values of an under-speci cation. Through this approach, we gain an insight into how - irrespective of uncertainty - we can still compute with game theoretic models, and present the types and kinds of analysis we can run that bene t from this uncertainty.