[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
article

Towards temporal verification of swarm robotic systems

Published: 01 November 2012 Publication History

Abstract

A robot swarm is a collection of simple robots designed to work together to carry out some task. Such swarms rely on the simplicity of the individual robots; the fault tolerance inherent in having a large population of identical robots; and the self-organised behaviour of the swarm as a whole. Although robot swarms present an attractive solution to demanding real-world applications, designing individual control algorithms that can guarantee the required global behaviour is a difficult problem. In this paper we assess and apply the use of formal verification techniques for analysing the emergent behaviours of robotic swarms. These techniques, based on the automated analysis of systems using temporal logics, allow us to analyse whether all possible behaviours within the robot swarm conform to some required specification. In particular, we apply model-checking, an automated and exhaustive algorithmic technique, to check whether temporal properties are satisfied on all the possible behaviours of the system. We target a particular swarm control algorithm that has been tested in real robotic swarms, and show how automated temporal analysis can help to refine and analyse such an algorithm.

References

[1]
Yuh, J., Design and control of autonomous underwater robots: a survey. Autonomous Robots. v8 i1. 7-24.
[2]
Editorial: advances in multi-robot systems. IEEE Transactions on Robotics and Automation. v18 i5. 655-661.
[3]
Truszkowski, W., Hallock, H., Rouff, C., Karlin, J., Rash, J., Hinchey, M. and Sterritt, R., Swarms in space missions. In: NASA Monographs in Systems and Software Eng., Springer. pp. 207-221.
[4]
Bonabeau, E., Dorigo, M. and Theraulaz, G., Swarm intelligence: from natural to artificial systems. Journal of Artificial Societies and Social Simulation. v4 i1.
[5]
Beni, G., From swarm intelligence to swarm robotics. In: Lecture Notes in Computer Science, vol. 3342. Springer. pp. 1-9.
[6]
Sahin, E. and Winfield, A.F.T., Special issue on swarm robotics. Swarm Intelligence. v2 i2-4. 69-72.
[7]
Spears, W.M., Spears, D.F., Hamann, J.C. and Heil, R., Distributed, physics-based control of swarms of vehicles. Autonomous Robots. v17 i2-3. 137-162.
[8]
Støy, K., Using situated communication in distributed autonomous mobile robotics. In: SCAI'01: Proceedings of the Seventh Scandinavian Conference on Artificial Intelligence, IOS Press. pp. 44-52.
[9]
J. Nembrini, Minimalist coherent swarming of wireless networked autonomous mobile robots, Ph.D. Thesis, University of the West of England, 2005.
[10]
Clarke, E., Grumberg, O. and Peled, D.A., Model Checking. 2000. MIT Press.
[11]
Fainekos, G., Kress-Gazit, H. and Pappas, G., Temporal logic motion planning for mobile robots. In: Proceedings of the IEEE International Conference on Robotics and Automation (ICRA), IEEE Computer Society Press. pp. 2020-2025.
[12]
Dixon, C., Winfield, A. and Fisher, M., Towards temporal verification of emergent behaviours in swarm robotic systems. In: LNCS, vol. 6856. Springer. pp. 336-347.
[13]
Winfield, A., Liu, W., Nembrini, J. and Martinoli, A., Modelling a wireless connected swarm of mobile robots. Swarm Intelligence. v2 i2-4. 241-266.
[14]
Winfield, A., Sa, J., Fernández-Gago, M.-C., Dixon, C. and Fisher, M., On formal specification of emergent behaviours in swarm robotic systems. International Journal of Advanced Robotic Systems. v2 i4. 363-370.
[15]
D. Chen, A simulation environment for swarm robotic system based on temporal logic specifications, Master's Thesis, University of the West of England, November 2005.
[16]
Behdenna, A., Dixon, C. and Fisher, M., Deductive verification of simple foraging robotic behaviours. International Journal of Intelligent Computing and Cybernetics. v2 i4. 604-643.
[17]
Liu, W., Winfield, A., Sa, J., Chen, J. and Dou, L., Strategies for energy optimisation in a swarm of foraging robots. In: LNCS, vol. 4433. Springer. pp. 14-26.
[18]
Hustadt, U. and Konev, B., TRP++ 2.0: A temporal resolution prover. In: Lecture Notes in Artificial Intelligence, vol. 2741. Springer. pp. 274-278.
[19]
Ludwig, M. and Hustadt, U., Fair derivations in monodic temporal reasoning. In: Lecture Notes in Computer Science, vol. 5663. Springer. pp. 261-276.
[20]
Konur, S., Dixon, C. and Fisher, M., Analysing robot swarm behaviour via probabilistic model checking. Robotics and Autonomous Systems. v60 i2. 199-213.
[21]
Liu, W. and Winfield, A.F.T., Modeling and optimization of adaptive foraging in swarm robotic systems. The International Journal of Robotics Research. v29 i14. 1743-1760.
[22]
Hinton, A., Kwiatkowska, M., Norman, G. and Parker, D., PRISM: a tool for automatic verification of probabilistic systems. In: LNCS, vol. 3920. Springer. pp. 441-444.
[23]
M. Kloetzer, C. Belta, Hierarchical abstractions for robotic swarms, in: Robotics and Automation, 2006, ICRA 2006, Proceedings 2006 IEEE International Conference on, 2006, pp. 952-957.
[24]
Kloetzer, M. and Belta, C., Temporal logic planning and control of robotic swarms by hierarchical abstractions. IEEE Transactions on Robotics. v23. 320-330.
[25]
Jeyaraman, S., Tsourdos, A., Zbikowski, R. and White, B., Kripke modelling approaches of a multiple robots system with minimalist communication: a formal approach of choice. International Journal of Systems Science. v37 i6. 339-349.
[26]
Rouff, C., Vanderbilt, A., Truszkowski, W., Rash, J. and Hinchey, M., Verification of NASA emergent systems. In: Proc. 9th IEEE International Conference on Engineering Complex Computer Systems Navigating Complexity in the e-Engineering Age, IEEE Computer Society Press. pp. 231-238.
[27]
Rouff, C., Hinchey, M., Pena, J. and Ruiz-Cortes, A., Using formal methods and agent-oriented software engineering for modeling NASA swarm-based systems. In: Proc. International Swarm Intelligence Symposium, IEEE Computer Society Press. pp. 348-355.
[28]
C.-C. Chen, S. Nagl, C. Clack, A calculus for multi-level emergent behaviours in component-based systems and simulations, in: Proceedings of Emergent Properties in Artificial and Natural Systems, EPNACS, 2007, pp. 35-51.
[29]
E.M. Clarke, O. Grumberg, Avoiding the state explosion problem in temporal logic model checking, in: ACM Symposium on Principles of Distributed Computing IEEE Transactions On Robotics, PODC, 1987, pp. 294-303.
[30]
. In: Barringer, H., Fisher, M., Gabbay, D., Gough, G. (Eds.), Applied Logic Series, vol. 16. Kluwer.
[31]
. In: Fisher, M., Gabbay, D., Vila, L. (Eds.), Foundations of Artificial Intelligence Series, vol. 1. Elsevier.
[32]
Fisher, M., An Introduction to Practical Formal Methods Using Temporal Logic. 2011. Wiley.
[33]
D. Gabbay, A. Pnueli, S. Shelah, J. Stavi, The temporal analysis of fairness, in: Proceedings of the Seventh ACM Symposium on the Principles of Programming Languages, Las Vegas, Nevada, 1980, pp. 163-173.
[34]
Clarke, E.M. and Emerson, E.A., Design and synthesis of synchronisation skeletons using branching time temporal logic. In: Kozen, D. (Ed.), LNCS, vol. 131. Springer. pp. 52-71.
[35]
Holzmann, G.J., The Spin Model Checker: Primer and Reference Manual. 2003. Addison-Wesley.
[36]
A. Cimatti, E.M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, A. Tacchella, NuSMV 2: an opensource tool for symbolic model checking, in: Proceedings of International Conference on Computer-Aided Verification, CAV, 2002, pp. 359-364.
[37]
Visser, W., Havelund, K., Brat, G. and Park, S., Model checking programs. In: Proc. 15th IEEE International Conference on Automated Software Engineering, IEEE Computer Society Press. pp. 3-12.
[38]
Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P. and Yi, W., Uppaal-a tool suite for automatic verification of real-time systems. In: LNCS, vol. 1066. Springer. pp. 232-243.
[39]
Henzinger, T., Ho, P.-H. and Wong-Toi, H., HYTECH: a model checker for hybrid systems. International Journal on Software Tools for Technology Transfer. v1 i1-2. 110-122.
[40]
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y. and Veith, H., Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM. v50 i5. 752-794.
[41]
Alur, R., Dang, T. and Ivančić, F., Counterexample-guided predicate abstraction of hybrid systems. Theoretical Computer Science. v354 i2. 250-271.
[42]
S. Tisue, U. Wilensky, Netlogo: design and implementation of a multi-agent modeling environment, in: Proc. Agent 2004, 2004, pp. 7-9.
[43]
C. Zeng, Simulation and verification of robot swarms, Master's Thesis, University of Liverpool, 2011.
[44]
Miller, A., Donaldson, A. and Calder, M., Symmetry in temporal logic model checking. ACM Computing Surveys. v38 i3.
[45]
. In: Grumberg, O., Veith, H. (Eds.), LNCS, vol. 5000. Springer.
[46]
Baier, C. and Katoen, J.-P., Principles of Model Checking. 2008. MIT Press.
[47]
J.D. Bjerknes, Scaling and fault tolerance in self-organised swarms of mobile robots, Ph.D. Thesis, University of the West of England, 2010.

Cited By

View all
  • (2022)Reasoning about Human-Friendly Strategies in Repeated Keyword AuctionsProceedings of the 21st International Conference on Autonomous Agents and Multiagent Systems10.5555/3535850.3535859(62-71)Online publication date: 9-May-2022
  • (2022)RoboSimVer: A Tool for RoboSim Modeling and AnalysisProceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering10.1145/3551349.3559533(1-4)Online publication date: 10-Oct-2022
  • (2022)Automated extraction and checking of property models from source code for robot swarmsProceedings of the 4th International Workshop on Robotics Software Engineering10.1145/3526071.3527516(47-54)Online publication date: 9-May-2022
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Robotics and Autonomous Systems
Robotics and Autonomous Systems  Volume 60, Issue 11
November, 2012
103 pages

Publisher

North-Holland Publishing Co.

Netherlands

Publication History

Published: 01 November 2012

Author Tags

  1. Emergent behaviour
  2. Formal verification
  3. Model-checking
  4. Swarm robotics
  5. Temporal logics

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)0
  • Downloads (Last 6 weeks)0
Reflects downloads up to 18 Dec 2024

Other Metrics

Citations

Cited By

View all
  • (2022)Reasoning about Human-Friendly Strategies in Repeated Keyword AuctionsProceedings of the 21st International Conference on Autonomous Agents and Multiagent Systems10.5555/3535850.3535859(62-71)Online publication date: 9-May-2022
  • (2022)RoboSimVer: A Tool for RoboSim Modeling and AnalysisProceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering10.1145/3551349.3559533(1-4)Online publication date: 10-Oct-2022
  • (2022)Automated extraction and checking of property models from source code for robot swarmsProceedings of the 4th International Workshop on Robotics Software Engineering10.1145/3526071.3527516(47-54)Online publication date: 9-May-2022
  • (2020)A corroborative approach to verification and validation of human–robot teamsInternational Journal of Robotics Research10.1177/027836491988333839:1(73-99)Online publication date: 1-Jan-2020
  • (2019)Formal Specification and Verification of Autonomous Robotic SystemsACM Computing Surveys10.1145/334235552:5(1-41)Online publication date: 13-Sep-2019
  • (2019)RoboChartSoftware and Systems Modeling (SoSyM)10.1007/s10270-018-00710-z18:5(3097-3149)Online publication date: 1-Oct-2019
  • (2018)Symbolic synthesis of fault-tolerance ratios in parameterised multi-agent systemsProceedings of the 27th International Joint Conference on Artificial Intelligence10.5555/3304415.3304462(324-330)Online publication date: 13-Jul-2018
  • (2017)Verifying fault-tolerance in parameterised multi-agent systemsProceedings of the 26th International Joint Conference on Artificial Intelligence10.5555/3171642.3171684(288-294)Online publication date: 19-Aug-2017
  • (2017)Probabilistic Supervisory Control Theory (pSCT) Applied to Swarm RoboticsProceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems10.5555/3091125.3091317(1395-1403)Online publication date: 8-May-2017
  • (2017)Validation and Verification of Smart Contracts: A Research AgendaComputer10.1109/MC.2017.357104550:9(50-57)Online publication date: 22-Sep-2017
  • Show More Cited By

View Options

View options

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media