What is it about?
It is about defining a new social semantics for conditional commitments and their actions (fulfillment, cancel, delegate and assign). Then, we developed a symbolic model checking algorithm for each one of these actions and conditional commitment operator. Such algorithms are built on top of the MCMAS symbolic model checker.
Featured Image
Why is it important?
Because we can use our approach to formally model many business scenarios, communication protocols and business protocols as we shown in the paper. We can then check the correctness of these models against predefined properties using our model checker tool, SMC4AC, at design time. This will give trust, safety, reliability and confidence to the resulting system models.
Perspectives
I recommend this article for prospective readers in the fields of agent communication, model checking, and social commitments as it review and evaluate the state-of-the-art of these fields and advance it effectively. Moreover, it opens the door to model checking the relationship between conditional commitments, goals, and trust.
Mohamed El Menshawy
Read the Original
This page is a summary of: SMC4AC: A New Symbolic Model Checker for Intelligent Agent Communication, Fundamenta Informaticae, April 2017, IOS Press,
DOI: 10.3233/fi-2017-1519.
You can read the full text:
Contributors
The following have contributed to this page
