Conditional commitments: Reasoning and model checking

While modeling interactions using social commitments provides a fundamental basis for capturing flexible and declarative interactions and helps in addressing the challenge of ensuring compliance with specifications, the designers of the system cannot guarantee that an agent complies with its commitments as it is supposed to, or at least an agent doesn't want to violate its commitments. They may still wish to develop efficient and scalable algorithms by which model checking conditional commitments, a natural and universal frame of social commitments, is feasible at design time. However, distinguishing between different but related types of conditional commitments, and developing dedicated algorithms to tackle the problem of model checking conditional commitments, is still an active research topic. In this article, we develop the temporal logic CTL^cc that extends Computation Tree Logic (CTL) with new modalities which allow representing and reasoning about two types of communicating conditional commitments and their fulfillments using the formalism of interpreted systems. We introduce a set of rules to reason about conditional commitments and their fulfillments. The verification technique is based on developing a new symbolic model checking algorithm to address this verification problem. We analyze the computational complexity and present the full implementation of the developed algorithm on top of the MCMAS model checker. We also evaluate the algorithm's effectiveness and scalability by verifying the compliance of the NetBill protocol, taken from the business domain, and the process of breast cancer diagnosis and treatment, taken from the health-care domain, with specifications expressed in CTL^cc. We finally compare the experimental results with existing proposals.