Parameterized verification of algorithms for oblivious robots on a ring

DOI10.1007/S10703-019-00335-YzbMATH Open1506.68058arXiv1706.05193OpenAlexW2625145304MaRDI QIDQ2225474FDOQ2225474

Authors: Arnaud Sangnier, Nathalie Sznajder, Sébastien Tixeuil, Maria Potop-Butucaru 

Publication date: 8 February 2021

Published in: Formal Methods in System Design (Search for Journal in Brave)

Abstract: We study verification problems for autonomous swarms of mobile robots that self-organize and cooperate to solve global objectives. In particular, we focus in this paper on the model proposed by Suzuki and Yamashita of anonymous robots evolving in a discrete space with a finite number of locations (here, a ring). A large number of algorithms have been proposed working for rings whose size is not a priori fixed and can be hence considered as a parameter. Handmade correctness proofs of these algorithms have been shown to be error-prone, and recent attention had been given to the application of formal methods to automatically prove those. Our work is the first to study the verification problem of such algorithms in the parameter-ized case. We show that safety and reachability problems are undecidable for robots evolving asynchronously. On the positive side, we show that safety properties are decidable in the synchronous case, as well as in the asynchronous case for a particular class of algorithms. Several properties on the protocol can be decided as well. Decision procedures rely on an encoding in Presburger arithmetics formulae that can be verified by an SMT-solver. Feasibility of our approach is demonstrated by the encoding of several case studies.

Full work available at URL: https://arxiv.org/abs/1706.05193

Recommendations

• Computing on rings by oblivious robots: a unified approach for different tasks
• Optimal deterministic ring exploration with oblivious asynchronous robots
• About ungatherability of oblivious and asynchronous robots on anonymous rings
• Optimal probabilistic ring exploration by semi-synchronous oblivious robots
• Optimal probabilistic ring exploration by semi-synchronous oblivious robots
• On the self-stabilization of mobile oblivious robots in uniform rings
• How to gather asynchronous oblivious robots on anonymous rings

zbMATH Keywords

formal verificationSMT-solverswarms of robots

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Artificial intelligence for robotics (68T40)

Cites Work

• Title not available (Why is that?)
• Distributed Anonymous Mobile Robots: Formation of Geometric Patterns
• Undecidable problems in unreliable computations.
• Bounds on Positive Integral Solutions of Linear Diophantine Equations
• Impossibility of gathering, a certification
• Computing without communicating: ring exploration by asynchronous oblivious robots
• Exclusive perpetual ring exploration without chirality
• Certified universal gathering in \(\mathbb {R}^2\) for oblivious mobile robots
• Synchronous gathering without multiplicity detection: a certified algorithm
• Formal verification of mobile robot protocols
• Model checking of a mobile robots perpetual exploration algorithm

Cited In (6)

• A framework for formal verification of robot kinematics
• Synchronous gathering without multiplicity detection: a certified algorithm
• Formal verification of mobile robot protocols
• Preface of the special issue on the conference on formal methods in computer-aided design 2017
• An environment for specifying and model checking mobile ring robot algorithms
• Model checking of robot gathering

Uses Software

• z3

This page was built for publication: Parameterized verification of algorithms for oblivious robots on a ring

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2225474)