Please wait a minute...
浙江大学学报(工学版)
J4  2009, Vol. 43 Issue (6): 1014-1019    DOI: 10.3785/j.issn.1008-973X.2009.
计算机技术、自动化技术     
规范多agent系统动态模型及其属性验证机制
胡斌1,2,高济1,郭航1
（1.浙江大学 计算机科学与技术学院,浙江 杭州 310027；2.杭州师范大学 信息工程学院,浙江 杭州 310018）
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)
 全文: PDF(993 KB)  
摘要：

针对规范多Agent系统（NMAS）并发性、动态性和规范性的特点,提出了一种规范多Agent系统动态模型和基于模型检验的属性验证机制.其中动态模型包括行为约束规范语言TNAL和联合行为转移结构两大部分.TNAL以现实世界法律法规为参考,实现了规范的时态特性和道义特性的建模.联合行为转移结构以多Agent联合行为作为状态转移标记,以规范剪枝后的计算树描述规范系统的动态语义,使系统属性描述语言和规范语言相互独立.以CTL*作为系统属性描述语言,借助现有模型检验工具即可实现NMAS的属性验证,这种实现方式使系统验证工作具有更高的灵活性.
关键词： 多Agent系统;  Kripke结构;  动态模型;  属性验证    
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．
Key words: multi-agent system    Kripke structure    dynamic model    property verification
出版日期: 2009-07-01
:  TP182  
基金资助:

国家“863”高技术研究发展计划资助项目（2007AA01Z187）;杭州师范大学科研启动资助项目(YS05203144).
通讯作者: 高济，男，教授，博导.     E-mail: gaoji@hz.zj.cn
作者简介: 胡斌 （1978-），男，浙江建德人，讲师，从事多Agent理论与技术、形式系统的研究.
服务　　
把本文推荐给朋友
加入引用管理器
E-mail Alert
RSS
作者相关文章　　
胡斌
高济
郭航

引用本文:

胡斌, 高济, 郭航. 规范多agent系统动态模型及其属性验证机制[J]. J4, 2009, 43(6): 1014-1019.

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

链接本文:

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

［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．
[1] 艾解清, 高济, 彭艳斌, 郑志军. 基于直推式支持向量机的协商决策模型[J]. J4, 2012, 46(6): 967-973.
[2] 徐萍, 高济, 郭航. 基于双层信誉和反馈机制的可信信誉计算[J]. J4, 2009, 43(12): 2160-2164.
[3] 徐小良 汪乐宇 周泓. 自动测试系统的对象框架[J]. J4, 2004, 38(1): 39-43.