spX-Machines: Formal State-Based Modelling of Spatial Agents

  • Isidora Petreska
  • Petros Kefalas
  • Marian Gheorghe
  • Ioanna Stamatopoulou
Part of the Communications in Computer and Information Science book series (CCIS, volume 358)


Applications of biological or biologically inspired multi-agent systems (MAS) often assume a certain level of reliability and robustness, which is not always straightforward. Formal modelling and verification of MAS may present many interesting challenges. For instance, formal verification may be cumbersome or even impossible to be applied on models with increased complexity. On the other hand, the behaviour of MAS consists of communities evolving in space and time (such as social insects, tissues, colonies of bacteria, etc.) which are characterised with a highly dynamic structure. In order to provide a neat and effective way to modelling and verification of these systems, we focus on their spatial characteristics. Spatial agents (i.e. agents distributed and moving through a physical space) can be modelled with X-machines – one of the most prominent formalisms for modelling the behaviour of biological colonies. However, it will be demonstrated that there are certain problems in the X-machines models, common to every spatial MAS. To overcome these disadvantages, we introduce an X-machines variation that besides facilitating formal modelling, will provide grounds towards visual animation of these systems. This approach resulted into a novel progression, Spatial X-machines ( sp XM), without retracting the legacy characteristics of X-machines such as testing and verification strategies. Finally, we present a supporting framework to modelling and verification of spatial multi-agent system, by utilizing the Spatial X-machines approach.


Formal modelling X-machines Spatial agents 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Spivey, M.: The Z Notation: A Reference Manual. Prentice-Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  2. 2.
    Jones, C.B.: Systematic Software Development using VDM, 2nd edn. Prentice-Hall, Englewood Cliffs (1990)zbMATHGoogle Scholar
  3. 3.
    Holcombe, M.: X-machines as a basis for dynamic system specification. Software Engineering Journal, 69–76 (1988)Google Scholar
  4. 4.
    Reisig, W.: Petri nets: An introduction. EATCS Monographs on Theoretical Computer Science. Springer, Berlin (1985)zbMATHGoogle Scholar
  5. 5.
    Pageau, J., Bédard, Y., Caron, C.: Spatial data modeling: The Modul-R formalism and CASE technology. In: ISPRS Symposium, Washington, United-States, August 1-14 (1992)Google Scholar
  6. 6.
    Cardelli, L., Gardner, P.: Processes in Space. In: Ferreira, F., Löwe, B., Mayordomo, E., Mendes Gomes, L. (eds.) CiE 2010. LNCS, vol. 6158, pp. 78–87. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  7. 7.
    Romero-Campero, F.J., Twycross, J., Camara, M., Bennett, M., Gheorghe, M., Krasnogor, N.: Modular assembly of cell systems biology models using P Systems. International Journal of Foundations of Computer Science, 427–442 (2009)Google Scholar
  8. 8.
    Petreska, I., Kefalas, P.: Population p systems with moving active cells. In: Gheorghe, M., Păun, G., Verlan, S. (eds.) Twelfth International Conference on Membrane Computing (CMC12), pp. 421–432. Laboratoire d’Algorithmique Complexité et Logique of the University of Paris Est – Créteil Val de Marne, Fontainebleau (2011)Google Scholar
  9. 9.
    Pogson, M., Holcombe, M., Smallwood, R., Qwarnstrom, E.: Introducing spatial information into predictive NF-kB modelling – An agent-based approach. PLoS ONE 3(6), e2367 (2008)CrossRefGoogle Scholar
  10. 10.
    Kefalas, P., Eleftherakis, G., Sotiriadou, A.: Developing tools for formal methods. In: Proceedings of the 9th Panehellenic Conference in Informatics (2002)Google Scholar
  11. 11.
    Kefalas, P., Kapeti, E.: A design language and tool for X-machines specification. In: Fotiadis, D.I., Nikolopoulos, S.D. (eds.) Advances in Informatics, pp. 134–145. World Scientific Publishing Company, Singapore (2000)Google Scholar
  12. 12.
    Kefalas, P., Holcombe, M., Eleftherakis, G., Gheorge, M.: A formal method for the development of agent based systems. In: Plekhanova, V. (ed.) Intelligent Agent Software Engineering, pp. 68–98. Idea Group Publishing Co. (2003)Google Scholar
  13. 13.
    Kefalas, P., Eleftherakis, G., Kehris, E.: Communicating X-machines: A practical approach for formal and modular specification of large systems. Information and Software Technology 45, 269–280 (2003)CrossRefGoogle Scholar
  14. 14.
    Kefalas, P.: Formal Modelling of Reactive Agents as an Aggregation of Simple Behaviours. In: Vlahavas, I.P., Spyropoulos, C.D. (eds.) SETN 2002. LNCS (LNAI), vol. 2308, pp. 461–472. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  15. 15.
    Petreska, I., Kefalas, P., Gheorghe, M.: A framework towards the verification of emergent properties in spatial multi-agent systems. In: Ivanovi, M., Ganzha, M., Paprzycki, M., Badica, C. (eds.) Proceedings of the Workshop on Applications of Software Agents, pp. 37–44. Department of Mathematics and Informatics Faculty of Sciences, University of Novi Sad, Serbia (2011)Google Scholar
  16. 16.
    Eleftherakis, G., Kefalas, P.,, S.: XmCTL: Extending temporal logic to facilitate formal verification of X-machines. Matematica-Informatica, 79–95 (2002)Google Scholar
  17. 17.
    Ipate, F., Holcombe, M.: Specification and testing using generalised machines: a presentation and a case study. In: Software Testing, Verification and Reliability, pp. 61–81 (1998)Google Scholar
  18. 18.
    Wilensky, U.: NetLogo. Center for Connected Learning and Computer-Based Modeling, Northwestern Univ., Evanston, IL (1999),
  19. 19.
    Stamatopoulou, I., Kefalas, P., Gheorghe, M.: OPERAS: A Framework for the Formal Modelling of Multi-Agent Systems and Its Application to Swarm-Based Systems. In: Artikis, A., O’Hare, G.M.P., Stathis, K., Vouros, G.A. (eds.) ESAW 2007. LNCS (LNAI), vol. 4995, pp. 158–174. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  20. 20.
    Wilensky, U.: NetLogo Segregation model. Center for Connected Learning and Computer-Based Modeling, Northwestern Univ., Evanston, IL (1997),
  21. 21.
    Collier, N.T., North, M.J.: Repast SC++: A platform for large-scale agent-based modeling. In: Large-Scale Computing Techniques for Complex System Simulations. Wiley (2011) (in press)Google Scholar
  22. 22.
    Petreska, I., Kefalas, P., Gheorghe, M.: Tools for simulating spatial mas. In: Proceedings of the 7th Annual SEERC Doctoral Student Conference, DSC 2012 (2012) (in print)Google Scholar
  23. 23.
    Petreska, I., Kefalas, P., Gheorghe, M.: Informal verification by visualisation of state-based formal models. In: Proceedings of the 6th Annual SEERC Doctoral Student Conference, DSC 2011, Thessaloniki, Greece, pp. 309–319 (September 2011)Google Scholar
  24. 24.
    Qwarnstrom, E., Pogson, M., Smallwood, R., Holcombe, M.: Formal agent-based modelling of intracellular chemical interactions. Biosystems 85, 37–45 (2006)CrossRefGoogle Scholar
  25. 25.
    Holcombe, M., Smallwood, R., Walker, D.: Development and validation of computational models of cellular interaction. Journal of Molecular Histology 35, 659–665 (2004)CrossRefGoogle Scholar
  26. 26.
    Michael, D.E., William, G.G., Yoshio, K., Notkin, D.: Dynamically discovering pointer-based program invariants. Technical Report UW-CSE-99-11-02, University of Washington Department of Computer Science and Engineering, Seattle, WA (November 1999) (revised March 17, 2000)Google Scholar
  27. 27.
    Holzmann, G.J.: The model checker spin. IEEE IFans. on Software Engineering, 279–295 (1997)Google Scholar
  28. 28.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic Symbolic Model Checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002)Google Scholar
  29. 29.
    McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Englewood Cliffs (1993)zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Isidora Petreska
    • 1
  • Petros Kefalas
    • 2
  • Marian Gheorghe
    • 3
  • Ioanna Stamatopoulou
    • 2
  1. 1.South East European Research Centre (SEERC)ThessalonikiGreece
  2. 2.CITY CollegeInternational Faculty of the University of SheffieldThessalonikiGreece
  3. 3.Dept. of Computer ScienceUniversity of SheffieldSheffieldU.K.

Personalised recommendations