Specification and verification of knowledge in a multi-agent system
Marina Bagić, Mojca Ciglarič · 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 model for MAS specification and then, with the proper technique to verify the system. In this paper we propose our model for MAS specification as the extended labelled transition system (Milner's Process Algebra), namely Mixed Transition System (MTS). We support our approach with the case study of specification and verification of FIPA Subscribe Scenario, a protocol for inter-agent communication.