Advertisement

A Formal Treatment of Agents, Goals and Operations Using Alternating-Time Temporal Logic

  • Christophe Chareton
  • Julien Brunel
  • David Chemouil
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7021)

Abstract

The aim of this paper is to provide a formal framework for Requirements Engineering modelling languages featuring agents, behavioural goals and operations as main concepts. To do so, we define Khi, a core modelling language, as well as its formal semantics in terms of a fragment of the multi-agent temporal logic ATL*, called ATLKHI. Agents in the sense of concrete and provided entities, called actors, are defined by their capabilities. They also pursue behavioural goals that are realised by operations, which are themselves gathered into abstract, required, agents, that we call roles. Then a notion of assignment, between (coalitions of) actors and roles is defined. Verifying the correctness of a given assignment then reduces to the validity of an ATLKHI formula that confronts the capabilities of (coalitions of) actors with the operations in roles played by the said actors. The approach is illustrated through a toy example featuring an online shopping marketplace.

Keywords

Assignment Problem Temporal Logic Multiagent System Formal Treatment Linear Temporal Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in to check access.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alur, R., Henzinger, T., Mang, F., Qadeer, S., Rajamani, S., Tasiran, S.: MOCHA: Modularity in model checking. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 521–525. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  2. 2.
    Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. J. ACM, 672–713 (2002)Google Scholar
  3. 3.
    Bresciani, P., Perini, A., Giorgini, P., Giunchiglia, F., Mylopoulos, J.: Tropos: An agent-oriented software development methodology. Autonomous Agents and Multi-Agent Systems, 203–236 (2004)Google Scholar
  4. 4.
    Brihaye, T., Da Costa, A., Laroussinie, F., Markey, N.: ATL with strategy contexts and bounded memory. Logical Foundations of Computer Science, 92–106 (2009)Google Scholar
  5. 5.
    Chopra, A., Dalpiaz, F., Giorgini, P., Mylopoulos, J.: Modeling and reasoning about service-oriented applications via goals and commitments. In: Pernici, B. (ed.) CAiSE 2010. LNCS, vol. 6051, pp. 113–128. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  6. 6.
    Chopra, A., Dalpiaz, F., Giorgini, P., Mylopoulos, J.: Reasoning about agents and protocols via goals and commitments. In: Proceedings of the 9th International Conference on Autonomous Agents and Multiagent Systems, vol. 1, pp. 457–464 (2010); International Foundation for Autonomous Agents and Multiagent SystemsGoogle Scholar
  7. 7.
    Chopra, A., Singh, M.: Multiagent commitment alignment. In: Proceedings of The 8th International Conference on Autonomous Agents and Multiagent Systems, vol. 2, pp. 937–944 (2009); International Foundation for Autonomous Agents and Multiagent SystemsGoogle Scholar
  8. 8.
    Du Bois, P.: The Albert II reference manual. Tech. rep., University of Namur, Belgium (1997)Google Scholar
  9. 9.
    Dubois, E., Du Bois, P., Petit, M.: ALBERT: an agent-oriented language for building and eliciting requirements for real-time systems. In: Proceedings of the Twenty-Seventh Hawaii International Conference on System Sciences. Information Systems: Collaboration Technology Organizational Systems and Technology, vol. 4, pp. 713–722. IEEE (1994)Google Scholar
  10. 10.
    van Lamsweerde, A.: Requirements engineering, From System Goals to UML Models to Software Specifications. Wiley (2009)Google Scholar
  11. 11.
    Letier, E., van Lamsweerde, A.: Agent-based tactics for goal-oriented requirements elaboration. In: Proceedings of the 24rd International Conference on Software Engineering, ICSE 2002, pp. 83–93 (May 2002)Google Scholar
  12. 12.
    Letier, E., Van Lamsweerde, A.: Deriving operational software specifications from system goals. In: Proceedings of the 10th ACM SIGSOFT Symposium on Foundations of Software Engineering, p. 128. ACM, New York (2002)Google Scholar
  13. 13.
    Letier, E.: Reasoning about Agents in Goal-Oriented Requirements Engineering. Ph.D. thesis, Universite Catholique de Louvain (November 05, 2002)Google Scholar
  14. 14.
    Mallya, A., Singh, M.: Incorporating commitment protocols into Tropos. In: Müller, J.P., Zambonelli, F. (eds.) AOSE 2005. LNCS, vol. 3950, pp. 69–80. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  15. 15.
    Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Compouter Science, pp. 46–57 (1977)Google Scholar
  16. 16.
    Silva, C., Castro, J., Tedesco, P., Araújo, J., Moreira, A., Mylopoulos, J.: Improving the architectural design of multi-agent systems: the tropos case. In: Proceedings of the 2006 International Workshop on Software Engineering for Large-Scale Multi-Agent Systems, pp. 107–113. ACM (2006)Google Scholar
  17. 17.
    Yu, E.: Agent-oriented modelling: software versus the world. In: Wooldridge, M.J., Weiß, G., Ciancarini, P. (eds.) AOSE 2001. LNCS, vol. 2222, pp. 206–225. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  18. 18.
    Yu, E.: Social modelling and i*. In: Conceptual Modelling: Foundations and Applications (2009)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Christophe Chareton
    • 1
  • Julien Brunel
    • 1
  • David Chemouil
    • 1
  1. 1.Onera – The French Aerospace LabToulouseFrance

Personalised recommendations

Cite paper

Buy options