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}
}