How to reduce, in principle, arms in a verifiable manner that is trusted by two or more parties is a hard but important problem. Nations and organisations that wish to engage in such arms control verification activities need to be able to design procedures and control mechanisms that capture their trust assumptions and let them compute pertinent degrees of belief. Crucially, they also will need methods for reliably assessing their confidence in such computed degrees of belief in situations with little or no contextual data. We model an arms control verification scenario with what we call constrained Bayesian Belief Networks (cBBN). A cBBN represents a set of Bayesian Belief Networks by symbolically expressing uncertainty about probabilities and scenario-specific constraints that are not represented by a BBN. We show that this abstraction of BBNs can mitigate well against the lack of prior data. Specifically, we describe how cBBNs have faithful representations within a Satisfiability Modulo Theory (SMT) solver, and that these representations open up new ways of automatically assessing the confidence that we may have in the degrees of belief represented by cBBNs. Furthermore, we show how to perform symbolic sensitivity analyses of cBBNs, and how to compute global optima of under-specified probabilities of particular interest to decision making. SMT solving also enables us to assess the relative confidence we have in two cBBNs of the same scenario, where these models may share some information but express some aspects of the scenario at different levels of abstraction.

Abstract CSP || B is an integration of two well known formal notations: CSP and B. It provides a method for modelling systems with both complex state (described in B machines) and control flow (described as CSP processes). Consistency checking within this approach verifies that a controller process never calls a B operation outside its precondition. Otherwise the behaviour of the operation cannot be predicted. In previous work, this check was carried out by manually decomposing the model before preprocessing the CSP processes to perform a hand-written weakest precondition proof. In this paper, a framework is described that mechanises consistency checking in a theorem prover and removes the need for preprocessing. This work is based on an existing PVS embedding of the CSP traces model, but it is extended by introducing a notion of state so that the interaction between processes and machines can be analysed. Numerous rules have been defined (and proved) which enable consistency checking and decomposition via PVS proof. These rules also formally justify the relaxation of previous constraints on CSP || B architectures, thereby widening the scope of CSP || B modelling. The PVS embedding and rules presented in this paper are not only applicable to CSP || B specifications, but to other combined approaches which use a non-blocking semantics for the state-based operations.