headerpos: 12198
 
 
 

Proceedings of the Estonian Academy of Sciences

ISSN 1736-7530 (electronic)   ISSN 1736-6046 (print)
Formerly: Proceedings of the Estonian Academy of Sciences, series Physics & Mathematics and  Chemistry
Published since 1952

Proceedings of the Estonian Academy of Sciences

ISSN 1736-7530 (electronic)   ISSN 1736-6046 (print)
Formerly: Proceedings of the Estonian Academy of Sciences, series Physics & Mathematics and  Chemistry
Published since 1952
Publisher
Journal Information
» Editorial Board
» Editorial Policy
» Archival Policy
» Article Publication Charges
» Copyright and Licensing Policy
Guidelines for Authors
» For Authors
» Instructions to Authors
» LaTex style files
Guidelines for Reviewers
» For Reviewers
» Review Form
Open Access
List of Issues
» 2018
» 2017
» 2016
» 2015
» 2014
» 2013
» 2012
» 2011
Vol. 60, Issue 4
Vol. 60, Issue 3
Vol. 60, Issue 2
Vol. 60, Issue 1
» 2010
» 2009
» 2008
» Back Issues Phys. Math.
» Back Issues Chemistry
» Back issues (full texts)
  in Google. Phys. Math.
» Back issues (full texts)
  in Google. Chemistry
» Back issues (full texts)
  in Google Engineering
» Back issues (full texts)
  in Google Ecology
» Back issues in ETERA Füüsika, Matemaatika jt
Subscription Information
» Prices
Internet Links
Support & Contact
Publisher
» Staff
» Other journals

Model checking of emergent behaviour properties of robot swarms; pp. 48–54

(Full article in PDF format) 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.

Keywords

model checking, emerging behaviour properties, robot swarm, distributed coordination algorithm.

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

Current Issue: Vol. 67, Issue 3 in Press, 2018




Publishing schedule:
No. 1: 20 March
No. 2: 20 June
No. 3: 20 September
No. 4: 20 December