|
- 2016
多Agent交互策略模型检测方法
|
Abstract:
提出一种基于模型检测的多Agent交互策略验证方法,首先通过责任政策语言建模多Agent的交互策略,基于责任政策语言的操作语义将政策模型转换为模型检测器NuSMV的输入,利用时态逻辑声明表征策略冲突的系统性质,然后利用模型检测器NuSMV自动验证政策模型对性质的可满足性,并根据模型检测器产生的反例分析交互策略中的各种错误。该方法可提高交互策略的验证效率,确保多Agent系统设计的正确性。
[1] | LOIZOS M, DAVID P C, PFEFFER A. Specifying and monitoring economic environments using rights and obligations[J]. Autonomous Agents and Multi-Agent Systems, 2010, 20(2):158-197. |
[2] | FORNARA N, COLOMBETTI M. Specifying and enforcing norms in artificial institutions:a retrospective review[C]//Proceedings of the 9th International Workshop on Declarative Agent Languages and Technologies. Taipei, Taiwan, China:Springer, 2012:117-119. |
[3] | YOLUM A P. Constraint satisfaction as a tool for modeling and checking feasibility of multiagent commitments[J]. Applied Intelligence, 2013, 39(3):489-509. |
[4] | ELRAKAIBY Y, CUPPENS F, CUPPENS-Boulahia N. Formalization and management of group obligations[C]//IEEE International Symposium on Policies for Distributed Systems and Networks. London, England:Springer, 2009:158-165. |
[5] | 吴丹, 危胜军. 基于模型检测的策略冲突检测方法[J].电子科技大学学报, 2013, 42(5):745-748. WU Dan, WEI Sheng-jun. Policy conflict detection method based on model checking[J]. Journal of University of Electronic Science and Technology of China, 2013, 42(5):745-748. |
[6] | CHRISTEL B, JOOST-PIETER K. Principles of model checking[M].[S.l.]:MIT Press, 2008. |
[7] | XU Dian-xiang, SANFORD M, LIU Zhao-liang. Testing access control and obligation policies[C]//International Conference on Computing, Networking and Communications. San Diego, CA, USA:IEEE Computer Society, 2013:540-544 |
[8] | BALDONI M, BAROGLIO C. Constitutive and regulative specifications of commitment protocols:a decoupled approach[J]. Acm Transactions on Intelligent Systems and Technology, 2013, 4(2):1-25. |
[9] | MINSKY N H, UNGUREANU V. Law-governed interaction:a coordination and control mechanism for heterogeneous distributed systems[J]. ACM Transactions on Software Engineering Methodology, 2000, 9(3):273-305. |
[10] | 董孟高, 毛新军, 常志明, 等. 自适应多Agent系统的运行机制和策略描述语言SADL[J]. 软件学报, 2011, 22(4):609-624. DONG Meng-gao, MAO Xin-jun, CHANG Zhi-ming, et al. Running mechanism and strategy description language SADL for self-adaptive MAS[J]. Journal of Software, 2011, 22(4):609-624. |
[11] | MINSKY N H, ROZENSHTEIN D. A law-based approach to object-oriented programming[C]//Proceedings on Object-Oriented Programming Systems, Languages and Applications. New York, NY, USA:Applied Intelligence, 1987:482-493. |
[12] | EI-MENSHAWY M, BENTAHAR J. Reducing model checking commitments for agent communication to model checking ARCTL and GCTL[J]. Autonomous Agents and Multi-Agent Systems, 2013, 27(3):375-418. |
[13] | DOUGHERTY D J, FISLER K, KRISHNAMURTHI S. Obligations and their interaction with programs[C]//Proceedings of 12th European Symposium on Research in Computer Security. Dresden, Germany:Springer, 2007:375-389. |
[14] | CRAVEN R, LOBO J, MA J, et al. Expressive policy analysis with enhanced system dynamicity[C]//Proceedings of the 4th International Symposium on Information, Computer, and Communications Security. New York, USA:Association for Computing Machinery, 2009:239-250. |
[15] | ZHANG Tao, HUANG Shao-bi, HUANG Hong-tao. Specification and verification of policy using raise and model checking[C]//International Conference on International Conference on BioMedical Engineering and Informatics. Shanghai, China:[s.n.], 2011. |