Abstract
The emergent global behaviours of robotic swarms are important for them to achieve their navigation task goals. These emergent behaviours can be verified to assess their correctness, through techniques like model checking. Model checking exhaustively explores all possible behaviours, based on a discrete model of the system, such as a swarm in a grid. A common problem in model checking is the state-space explosion that arises when the states of the model are numerous. We propose a novel implementation of symmetry reduction, in the form of encoding navigation algorithms relatively with respect to a reference, exploiting the symmetrical properties of swarms in grids. We applied the relative encoding to a swarm navigation algorithm, Alpha, modelled for the NuSMV model checker. A comparison of the state-space and verification results with an absolute (or global) and a relative encoding of the Alpha algorithm highlights the advantages of our approach, allowing model checking both larger grid sizes and higher numbers of robots, and consequently verifying more complex emergent behaviours. For example, a property was verified for a grid with 3 robots and a maximum allowed size of \(8 \times 8\) cells in a global encoding, whereas this size was increased to \(16 \times 16\) using a relative encoding. Also, the time to verify a property for a swarm of 3 robots in a \(6 \times 6\) grid was reduced from almost 10 hours to only 7 minutes. Our approach is transferable to other swarm navigation algorithms.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Appold, C.: Efficient symmetry reduction and the use of state symmetries for symbolic model checking. In: Proc. GandALF, pp. 173–187 (2010)
Bosnacki, D., Dams, D., Holenderski, L.: Symmetric SPIN. In: SPIN Model Checking and Software Verification, Stanford, CA, USA, pp. 1–19 (2000)
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV version 2: an opensource tool for symbolic model checking. In: Computer-Aided Verification, Copenhagen, Denmark. pp. 359–364 (2002)
Clarke Jr, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Clarke, E., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Formal Methods in System Design 9(1–2), 77–104 (1996)
Dixon, C., Winfield, A.F., Fisher, M.: Verification of swarm robots: the Alpha algorithm. In: Proc. ARW, Westminster, UK, pp. 10–11 (2010)
Dixon, C., Winfield, A., Fisher, M.: Towards temporal verification of emergent behaviours in swarm robotic systems. In: Groß, R., Alboul, L., Melhuish, C., Witkowski, M., Prescott, T.J., Penders, J. (eds.) TAROS 2011. LNCS, vol. 6856, pp. 336–347. Springer, Heidelberg (2011)
Dixon, C., Winfield, A.F., Fisher, M., Zeng, C.: Towards temporal verification of swarm robotic systems. In: Robotics and Autonomous Systems, Bristol, UK, pp. 1429–1441 (2012)
Donaldson, A.F., Miller, A.: Automatic symmetry detection for model checking using computational group theory. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 481–496. Springer, Heidelberg (2005)
Emerson, E.A., Wahl, T.: On combining symmetry reduction and symbolic representation for efficient model checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 216–230. Springer, Heidelberg (2003)
Emerson, E.A., Wahl, T.: Dynamic symmetry reduction. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 382–396. Springer, Heidelberg (2005)
Gomes, P.d.C.: Verification of symmetric models using semiautomatic abstractions. Master’s thesis, Computer Science, Belo Horizonte, Brazil (2010)
Juurik, S., Vain, J.: Model checking of emergent behaviour properties of robot swarms. Proceedings of the Estonian Academy of Sciences 60(1), 48–54 (2011)
Kloetzer, M., Belta, C.: Temporal logic planning and control of robotic swarms by hierachical abstractions. IEEE Transactions on Robotics 23(2), 320–330 (2007)
Konur, S., Dixon, C., Fisher, M.: Analysing robot swarm behaviour via probabilistic model checking. Robotics and Autonomous Systems 60, 199–213 (2012)
Kouvaros, P., Lomuscio, A.: A counter abstraction technique for the verification of robot swarms. In: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, January 25–30, 2015, Austin, Texas, USA, pp. 2081–2088 (2015)
Nembrini, J.: Minimalist Coherent Swarming of Wireless Networked Autonomous Mobile Robots. Ph.D. thesis, Bristol, UK (2005)
Norris Ip, C., Dill, D.L.: Better verification through symmetry. Formal Methods in System Design 9(1–2), 41–75 (1996)
Rouff, C., Hinchey, M., Truszkowski, W., Rash, J.: Formal methods for autonomic and swarm-based systems. In: Proc. ISoLA, Paphos, Cyprus, pp. 100–102 (2004)
Winfield, A.F., Sa, J., Fernandez-Gago, M.C., Dixon, C., Fisher, M.: On formal specification of emergent behaviours of swarm robotic systems. International Journal of Advanced Robotic Systems 2(4), 363–370 (2005)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Antuña, L., Araiza-Illan, D., Campos, S., Eder, K. (2015). Symmetry Reduction Enables Model Checking of More Complex Emergent Behaviours of Swarm Navigation Algorithms. In: Dixon, C., Tuyls, K. (eds) Towards Autonomous Robotic Systems. TAROS 2015. Lecture Notes in Computer Science(), vol 9287. Springer, Cham. https://doi.org/10.1007/978-3-319-22416-9_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-22416-9_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-22415-2
Online ISBN: 978-3-319-22416-9
eBook Packages: Computer ScienceComputer Science (R0)