Conditional commitments: Reasoning and model checking

Warda El Kholy, Jamal Bentahar, Mohamed El Menshawy, Hongyang Qu, Rachida Dssouli

Research output: Contribution to journalArticlepeer-review

22 Scopus citations

Abstract

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 CTLcc 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 CTLcc. We finally compare the experimental results with existing proposals.

Original languageBritish English
Article number9
JournalACM Transactions on Software Engineering and Methodology
Volume24
Issue number2
DOIs
StatePublished - 1 Dec 2014

Keywords

  • Reasoning rules
  • Strong and weak conditional commitments

Fingerprint

Dive into the research topics of 'Conditional commitments: Reasoning and model checking'. Together they form a unique fingerprint.

Cite this