Modelling Epistemic Properties for Specification and Verification of a Multi-agent System
Marina Bagić, Mojca Ciglarič · International Conference on Software Engineering · 2007
Verification of epistemic properties, i.e. properties involving knowledge of a multi-agent system (MAS) is a great challenge because there are still many open problems especially with the choice of a proper formal model for multi- agent specification and then, with the proper technique to verify the system. In this paper we propose our formal model for MAS specification as the extended Labelled Transition System (LTS) which is used in Milner's Process Algebra. In oder to verify the system we use model checking technique which aims to create total state space and the transition relation among all the states in which the system can be during its lifetime. We give our analysis with the case study of formal specification and verification of FIPA Query Protocol.