A Formal Method of Obligation Policy for Agent Interaction

Abstract:

In Multi-Agent System, obligations are actions that agents are required to take or some states of affairs which should be maintained, formal modeling and verifying obligation policy which is high-level requirements specifications or communication protocol for constraining agent interaction can enhance the correctness of the system design. Therefore, in this paper a formal framework language for modeling obligation policy is introduced. In this method, the obligations are defined as a special social commitment, the state models of obligation are defined by classifying the obligation. Then we use the policy context and state model to formal the dynamic execution of obligation policy, finally the operational semantics of the framework language is defined as a state transition system which has Kripke semantic structure and it can be as formal foundation for model checking.

• Periodical: Applied Mechanics and Materials (Volumes 571-572)
• Pages: 481-489
• DOI: https://doi.org/10.4028/www.scientific.net/AMM.571-572.481
• Online since: June 2014
• Authors: Tao Zhang*, Hong Xie, Shao Bin Huang
• Keywords: Formal Method, Multi-Agent System (MAS), Obligation Policy Model, Social Commitment

References

[1] DONG Meng-Gao, MAO Xin-Jun, CHANG Zhi-Ming, et al. Running Mechanism and Strategy Description Language SADL for Self-Adaptive MAS. JOURNAL OF SOFTWARE, 2011, 22(4): 609-624.

DOI: 10.3724/sp.j.1001.2011.03762

[2] M. Loizos, P. David C., Pfeffer Avi. Specifying and monitoring economic environments using rights and obligations. AUTONOMOUS AGENTS AND MULTI-AGENT SYSTEMS, 2010, 20(2): 158-197.

DOI: 10.1007/s10458-009-9089-6

[3] Xu Dian-xiang, Sanford Michael, Liu Zhao-liang. Testing Access Control and Obligation Policies[C]/ International Conference on Computing, Networking and Communications. San Diego, CA, 2013: 540-544.

DOI: 10.1109/iccnc.2013.6504143

[4] Young Jessica D., Antón Annie I. A method for identifying software requirements based on policy commitments[C]/Proceedings of the 18th IEEE International Requirements Engineering Conference. Sydney, NSW, Australia, 2010: 47-56.

DOI: 10.1109/re.2010.17

[5] Baldoni M., Baroglio C., et al. Constitutive and Regulative Specifications of Commitment Protocols: A Decoupled Approach. ACM TRANSACTIONS ON INTELLIGENT SYSTEMS AND TECHNOLOGY, 2013, 4(2): 1-25.

DOI: 10.1145/2438653.2438657

[6] Minsky, N.H., Rozenshtein, D. A law-based approach to object-oriented programming. Proceedings on Object-Oriented Programming Systems, Languages and Applications. New York, NY, USA, 1987: 482–493.

DOI: 10.1145/38765.38851

[7] Minsky, N.H., Ungureanu, V. Law-governed interaction: a coordination and control mechanism for heterogeneous distributed systems. ACM Transactions on Software Engineering Methodology, 2000, 9 (3): 273–305.

DOI: 10.1145/352591.352592

[8] R. Craven, J. Lobo, J. Ma, A. Russo, et al. Expressive policy analysis with enhanced system dynamicity. Proceedings of the 4th International Symposium on Information, Computer, and Communications Security. New York, USA, 2009: 239-250.

DOI: 10.1145/1533057.1533091

[9] D.J. Dougherty, K. Fisler, S. Krishnamurthi, Obligations and their interaction with programs. Proceedings of 12th European Symposium on Research in Computer Security, Dresden, Germany, 2007: 375–389.

DOI: 10.1007/978-3-540-74835-9_25

[10] B. Katt, X. Zhang, R. Breu, M. Hafner, J.P. Seifert, A general obligation model and continuity: enhanced policy enforcement engine for usage control. Proceedings of the 13th ACM symposium on Access control models and technologies. New York, NY, USA, 2008: 123–132.

DOI: 10.1145/1377836.1377856

[11] Y. Elrakaiby, F. Cuppens, N. Cuppens-Boulahia, Formalization and management of group obligations. IEEE International Symposium on Policies for Distributed Systems and Networks. London, ENGLAND , 2009: 158–165.

DOI: 10.1109/policy.2009.10

[12] M., J. Bentahar, El-Menshawy, et al. Communicative commitments: Model checking and complexity analysis. Knowledge-Based Systems, 2012, 35(11): 21-34.

DOI: 10.1016/j.knosys.2012.04.010

[13] Chesani F., Mello P., et al. Representing and monitoring social commitments using the event calculus. Autonomous Agents and Multi-Agent Systems, 2013, 27(1): 85-130.

DOI: 10.1007/s10458-012-9202-0

[14] EI-Menshawy, M., J. Bentahar, et al. Modeling and Verifying Business Interactions via Commitments and Dialogue Actions. Proceedings of the 4th KES International Symposium on Agent and Multi-Agent Systems. Gdynia, POLAND, 2010: 11-21.

DOI: 10.1007/978-3-642-13541-5_2

[15] Fornara N. and M. Colombetti. Specifying and enforcing norms in artificial institutions: A retrospective review. Proceedings of the 9th International Workshop on Declarative Agent Languages and Technologies. Taipei, Taiwan, 2012: 117-119.

DOI: 10.1007/978-3-642-29113-5_12

[16] EI-Menshawy, M., J. Bentahar, et al. Reducing model checking commitments for agent communication to model checking ARCTL and GCTL*. Autonomous Agents and Multi-Agent Systems, 2013, 27(3): 375-418.

DOI: 10.1007/s10458-012-9208-7

[17] A. Gunay, P. Yolum. Constraint satisfaction as a tool for modeling and checking feasibility of multiagent commitments. Applied Intelligence, 2013, 39(3): 489-509.

DOI: 10.1007/s10489-013-0428-6

[18] Elrakaiby, Y., F. Cuppens, et al. Formal enforcement and management of obligation policies., Data & Knowledge Engineering 71(1): 127-147.

DOI: 10.1016/j.datak.2011.09.001

[19] E.M. Clarke, O. Grumberg, D.A. Peled. Model Checking. Cambridge, MA: MIT Press. (1999).

[20] McMillan L. Symbolic model checking. Carnegie Mellon University, (1992).

[21] Holzmann J. The model checker SPIN. IEEE Trans. on Software Engineering, 1997, 23(5): 279−295.

DOI: 10.1109/32.588521

[22] Christel Baier, Joost-Pieter Katoen, Kim Guldstrand Larsen. Principles of Model Checking. The MIT Press. May 31, (2008).

DOI: 10.1093/comjnl/bxp025