Dynamic model of normative multi-agent system and its property verification mechanism
Guo Hang · Journal of Zhejiang University(Engineering Science) · 2009
Concerned with the concurrency,dynamicity and normativity of normative multi-agent systems(NMAS),a dynamic model for such systems and a model checking based property verification mechanism were introduced.The dynamic model includes an action constraint norm language,temporal normative action language(TNAL),and a joint action transition structure.TNAL is a norm language based on action constraint which references the real world laws and rules and can model the temporal and deontic character of norms.The joint action transition structure signs the transition with agents' joint actions and models the normative system's dynamic semantic with the pruning computational tree which makes the system property description language and norm language independent from each other.System properties are described with the temporal logic CTL*,so the model checking can be easily realized with current model checking tools,which makes the property checking more agile.