Parameterized verification of algorithms for oblivious robots on a ring

DOI10.1007/S10703-019-00335-YMaRDI QIDQ2225474zbMATH OpenOpenAlexFDO

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)

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

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)

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.

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

Cites work

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

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

Describes a project that uses

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)