Verification of CTL_BDI Properties by Symbolic Model Checking
Ran Chen, Wenhui Zhang · 2019
The Belief-Desire-Intention (BDI) architecture is a framework for studying computational agents capable of rational behaviors. The behaviors of such agents may be modeled by possible world structures, for the specification of the behaviors, CTLBDImay be used. As multi-agent systems are increasingly complex, the problem of their verification is acquiring importance. This work develops a symbolic model checking approach for the verification of CTLBDIproperties within the BDI-architecture. In addition, we develop a symbolic approach for checking whether a model satisfies the weak and strong realism constraints. The approaches for model checking and realism checking have been implemented, and the experimental data show that the approaches are able to handle models with a fairly large number of possible worlds.