OPERAS: A Framework for the Formal Modelling of Multi-Agent Systems and Its Application to Swarm-Based Systems

  • Ioanna Stamatopoulou
  • Petros Kefalas
  • Marian Gheorghe
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4995)


Swarm-based systems are a class of multi-agent systems (MAS) of particular interest because they exhibit emergent behaviour through self-organisation. They are biology-inspired but find themselves applicable to a wide range of domains, with some of them characterised as mission critical. It is therefore implied that the use of a formal framework and methods would facilitate modelling of a MAS in such a way that the final product is fully tested and safety properties are verified. One way to achieve this is by defining a new formalism to specify MAS, something which could precisely fit the purpose but requires significant period to formally prove the validation power of the method. The alternative is to use existing formal methods thus exploiting their legacy. In this paper, we follow the latter approach. We present OPERAS, an open framework that facilitates formal modelling of MAS through employing existing formal methods. We describe how a particular instance of this framework, namely OPERAS XC , could integrate the most prominent characteristics of finite state machines and biological computation systems, such as X-machines and P Systems respectively. We demonstrate how the resulting method can be used to formally model a swarm system and discuss the flexibility and advantages of this approach.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Mamei, M., Menezes, R., Tolksdorf, R., Zambonelli, F.: Case studies for self-organization in computer science. Journal of Systems Arch. 52, 443–460 (2006)CrossRefGoogle Scholar
  2. 2.
    Dignum, V., Dignum, F.: Understanding organizational congruence: Formal model and simulation framework. In: Proceedings of the Agent-Directed Simulation Symposium (ADS 2007), Norfolk, USA (March 2007)Google Scholar
  3. 3.
    Dignum, V., Dignum, F.: A logic for agent organization. In: Proceedings of the Workshop on Formal Approaches to Multi-Agent Systems Durham, September 3-7 (2007)Google Scholar
  4. 4.
    Hoogendoorn, M., Schut, M.C., Treur, J.: Modeling decentralized organizational change in honeybee societies. In: Almeida e Costa, F., Rocha, L.M., Costa, E., Harvey, I., Coutinho, A. (eds.) ECAL 2007. LNCS (LNAI), vol. 4648, pp. 615–624. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  5. 5.
    Charrier, R., Bourjot, C., Charpillet, F.: Deterministic nonlinear modeling of ant algorithm with logistic multiagent system. In: Proceedings of the 6th international Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2007). ACM, New York (2007)Google Scholar
  6. 6.
    Matson, E., DeLoach, S.: Formal transition in agent organizations. In: Proceedings of the International Conference on Integration of Knowledge Intensive Multi-Agent Systems, pp. 235–240 (2005)Google Scholar
  7. 7.
    DeLoach, S.A.: Engineering organization-based multiagent systems. In: Garcia, A., Choren, R., Lucena, C., Giorgini, P., Holvoet, T., Romanovsky, A. (eds.) SELMAS 2005. LNCS, vol. 3914, pp. 109–125. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  8. 8.
    dInverno, M., Luck, M., Georgeff, M., Kinny, D., Wooldridge, M.: The dMARS architechure: A specification of the distributed multi-agent reasoning system. Autonomous Agents and Multi-Agent Systems 9, 5–53 (2004)CrossRefGoogle Scholar
  9. 9.
    Rabinovich, Z., Rosenschein, J.S.: Dynamics based control: Structure. In: Workshop on Multi-Agent Sequential Decision Making in Uncertain Domains, at The 5th International Joint Conference on Autonomous Agents and Multiagent Systems, Hakodate, Japan, pp. 148–161 (2006)Google Scholar
  10. 10.
    Luck, M., d’Inverno, M.: Formal methods and agent-based systems. In: Rouff, C., Truszkowski, M.H.J.R.J., Gordon-Spears, D. (eds.) NASA Monographs in Systems and Software Engineering. Springer, Heidelberg (2006)Google Scholar
  11. 11.
    Fisher, M., Wooldridge, M.: On the formal specification and verification of multi-agent systems. International Journal of Cooperating Information Systems 6, 37–65 (1997)CrossRefGoogle Scholar
  12. 12.
    Hilaire, V., Koukam, A., Gruer, P., Müller, J.P.: Formal specification and prototyping of multi-agent systems. In: Omicini, A., Tolksdorf, R., Zambonelli, F. (eds.) ESAW 2000. LNCS (LNAI), vol. 1972, pp. 114–127. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  13. 13.
    Odell, J., Parunak, H.V.D., Bauer, B.: Extending UML for agents. In: Proceedings of the Agent-Oriented Information Systems Workshop at the 17th National Conference on Artificial Intelligence, pp. 3–17 (2000)Google Scholar
  14. 14.
    Ferber, J., Gutknecht, O., Michel, F.: From agents to organizations: an organizational view of multiagent systems. In: Giorgini, P., Müller, J.P., Odell, J.J. (eds.) AOSE 2003. LNCS, vol. 2935, pp. 214–230. Springer, Heidelberg (2004)Google Scholar
  15. 15.
    Gutknecht, O., Ferber, J.: MadKit: a generic multi-agent platform. In: Proc. of the 4th International Conference on Autonomous Agents, pp. 78–79 (2000)Google Scholar
  16. 16.
    Chopra, A.K., Mallya, A.U., Desai, N.V., Singh, M.P.: Modeling flexible business processes. In: AAMAS 2004 (2004)Google Scholar
  17. 17.
    Krishna, S.N., Păun, G.: P systems with mobile membranes. Natural Computing: an international journal 4, 255–274 (2005)CrossRefMathSciNetzbMATHGoogle Scholar
  18. 18.
    Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, pp. 140–155. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  19. 19.
    Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes I. Information and Computation 100, 1–40 (1992)CrossRefMathSciNetzbMATHGoogle Scholar
  20. 20.
    Păun, G.: Computing with membranes. Journal of Computer and System Sciences 61, 108–143 (2000); Also circulated as a TUCS report since (1998)CrossRefMathSciNetzbMATHGoogle Scholar
  21. 21.
    Banatre, J., Le Metayer, D.: The gamma model and its discipline of programming. Science of Computer Programming 15, 55–77 (1990)CrossRefMathSciNetzbMATHGoogle Scholar
  22. 22.
    Berry, G., Boudol, G.: The chemical abstract machine. Journal of Theoretical Computer Science 96, 217–248 (1992)CrossRefMathSciNetzbMATHGoogle Scholar
  23. 23.
    Rouf, C., Vanderbilt, A., Truszkowski, W., Rash, J., Hinchey, M.: Verification of NASA emergent systems. In: Proceedings of the 9th IEEE International Conference on Engineering Complex Computer Systems (ICECCS 2004), pp. 231–238 (2004)Google Scholar
  24. 24.
    Stamatopoulou, I., Kefalas, P., Gheorghe, M.: Modelling the dynamic structure of biological state-based systems. BioSystems 87, 142–149 (2007)CrossRefGoogle Scholar
  25. 25.
    Kefalas, P., Stamatopoulou, I., Gheorghe, M.: A formal modelling framework for developing multi-agent systems with dynamic structure and behaviour. In: Pěchouček, M., Petta, P., Varga, L.Z. (eds.) CEEMAS 2005. LNCS (LNAI), vol. 3690, pp. 122–131. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  26. 26.
    Stamatopoulou, I., Kefalas, P., Gheorghe, M.: Specification of reconfigurable MAS: A hybrid formal approach. In: Antoniou, G., Potamias, G., Spyropoulos, C., Plexousakis, D. (eds.) SETN 2006. LNCS (LNAI), vol. 3955, pp. 592–595. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  27. 27.
    Stamatopoulou, I., Kefalas, P., Gheorghe, M.: OPERASCC: An instance of a formal framework for MAS modelling based on Population P Systems. In: Eleftherakis, G., Kefalas, P., Păun, G., Rozenberg, G., Salomaa, A. (eds.) WMC 2007. LNCS, vol. 4860, pp. 551–566. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  28. 28.
    Eilenberg, S.: Automata, Languages and Machines. Academic Press, London (1974)zbMATHGoogle Scholar
  29. 29.
    Kefalas, P., Eleftherakis, G., Kehris, E.: Communicating X-machines: A practical approach for formal and modular specification of large systems. Journal of Information and Software Technology 45, 269–280 (2003)CrossRefGoogle Scholar
  30. 30.
    Eleftherakis, G.: Formal Verification of X-machine Models: Towards Formal Development of Computer-based Systems. PhD thesis, Department of Computer Science, University of Sheffield (2003)Google Scholar
  31. 31.
    Holcombe, M., Ipate, F.: Correct Systems: Building a Business Process Solution. Springer, London (1998)zbMATHGoogle Scholar
  32. 32.
    Bernandini, F., Gheorghe, M.: Population P Systems. Journal of Universal Computer Science 10, 509–539 (2004)Google Scholar
  33. 33.
    Kefalas, P., Eleftherakis, G., Holcombe, M., Stamatopoulou, I.: Formal modelling of the dynamic behaviour of biology-inspired agent-based systems. In: Gheorghe, M. (ed.) Molecular Computational Models: Unconventional Approaches, pp. 243–276. Idea Publishing Inc. (2005)Google Scholar
  34. 34.
    Rouff, C., Vanderbilt, A., Hinchey, M., Truszkowski, W., Rash, J.: Properties of a formal method for prediction of emergent behaviors in swarm-based systems. In: Procedings of the 2nd International Conference on Software Engineering and Formal Methods, pp. 24–33 (2004)Google Scholar
  35. 35.
    Kefalas, P., Stamatopoulou, I., Gheorghe, M.: Principles of transforming Communicating X-machines to Population P Systems. In: Proceedings of the International Workshop on Automata for Cellular and Molecular Computing (ACMC 2007) (2007); Also to appear in the International Journal of Foundations of Computer Science Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Ioanna Stamatopoulou
    • 1
  • Petros Kefalas
    • 2
  • Marian Gheorghe
    • 3
  1. 1.South-East European Research CentreThessalonikiGreece
  2. 2.Department of Computer ScienceCITY CollegeThessalonikiGreece
  3. 3.Department of Computer ScienceUniversity of SheffieldUK

Personalised recommendations