SAT-Based Bounded Model Checking for Weighted Deontic Interpreted Systems

In this paper we present a SAT-based Bounded Model Checking (BMC) method for weighted deontic interpreted systems (i.e., Kripke structures where transitions carry a weight, which is an arbitrary natural number) and properties expressed in the existential fragment of a weighted temporal logic augmented to include knowledge and deontic components (WECTLKD). In particular, since in BMC both the system model and the checked property are translated into a Boolean formula to be analysed by a SAT-solver, we introduce a new Boolean encoding of the WECTLKD formulae that is particularly optimized for managing quantitative weighted temporal operators, knowledge operators, and deontic operators, which are typically found in properties of complex multiagent systems in models of which we assume the possibility that agents may not behave as they are supposed to, and that acting (coordination, negotiation, cooperation, etc.) of agents may cost. We illustrate how the weighted deontic interpreted systems can be applied to the analysis of a variant of the standard bit transmission problem in which an agent may fail to do something it is supposed to do.