Simulation and Verification in a Process Calculus for Spatially-Explicit Ecological Models

Published in Volume XXIII, Issue 1, 2013, pages 119-167, doi: 10.7561/SACS.2013.1.119

Authors: A. Philippou, M. Toro, M. Antonaki

Abstract

We propose PALPS, a Process Algebra with Locations for Population Systems. PALPS allows us to produce spatially-explicit individual-based ecological models and to reason about their behavior. PALPS has two abstraction levels: At the first level, we may define the behavior of an individual of a population and, at the second level, we may specify a system as the collection of individuals of various species located in space. In PALPS, the individuals move through their life cycle while changing their location and interact with each other in various ways such as predation, infection or mating. Furthermore, we propose a translation of a subset of PALPS into the probabilistic model checker PRISM. We illustrate our framework via models of dispersal in metapopulations and by applying PRISM on PALPS models for verifying temporal logic properties and conducting reachability and steady-state analysis.

Full Text (PDF)

References

[1] Online PRISM documentation. http://www.prismmodelchecker.org/doc/ .

[2] M. Antonaki. A probabilistic process algebra and a simulator for modeling population systems. Master’s thesis, University of Cyprus, 2012 .

[3] R. Barbuti, A. Maggiolo-Schettini, P. Milazzo, and G. Pardini. Spatial calculus of looping sequences. Theoretical Computer Science, 412(43):5976–6001, 2011. http://dx.doi.org/10.1016/j.tcs.2011.01.020 .

[4] Roberto Barbuti, Andrea Maggiolo-Schettini, Paolo Milazzo, and Angelo Troina. A calculus of looping sequences for modelling microbiological systems. Fundamenta Informaticae, 72(1-3):21–35, 2006 .

[5] L. Berec. Techniques of spatially explicit individual-based models: construction, simulation, and mean-field analysis. Ecological Modeling, 150:55–81, 2002. http://dx.doi.org/10.1016/S0304-3800(01)00463-X .

[6] D. Besozzi, P. Cazzaniga, D. Pescini, and G. Mauri. Modelling metapopulations with stochastic membrane systems. BioSystems, 91(3):499–514, 2008. http://dx.doi.org/10.1016/j.biosystems.2006.12.011 .

[7] D. Besozzi, P. Cazzaniga, D. Pescini, and G. Mauri. An analysis on the influence of network topologies on local and global dynamics of metapopulation systems. In Proceedings of AMCA-POP’10, pages 1– 17, 2010. http://dx.doi.org/10.4204/EPTCS.33.1 .

[8] A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In Proceedings of FSTTCS’95, LNCS 1026, pages 499–513. Springer, 1995. http://dx.doi.org/10.1007/3-540-60692-0_70 .

[9] Livio Bioglio, Cristina Calcagno, Mario Coppo, Ferruccio Damiani, Eva Sciacca, Salvatore Spinella, and Angelo Troina. A Spatial Calculus of Wrapped Compartments. CoRR, abs/1108.3426, 2011 .

[10] L. Cardelli. Brane calculi – interactions of biological membranes. In Proceedings of CMSB’04, LNCS 3082, pages 257–278. Springer, 2005. http://dx.doi.org/10.1007/978-3-540-25974-9_24 .

[11] Luca Cardelli and Radu Mardare. Stochastic Pi-Calculus Revisited. Technical report, Microsoft Research, Cambridge, UK, 2012 .

[12] M. Cardona, M. Colomer, A. Margalida, I. Pérez-Hurtado, M. J. Pérez-Jiménez, and D. Sanuy. A P system based model of an ecosystem of the scavenger birds. In Proceedings of WMC’09, LNCS 5957, pages 182–195. Springer, 2009. http://dx.doi.org/10.1007/978-3-642-11467-0_14 .

[13] Mónica Cardona, M. Angels Colomer, Antoni Margalida, Antoni Palau, Ignacio Pérez-Hurtado, Mario J. Pérez-Jiménez, and Delfí Sanuy. A computational modeling for real ecosystems based on P systems. Natural Computing, 10(1):39–53, 2011. http://dx.doi.org/10.1007/s11047-010-9191-3 .

[14] P. Cazzaniga, D. Pescini, D. Besozzi, and G. Mauri. Tau leaping stochastic simulation method in P systems. In Proceedings of WMC’06, LNCS 4361, pages 298–313. Springer, 2006. http://dx.doi.org/10.1007/11963516_19 .

[15] Qiuwen Chen, Fei Ye, and Weifeng Li. Cellular-automata-based ecological and ecohydraulics modelling. Journal of Hydroinformatics, 11(3- 4):252–265, 2009. http://dx.doi.org/10.2166/hydro.2009.026 .

[16] Federica Ciocchetta and Jane Hillston. Bio-PEPA: A framework for the modelling and analysis of biological systems. Theoretical Computer Science, 410(33–34):3065–3084, 2009. http://dx.doi.org/10.1016/j.tcs.2009.02.037 .

[17] Rocco De Nicola, Diego Latella, Michele Loreti, and Mieke Massink. Rate-based transition systems for stochastic process calculi. In Proceedings of ICALP (2), LNCS 5556, pages 435–446. Springer, 2009. http://dx.doi.org/10.1007/978-3-642-02930-1_36 .

[18] V. Forejt, M. Kwiatkowska, G. Norman, and D. Parker. Automated verification techniques for probabilistic systems. In Proceedings of SFM’11, LNCS 6659, pages 53–113. Springer, 2011. http://dx.doi.org/10.1007/978-3-642-21455-4_3 .

[19] S. C. Fu and G. Milne. A flexible automata model for disease simulation. In Proceedings of ACRI’04, LNCS 3305, pages 642–649. Springer, 2004. http://dx.doi.org/10.1007/978-3-540-30479-1_66 .

[20] V. Galpin. Modelling network performance with a spatial stochastic process algebra. In Proceedings of AINA’09, pages 41–49. IEEE Computer Society, 2009. http://dx.doi.org/10.1109/AINA.2009.75 .

[21] L. R. Gerber and G. R. VanBlaricom. Implications of three viability models for the conservation status of the western population of steller sea lions (Eumetopias jubatus). Biological Conservation, 102(3):261– 269, 2001. http://dx.doi.org/10.1016/S0006-3207(01)00104-5 .

[22] D. T. Gillespie. Exact stochastic simulation of coupled chemical reactions. Journal of Physical Chemistry, 81:2340–2361, 1977. http://dx.doi.org/10.1021/j100540a008 .

[23] D. T. Gillespie and L.R. Petzold. Approximate accelerated stochastic simulation of chemically reacting systems. Journal of Chemical Physics, 115:1716–1733, 2001. http://dx.doi.org/10.1063/1.1378322 .

[24] Stephen Gilmore and Jane Hillston. The PEPA workbench: A tool to support a process algebra-based approach to performance modelling. In Proceedings of Computer Performance Evaluation Modelling Techniques and Tools’94, LNCS 794, pages 353–368, 1994. http://dx.doi.org/10.1007/3-540-58021-2_20 .

[25] C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985 .

[26] M. Jeschke, R. Ewald, and A. Uhrmacher. Exploring the performance of spatial stochastic simulation algorithms. Journal of Computational Physics, 230(7):2562–2574, 2011. http://dx.doi.org/10.1016/j.jcp.2010.12.030 .

[27] D. Kouzapas and A. Philippou. A process calculus for dynamic networks. In Proceedings of FMOODS/FORTE’11, LNCS 6722, pages 213–227. Springer, 2011. http://dx.doi.org/10.1007/978-3-642-21461-5_14 .

[28] Tomas Krilaviˇcius and Helen Schonenberg. Discrete Simulation of Behavioural Hybrid Process Calculus. In Proceedings of IFM 2005, pages 33–38, 2005. URL: http://doc.utwente.nl/54779/ .

[29] C. McCaig, R. Norman, and C. Shankland. Process algebra models of population dynamics. In Proceedings of AB’08, LNCS 5147, pages 139–155. Springer, 2008. http://dx.doi.org/10.1007/978-3-540-85101-1_11 .

[30] Chris McCaig, Rachel Norman, and Carron Shankland. From individuals to populations: A mean field semantics for process algebra. Theoretical Computer Science, 412(17):1557–1580, 2011. http://dx.doi.org/10.1016/j.tcs.2010.09.024 .

[31] R. Milner. A Calculus of Communicating Systems. Springer, 1980.

[32] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, parts 1 and 2. Information and Computation, 100:1–77, 1992. http://dx.doi.org/10.1016/0890-5401(92)90008-4 .

[33] E. S. Minor, R. I. McDonald, E. A. Treml, and D. L. Urban. Uncertainty in spatially explicit population models. Biological Conservation, 141(4):956–970, 2008. http://dx.doi.org/10.1016/j.biocon.2007.12.032 .

[34] Gethin Norman, Catuscia Palamidessi, David Parker, and Peng Wu. Model Checking Probabilistic and Stochastic Extensions of the π- Calculus. IEEE Transactions on Software Engineering, 35(2):209–223, March 2009. http://dx.doi.org/10.1109/TSE.2008.77 .

[35] G. Pardini. Formal Modelling and Simulation of Biological Systems with Spatiality. PhD thesis, University of Pisa, 2011 .

[36] R. G. Pearson and T. P. Dawson. Long-distance plant dispersal and habitat fragmentation: identifying conservation targets for spatial landscape planning under climate change. Biological Conservation, 123:389– 401, 2005. http://dx.doi.org/10.1016/j.biocon.2004.12.006 .

[37] Mario J. Pérez-Jiménez and Francisco José Romero-Campero. A study of the robustness of the EGFR signalling cascade using continuous membrane systems. In Proceedings of IWINAC’05, LNCS 3561, pages 268– 278, 2005. http://dx.doi.org/10.1007/11499220_28 .

[38] D. Pescini, D. Besozzi, G. Mauri, and C. Zandron. Dynamical probabilistic P-systems. International Journal of Foundations of Computer Science, 17(1):183–204, 2006. http://dx.doi.org/10.1142/S0129054106003760 .

[39] Anna Philippou and David Walker. On confluence in the π-calculus. In Proceedings of ICALP ’97, LNCS 1256, pages 314–324. Springer, 1997. http://dx.doi.org/10.1007/3-540-63165-8_188 .

[40] Gheorghe Păun. Computing with Membranes (P Systems): An Introduction. In Current Trends in Theoretical Computer Science, pages 845–866. World Scientific, 2001 .

[41] Aviv Regev, Ekaterina M. Panina, William Silverman, Luca Cardelli, and Ehud Shapiro. BioAmbients: an abstraction for biological compartments. Theoretical Computer Science, 325(1):141–167, September 2004. http://dx.doi.org/10.1016/j.tcs.2004.03.061 .

[42] Antoine Spicher, Olivier Michel, Mikolaj Cieslak, Jean-Louis Giavitto, and Przemyslaw Prusinkiewicz. Stochastic P systems and the simulation of biochemical processes with dynamic compartments. Biosystems, 91(3):458–472, 2008. http://dx.doi.org/10.1016/j.biosystems.2006.12.009 .

[43] D. J. T. Sumpter, G. B. Blanchard, and D. S. Broomhear. Ants and agents: a process algebra approach to modelling ant colony behaviour. Bulletin of Mathematical Biology, 63(5):951–980, 2001. http://dx.doi.org/10.1006/bulm.2001.0252 .

[44] D. J. T. Sumpter and D. S. Broomhead. Relating individual behaviour to population dynamics. Proceedings of of Royal Society B: Biological Sciences, 268(1470):925–932, 2001. http://dx.doi.org/10.1098/rspb.2001.1604 .

[45] C. Tofts. Processes with probabilities, priority and time. Formal Aspects of Computing, 6:536–564, 1994. http://dx.doi.org/10.1007/BF01211867 .

[46] J. M. J. Travis and C. Dytham. The evolution of disperal in a metapopulation: a spatially explicit, individual-based model. Proceedings: Biological Sciences, 265(1390):17–23, 1998. http://dx.doi.org/10.1098/rspb.1998.0258 .

[47] D. L. Urban and H. H. Shugart. Avian demography in mosaic landscapes: modeling paradigm and preliminary results. Wildlife 2000: Modeling Habitat Relationships of Terrestrial Vertebrates, pages 273– 279, 1986.

Bibtex

@article{sacscuza:philippou2013saviapcfsem,
  title={Simulation and Verification in a Process Calculus for Spatially-Explicit Ecological Models},
  author={A. Philippou and M. Toro and M. Antonaki},
  journal={Scientific Annals of Computer Science},
  volume={23},
  number={1},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  year={2013},
  pages={119--167},
  doi={10.7561/SACS.2013.1.119},
  publisher={``A.I. Cuza'' University Press}
}