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

Weconsidertheuseofgametheoryinanarmscontrolinspectionplanningscenario.Specifically 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-off 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 Satisfiability Modulo Theory (SMT) constraint solving programs. Our approach allows a user to under-specify pay-offs in games, and to check, in a manner akin to robust optimisation, for how such under-specifications affect 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-offs and use of individual pure strategies for all possible values of an under-specification. 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 benefit from this uncertainty.