ESTONIAN ACADEMY
PUBLISHERS
eesti teaduste
akadeemia kirjastus
PUBLISHED
SINCE 1952
 
Proceeding cover
proceedings
of the estonian academy of sciences
ISSN 1736-7530 (Electronic)
ISSN 1736-6046 (Print)
Impact Factor (2022): 0.9
Model checking of emergent behaviour properties of robot swarms; pp. 48–54
PDF | doi: 10.3176/proc.2011.1.05

Authors
Silver Juurik, Jüri Vain
Abstract
This paper presents a case study on scalability of explicit state model checking. Three state space reduction methods – state vector compression, bit state hashing, and symmetry reduction – were applied on an exercise with the objective of verifying a distributed coordination algorithm for robot swarms. Based on the analysis results, the feasibility of using explicit state model checking to prove properties of large multi-agent systems is questioned and the limitations faced in verifying a dynamic cleaning algorithm are outlined.
References

  1. Altshuler, Y., Bruckelstein, A. M., and Wagner, I. A. Swarm robotics for a dynamic cleaning problem. In IEEE Swarm Intelligence Symposium. 2005, 209–216.
doi:10.1109/SIS.2005.1501624

  2. Baier, C. and Katoen, J.-P. Principles of Model Checking. MIT Press, 2008.

  3. Behrmann, G., David, A., and Larsen, K. G. A tutorial on Uppaal. In Formal Methods for the Design of Real-Time Systems: 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, number 3185 in LNCS (Bernardo, M. and Corradini, F., eds). Springer-Verlag, 2004, 200–236.

  4. Bonabeau, E., Theraulaz, G., Deneubourg, J.-L., Aron, S., and Camazine, S. Self-organization in social insects. Trends in Ecology and Evolution, 1997, 12, 188–193.
doi:10.1016/S0169-5347(97)01048-3

  5. Chandy, K. M. and Sanders, B. A. Reasoning about program composition. Preprint. 1998.

  6. Clarke, E. M., Grumberg, O., and Long, D. E. Model checking and abstraction. ACM T. Progr. Lang. Sys., 1994, 16(5), 1512–1542.
doi:10.1145/186025.186051

  7. Curtis, S. A., Rilee, M. L., Clark, P. E., and Marr, G. C. Use of swarm intelligence in spacecraft constellations for the resource exploration of the asteriod belt. In Proceedings of the Third International Workshop on Satellite Constellations and Formation Flying. 2003, 24–26.

  8. Donaldson, A. TopSPIN 2.2 manual. http://www.\linebreakallydonaldson.co.uk/topspin/TopSPIN\_2.2\_manual.pdf. November 2009.

  9. Eilenberg, S. Automata, Languages and Machines. Vol. A. Academic Press, 1974.

10. Hoare, C. A. R. Communicating sequential processes. Commun. ACM, 1978, 21(8), 666–677.
doi:10.1145/359576.359585

11. Holzmann, G. J. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 2003.

12. Holzmann, G. J. and Peled, D. Partial order reduction of the state space. In First SPIN Workshop. Montreal, Quebec, 1995.

13. Holzmann, G. J. and Puri, A. A minimized automaton representation of reachable states. Software Tools for Technology Transfer, 1999, 2(3), 270–278.
doi:10.1007/s100090050034

14. Lomuscio, A., Pecheur, C., and Raimondi, F. Automatic verification of knowledge and time with NuSMV. In Proceedings of 20th International Joint Conference on Artificial Intelligence. 2007, 1384–1389.

15. Martinoli, A., Easton, K., and Agassounon, W. Modeling swarm robotic systems: a case study in collaborative distributed manipulation. Int. J. Robot. Res., 2004, 23(4), 415–436.
doi:10.1177/0278364904042197

16. Morris, R. Scatter storage techniques. Communications of the ACM, 1968, 11(1), 38–44.
doi:10.1145/362851.362882

17. Rouff, C., Vanderbilt, A., Hinchey, M., Truszkowski, W., and Rash, J. Properties of a formal method for prediction of emergent behaviors in swarm-based systems. In Second International Conference on Soft\-ware Engineering and Formal Methods (SEFM'04). 2004, 24–33.

18. Tofts, C. Describing social insect behaviour using process algebra. Trans. Social Comput. Simul., 1991, 227–283.

19. Vain, J., Tammet, T., Kuusik, A., and Juurik, S. Towards scalable proofs of robot swarm dependability. In Proceedings of BEC 2008. 2008, 199–202.
Back to Issue