Bounded analysis of constrained dynamical systems: a case study in nuclear arms control

Abstract

We introduce a simple dynamical system that describes key features of a bilateral nuclear arms control regime. The evolution of each party's beliefs and declarations under the regime are represented, and the e ects of inspection processes are captured. Bounded analysis of this model allows us to explore { within a nite horizon { the consequences of changes to the rules of the arms control process and to the strategies of each party, bounded scope invariants for variables of interest, and dynamics for initial states containing strict uncertainty. Together these would potentially enable a decision support system to consider cases of interest irrespective of unknowns. We realize such abilities by building a Python package that draws on the capabilities of a Satis ability Modulo Theory (SMT) solver to explore particular scenarios and to optimize measures of interest { such as the belief of one nation in the statements made by another, or the timing of an unscheduled inspection such that it has maximum value. We show that these capabilities can in principle support the design or assessment of future bilateral arms control instruments by applying them to a set of representative and relevant test scenarios with realistic nite horizons.