On the use of Bio-PEPA for modelling and analysing collective behaviours in swarm robotics
Tóm tắt
In this paper we analyse a swarm robotics system using Bio-PEPA. Bio-PEPA is a process algebra language originally developed to analyse biochemical systems. A swarm robotics system can be analysed at two levels: the macroscopic level, to study the collective behaviour of the system, and the microscopic level, to study the robot-to-robot and robot-to-environment interactions. In general, multiple models are necessary to analyse a system at different levels. However, developing multiple models increases the effort needed to analyse a system and raises issues about the consistency of the results. Bio-PEPA, instead, allows the researcher to perform stochastic simulation, fluid flow (ODE) analysis and statistical model checking using a single description, reducing the effort necessary to perform the analysis and ensuring consistency between the results. Bio-PEPA is well suited for swarm robotics systems: by using Bio-PEPA it is possible to model distributed systems and their space-time characteristics in a natural way. We validate our approach by modelling a collective decision-making behaviour.
Tài liệu tham khảo
Aldini, A., Bernardo, M., & Corradini, F. (2010). A process algebraic approach to software architecture design. Heidelberg: Springer.
Aziz, A., Sanwal, K., Singhal, V., & Brayton, R. (2000). Model checking continuous time Markov chains. ACM Transactions on Computational Logic, 1(1), 162–170.
Baier, C., Katoen, J.-P., & Hermanns, H. (1999). Approximate symbolic model checking of continuous-time Markov chains. In Lecture notes in computer science: Vol. 1664. Concur ’99 (pp. 146–162). Heidelberg: Springer.
Benkirane, S., Norman, R., Scott, E., & Shankland, C. (2012). Measles epidemics and PEPA: an exploration of historic disease dynamics using process algebra. In D. Giannakopoulou & D. Méry (Eds.), Lecture notes in computer science: Vol. 7436. FM 2012: formal methods (pp. 101–115). Berlin: Springer.
Bergstra, J., Ponse, A., & Smolka, S. (Eds.) (2001). Handbook of process algebra. Amsterdam: Elsevier.
Bornstein, B., Doyle, J., Finney, A., Funahashi, A., Hucka, M., Keating, S., Kovitz, H. K. B., Matthews, J., Shapiro, B., & Schilstra, M. (2004). Evolving a lingua franca and associated software infrastructure for computational systems biology: the systems biology markup language (SBML) project. Systems Biology, 1, 4153.
Bortolussi, L., & Hillston, J. (2012). Fluid model checking. In M. Koutny & I. Ulidowski (Eds.), Lecture notes in computer science: Vol. 7454. CONCUR (pp. 333–347). Berlin: Springer.
Brambilla, M., Pinciroli, C., Birattari, M., & Dorigo, M. (2012). Property-driven design for swarm robotics. In Proceedings of 11th international conference on autonomous agents and multiagent systems (AAMAS 2012) (pp. 139–146). IFAAMAS.
Brambilla, M., Ferrante, E., Birattari, M., & Dorigo, M. (2013). Swarm robotics: a review from the swarm engineering perspective. Swarm Intelligence, 7(1), 1–41.
Burch, J., Clarke, E., McMillan, K., & Dill, D. (1990). Sequential circuit verification using symbolic model checking. In Proceedings of the 27th design automation conference (pp. 46–51). Washington: IEEE Press.
Ciocchetta, F., & Hillston, J. (2008). Bio-PEPA: an extension of the process algebra PEPA for biochemical networks. Electronic Notes in Theoretical Computer Science, 194(3), 103–117.
Ciocchetta, F., & Hillston, J. (2009). Bio-PEPA: a framework for the modelling and analysis of biological systems. Theoretical Computer Science, 410(33–34), 3065–3084.
Ciocchetta, F., & Hillston, J. (2012). Bio-PEPA http://www.biopepa.org. Last checked on October 2012.
Ciocchetta, F., Duguid, A., Gilmore, S., Guerriero, M. L., & Hillston, J. (2009). The Bio-PEPA tool suite. In Proceedings of the 6th international conference on quantitative evaluation of SysTems (QEST 2009) (pp. 309–310). Washington: IEEE Computer Society.
Clarke, E. M., Emerson, E. A., & Sifakis, J. (2009). Model checking: algorithmic verification and debugging. Communications of the ACM, 52(11), 74–84.
Dixon, C., Winfield, A., & Fisher, M. (2011). Towards temporal verification of emergent behaviours in swarm robotic systems. In Lecture notes in computer science: Vol. 6856. Towards autonomous robotic systems (pp. 336–347). Heidelberg: Springer.
Eaton, J. W. (2002). GNU octave manual. London: Network Theory Ltd.
Evans, W., Mermoud, G., & Martinoli, A. (2010). Comparing and modeling distributed control strategies for miniature self-assembling robots. In IEEE international conference on robotics and automation (ICRA) (pp. 1438–1445).
Gilat, A. (2004). MATLAB: an introduction with applications (2nd ed.). New York: Wiley.
Gillespie, D. T. (1977). Exact stochastic simulation of coupled chemical reactions. Journal of Physical Chemistry, 81(25), 2340–2361.
Goss, S., Aron, S., Deneubourg, J.-L., & Pasteels, J. (1989). Self-organized shortcuts in the Argentine ant. Naturwissenschaften, 76, 579–581.
Havelund, K., Lowry, M., & Penix, J. (2001). Formal analysis of a space-craft controller using spin. IEEE Transactions on Software Engineering, 27(8), 749–765.
Hermanns, H., Herzog, U., & Katoen, J.-P. (2002). Process algebra for performance evaluation. Theoretical Computer Science, 274(1–2), 43–87.
Hillston, J. (1996). Distinguished dissertation in computer science: A compositional approach to performance modelling. Cambridge: Cambridge University Press.
Hillston, J. (2005). Fluid flow approximation of PEPA models. In Proceedings of the 2th international conference on quantitative evaluation of SysTems (QEST 2005) (pp. 33–43). Washington: IEEE Computer Society.
Holzmann, G. J. (1991). Design and validation of computer protocols. Upper Saddle River: Prentice-Hall
Kleinrock, L. (1975). Queueing systems: Vol. 1. Theory. New York: Wiley.
Konur, S., Dixon, C., & Fisher, M. (2012). Analysing robot swarm behaviour via probabilistic model checking. Robotics and Autonomous Systems, 60(2), 199–213.
Kurtz, T. (1970). Solutions of ordinary differential equations as limits of pure jump Markov processes. Journal of Applied Probability, 7, 49–58.
Kwiatkowska, M., Norman, G., & Parker, D. (2011). PRISM 4.0: verification of probabilistic real-time systems. In Lecture notes in computer science: Vol. 6806. Proceedings of 23rd international conference on computer aided verification (CAV’11) (pp. 585–591). Heidelberg: Springer.
Lerman, K., Martinoli, A., & Galstyan, A. (2005). A review of probabilistic macroscopic models for swarm robotic systems. In Lecture notes in computer science: Vol. 3342. Swarm robotics (pp. 143–152). Heidelberg: Springer.
Martinoli, A., Easton, K., & Agassounon, W. (2004). Modeling swarm robotic systems: a case study in collaborative distributed manipulation. International Journal of Robotics Research, 23(4–5), 415–436.
Massink, M., & Latella, D. (2012). Fluid analysis of foraging ants. In M. Sirjani (Ed.), Lecture notes in computer science: Vol. 7274. Coordination (pp. 152–165). Heidelberg: Springer.
Massink, M., Latella, D., Bracciali, A., & Hillston, J. (2011a). Modelling non-linear crowd dynamics in Bio-PEPA. In D. Giannakopoulou & F. Orejas (Eds.), Lecture notes in computer science: Vol. 6603. FASE (pp. 96–110). Heidelberg: Springer.
Massink, M., Latella, D., Bracciali, A., & Hillston, J. (2011b). Modelling non-linear crowd dynamics in Bio-PEPA. In Lecture notes in computer science: Vol. 6603. Fundamental approaches to software engineering (pp. 96–110). Heidelberg: Springer.
Massink, M., Brambilla, M., Latella, D., Dorigo, M., & Birattari, M. (2012a). Analysing robot swarm decision-making with Bio-PEPA: complete data. Supplementary information page at http://iridia.ulb.ac.be/supp/IridiaSupp2012-012/.
Massink, M., Brambilla, M., Latella, D., Dorigo, M., & Birattari, M. (2012b). Analysing robot swarm decision-making with Bio-PEPA. In Lecture notes in computer science: Vol. 7461. Swarm intelligence (pp. 25–36). Heidelberg: Springer.
Massink, M., Latella, D., Bracciali, A., Harrison, M., & Hillston, J. (2012c). Scalable context-dependent analysis of emergency egress models. Formal Aspects of Computing, 24(2), 267–302. doi:10.1007/s00165-011-0188-1. Published online: 03 July 2011.
Mather, T., & Hsieh, M. (2012). Ensemble synthesis of distributed control and communication strategies. In IEEE international conference on robotics and automation (ICRA) (pp. 4248–4253).
Montes de Oca, M. A., Ferrante, E., Scheidler, A., Pinciroli, C., Birattari, M., & Dorigo, M. (2011). Majority-rule opinion dynamics with differential latency: a mechanism for self-organized collective decision-making. Swarm Intelligence, 5(3–4), 305–327.
Napp, N., Burden, S., & Klavins, E. (2011). Setpoint regulation for stochastically interacting robots. Autonomous Robots, 30, 57–71.
Nimal, V. (2010). Statistical approaches for probabilistic model checking. MSc mini-project dissertation, Oxford University Computing Laboratory
Sahin, E. (2005). Swarm robotics: from sources of inspiration to domains of application. In Lecture notes in computer science: Vol. 3342. Swarm robotics (pp. 10–20). Heidelberg: Springer.
Scheidler, A. (2011). Dynamics of majority rule with differential latencies. Physical Review E, 83, 031116.
Tribastone, M., Gilmore, S., & Hillston, J. (2012). Scalable differential analysis of process algebra models. IEEE Transactions on Software Engineering, 38(1), 205–219.
Tschaikowski, M., & Tribastone, M. (2012). Exact fluid lumpability for Markovian process algebra. In M. Koutny & I. Ulidowski (Eds.), Lecture notes in computer science: Vol. 7454. CONCUR 2012—concurrency theory: 23rd international conference (pp. 380–394). Heidelberg: Springer.
Valentini, G., Birattari, M., & Dorigo, M. (2013). Majority rule with differential latency: an absorbing Markov chain to model consensus. In European conference on complex systems (ECCS’12).
Younes, H. L. S., Kwiatkowska, M. Z., Norman, G., & Parker, D. (2006). Numerical vs. statistical probabilistic model checking. International Journal on Software Tools for Technology Transfer, 8(3), 216–228.
Zarzhitsky, D., Spears, D., Thayer, D., & Spears, W. (2005). Agent-based chemical plume tracing using fluid dynamics. In M. Hinchey, J. Rash, W. Truszkowski, & C. Rouff (Eds.), Lecture notes in computer science: Vol. 3228. Formal approaches to agent-based systems (pp. 146–160). Heidelberg: Springer.