Formal verification of mobile robot protocols

DOI10.1007/S00446-016-0271-1MaRDI QIDQ2359768zbMATH OpenOpenAlexFDO

Authors Pascal Lafourcade, Laure Millet, Yann Thierry-Mieg, Sébastien Tixeuil, Béatrice Bérard, Maria Potop-Butucaru

Publication date 22 June 2017

Published in Distributed Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00446-016-0271-1

zbMATH Keywords

mobile robotsmodel checkingverification

Mathematics Subject Classification ID

Network protocols (68M12) Distributed systems (68M14) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Model checking of robot gathering
• Model checking of a mobile robots perpetual exploration algorithm
• Parameterized verification of algorithms for oblivious robots on a ring
• Certified universal gathering in \(\mathbb {R}^2\) for oblivious mobile robots
• Model checking mobile ad hoc networks

Cites work

• Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3--7, 2007. Proceedings.
• Computing without communicating: ring exploration by asynchronous oblivious robots
• Diagram refinements for the design of reactive systems
• Distributed Anonymous Mobile Robots: Formation of Geometric Patterns
• Distributed computing by mobile robots: gathering
• Exclusive perpetual ring exploration without chirality
• Gathering an even number of robots in an odd ring without global multiplicity detection
• Gathering of asynchronous robots with limited visibility
• Gathering six oblivious robots on anonymous symmetric rings
• scientific article; zbMATH DE number 1633145 (Why is no real title available?)
• scientific article; zbMATH DE number 3887558 (Why is no real title available?)
• scientific article; zbMATH DE number 3639163 (Why is no real title available?)
• scientific article; zbMATH DE number 1479642 (Why is no real title available?)
• scientific article; zbMATH DE number 1796136 (Why is no real title available?)
• scientific article; zbMATH DE number 910719 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Mechanical Verification of Automatic Synthesis of Fault-Tolerant Programs
• Model checking transactional memories
• On Reasoning About Rings
• Parameterized model checking of rendezvous systems
• Proving properties of a ring of finite-state machines
• Tutorial on parameterized model checking of fault-tolerant distributed algorithms
• Verification of consensus algorithms using satisfiability solving

Cited in

(13)

• Verification of agent navigation in partially-known environments
• Parameterized verification of algorithms for oblivious robots on a ring
• Embedded pattern formation by asynchronous robots without chirality
• Asynchronous arbitrary pattern formation: the effects of a rigorous approach
• Model checking of robot gathering
• Formal Verification Applied to Robotic Surgery
• Model checking of a mobile robots perpetual exploration algorithm
• Automated Technology for Verification and Analysis
• Synchronous gathering without multiplicity detection: a certified algorithm
• Squeezing streams and composition of self-stabilizing algorithms
• An environment for specifying and model checking mobile ring robot algorithms
• Deterministic color-optimal self-stabilizing semi-synchronous gathering: two certified algorithms
• Topological sensitivity analysis for the narrow escape problem

Describes a project that uses

Uses Software

• DiVinE
• UPPAAL TIGA
• SPIN
• Uppaal

This page was built for publication: Formal verification of mobile robot protocols

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