Please wait a minute...
浙江大学学报(工学版)
J4  2009, Vol. 43 Issue (6): 1014-1019    DOI: 10.3785/j.issn.1008-973X.2009.
    
Dynamic model of normative multi-agent system and its property verification mechanism
HU Bin1,2, GAO Ji1, GUO Hang1
(1. College of Computer Science and Technology, Zhejiang University, Hangzhou 310027, China;
2. College of Information Engineering, Hangzhou Normal University, Hangzhou 310018, China)
Download:   PDF(993KB) HTML
Export: BibTeX | EndNote (RIS)      

Abstract  

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．

Published: 01 June 2009
CLC:  TP182  
Service
E-mail this article
Add to my bookshelf
Add to citation manager
E-mail Alert
RSS
Articles by authors
Cite this article:

HU Bin, GAO Ji, GUO Hang. Dynamic model of normative multi-agent system and its property verification mechanism. J4, 2009, 43(6): 1014-1019.

URL:

http://www.zjujournals.com/eng/10.3785/j.issn.1008-973X.2009.     OR     http://www.zjujournals.com/eng/Y2009/V43/I6/1014


规范多agent系统动态模型及其属性验证机制

针对规范多Agent系统（NMAS）并发性、动态性和规范性的特点,提出了一种规范多Agent系统动态模型和基于模型检验的属性验证机制.其中动态模型包括行为约束规范语言TNAL和联合行为转移结构两大部分.TNAL以现实世界法律法规为参考,实现了规范的时态特性和道义特性的建模.联合行为转移结构以多Agent联合行为作为状态转移标记,以规范剪枝后的计算树描述规范系统的动态语义,使系统属性描述语言和规范语言相互独立.以CTL*作为系统属性描述语言,借助现有模型检验工具即可实现NMAS的属性验证,这种实现方式使系统验证工作具有更高的灵活性.

［1］ AGONTNES T, HOEK W V D, AGUILAR J A, et al. On the logic of normative systems［C］∥Proceedings of the 20th International Joint Conference on Artificial Intelligence. Hyderabad : AAAI, 2007: 11751180．
［2］ SHOHAM Y, TENNENHOLTZ M, On social laws for artificial agent societies: off-line design［J］. Artificial Intelligence, 1995, 73(1): 231252.
［3］ WOOLDRIDGE M, HOEK W V D. On obligations and normative ability: towards a logical analysis of the social contract［J］. Journal of Applied Logic, 2005, 3 (3):396420．
［4］ ALCHOURRON C E, BULYGIN E. Normative sytems［M］. Berlin: Springer,1971．
［5］ BOELLA G, TORRE L V D, VERHAGEN H. Introduction to normative multiagent systems［J］. Computational & Mathematical Organization Theory, 2006, 12 (2): 7179．
［6］ MEYER J J C, WIERINGA R. Deontic logic in computer science: normative system specification［M］. Hoboken: Wiley, 1993．
［7］ ALUR R, HENZINGER T A, KUPFERMAN O. Alternating time temporal logic［J］. Journal of the ACM, 2002, 49(1): 672713．
［8］ GOVERNATON G, ROTOLO A. BIO logical agents: norms, beliefs, intentions in defeasible logic［J］. Autonomous Agents and Multi-Agent Systems, 2008, 17 (1): 3669．
［9］ FAGIN R, HALPERN J Y, MOSES Y, et al. Reasoning about knowledge［M］. Cambridge: MIT, 1995．
［10］ ARTIKIS A, SERGOT M, PITT J. Specifying norm governed computational societies［J］. ACM Trans actious on Computational Logic, 2009, 10(1): 141．
［11］ WOOLDRIDGE M. An introduction to multiagent systems［M］. Chichester: Wiley, 2002．
［12］ EMERSON E A. Model checking and the mu-calculus［C］∥ Proceedings of the DIMACS Symposium on Descriptive Complexity and Finite Model. Princeton: American Mathematical Society, 1996: 185214．
［13］ HUTH M, RYAN M. Logic in computer science: modelling and reasoning about systems［M］. Cambridge: Cambridge University Press, 2004．
No related articles found!