Formal verification of mobile robot protocols

No abstract is available for this paper.

• Publication year

  2016

• Venue

  Distributed computing

• Publication date

  2016-04-15

• Fields of study

  Computer Science, Engineering

• Identifiers
  DOI 10.1007/s00446-016-0271-1
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Model Checking

  2018cited by this paper
• Guidelines for Verification of Population Protocols

  2017cited by this paper
• On the Synthesis of Mobile Robots Algorithms: The Case of Ring Gathering

  2014cited by this paper
• Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms

  2014cited by this paper
• Parameterized model checking of rendezvous systems

  2014cited by this paper
• DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs

  2013influential reference
• Towards Distributed Software Model-Checking Using Decision Diagrams

  2013influential reference
• Gathering an Even Number of Robots in an Odd Ring without Global Multiplicity Detection

  2012cited by this paper
• Distributed Computing by Oblivious Mobile Robots

  2012influential reference
• Discovering and Assessing Fine-Grained Metrics in Robot Networks Protocols

  2012cited by this paper
• Optimal Grid Exploration by Asynchronous Oblivious Robots

  2011cited by this paper
• Towards Verification of the Pastry Protocol Using TLA +

  2011cited by this paper
• Verification of consensus algorithms using satisfiability solving

  2011cited by this paper
• Formal Verification of Consensus Algorithms Tolerating Malicious Faults

  2011cited by this paper
• Asynchronous Mobile Robot Gathering from Symmetric Configurations without Global Multiplicity Detection

  2011cited by this paper
• Gathering of Six Robots on Anonymous Symmetric Rings

  2011cited by this paper
• DiVinE: Parallel Distributed Model Checker

  2010cited by this paper
• DiVinE: Parallel Distributed Model Checker (Tool paper)

  2010cited by this paper
• Algorithmic Verification of Population Protocols

  2010cited by this paper
• Exclusive Perpetual Ring Exploration without Chirality

  2010influential reference
• Principles of model checking

  2008cited by this paper
• Uncertainty and imprecision modeling for the mobile robot localization problem

  2008cited by this paper
• Principles of Model Checking (Representation and Mind Series)

  2008cited by this paper
• Computing Without Communicating: Ring Exploration by Asynchronous Oblivious Robots

  2007influential reference
• UPPAAL-Tiga: Time for Playing Games!

  2007cited by this paper
• Border

  2007cited by this paper
• Gathering of asynchronous robots with limited visibility

  2005cited by this paper
• Recent Advances on Multi-agent Patrolling

  2004cited by this paper
• Mechanical Verification of Automatic Synthesis of Fault-Tolerant Programs

  2004cited by this paper
• The SPIN Model Checker - primer and reference manual

  2003cited by this paper
• Diagram Refinements for the Design of Reactive Systems

  2001cited by this paper
• Systems and Software Verification, Model-Checking Techniques and Tools

  2001cited by this paper
• Parameterized Verification with Automatically Computed Inductive Assertions

  2001cited by this paper
• Distributed Anonymous Mobile Robots: Formation of Geometric Patterns

  1999influential reference
• On the Veri cation of Broadcast

  1999cited by this paper
• On the verification of broadcast protocols

  1999cited by this paper
• Visual Verification of Reactive Systems

  1997cited by this paper
• Model Cheking

  1997cited by this paper
• Automatic Verification of Parameterized Synchronous Systems (Extended Abstract)

  1996cited by this paper
• STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems

  1996cited by this paper
• UPPAAL - a Tool Suite for Automatic Verification of Real-Time Systems

  1996cited by this paper
• Veryfying Parameterized Networks using Abstraction and Regular Languages

  1995cited by this paper
• Reasoning about rings

  1995cited by this paper
• Specifying and Verifying Fault-Tolerant Systems

  1994cited by this paper
• Temporal Verification Diagrams

  1994cited by this paper
• Temporal Veri cation Diagrams ?

  1994cited by this paper
• The synchronous data flow programming language LUSTRE

  1991cited by this paper
• Proving Properties of a Ring of Finite-State Machines

  1988cited by this paper
• Supervisory control of a class of discrete event processes

  1987cited by this paper
• Limits for Automatic Verification of Finite-State Concurrent Systems

  1986cited by this paper
• Introduction to formal language theory

  1978cited by this paper

• Deterministic Color-Optimal Self-stabilizing Semi-synchronous Gathering: A Certified Algorithm

  2025cites this paper
• Knowledge in multi-robot systems: an interplay of dynamics, computation and communication

  2025cites this paper
• Memoryless Adversaries in Imperfect Information Games

  2023cites this paper
• Verification of agent navigation in partially-known environments

  2022cites this paper
• Swarms of Mobile Robots: Towards Versatility with Safety

  2022cites this paper
• Compacting oblivious agents on dynamic rings

  2021cites this paper
• Agents and Robots for Reliable Engineered Autonomy: A Perspective from the Organisers of AREA 2020

  2021cites this paper
• Unreliable Sensors for Reliable Efficient Robots

  2021cites this paper
• Computer Aided Formal Design of Swarm Robotics Algorithms

  2021cites this paper
• Using Model Checking to Formally Verify Rendezvous Algorithms for Robots with Lights in Euclidean Space

  2019cites this paper
• On the encoding and solving partial information games

  2019cites this paper
• Formal Methods for Mobile Robots

  2019cites this paper
• Oblivious Robots on Graphs: Exploration

  2019influential citation
• Squeezing Streams and Composition of Self-stabilizing Algorithms

  2019cites this paper
• Continuous vs. Discrete Asynchronous Moves: A Certified Approach for Mobile Robots

  2019cites this paper
• Stabilization, Safety, and Security of Distributed Systems: 21st International Symposium, SSS 2019, Pisa, Italy, October 22–25, 2019, Proceedings

  2019influential citation
• An Environment for Specifying and Model Checking Mobile Ring Robot Algorithms

  2019cites this paper
• Structural Information in Distributed Computing

  2019cites this paper
• A Foundational Framework for Certified Impossibility Results with Mobile Robots on Graphs

  2018cites this paper
• On the Encoding and Solving of Partial Information Games

  2018cites this paper
• Brief Announcement Continuous vs. Discrete Asynchronous Moves: A Certified Approach for Mobile Robots

  2018cites this paper
• Embedded pattern formation by asynchronous robots without chirality

  2018cites this paper
• Certified Gathering of Oblivious Mobile Robots: Survey of Recent Results and Open Problems

  2017cites this paper
• Parameterized verification of algorithms for oblivious robots on a ring

  2017cites this paper
• Model Checking of Robot Gathering

  2017cites this paper
• Optimally Gathering Two Robots

  2017cites this paper
• Asynchronous Arbitrary Pattern Formation: the effects of a rigorous approach

  2017cites this paper
• Asynchronous Pattern Formation: the effects of a rigorous approach

  2017cites this paper
• Model Checking of a Mobile Robots Perpetual Exploration Algorithm

  2016cites this paper
• Certified Universal Gathering in \mathbb R ^2 for Oblivious Mobile Robots

  2016cites this paper
• Brief Announcement: Certified Universal Gathering in R2 for Oblivious Mobile Robots

  2016cites this paper
• Synchronous Gathering without Multiplicity Detection: a Certified Algorithm

  2016cites this paper
• A Certified Universal Gathering Algorithm for Oblivious Mobile Robots

  2015cites this paper
• Parameterised Verification of Autonomous Mobile-Agents in Static but Unknown Environments

  2015cites this paper
• Improving the model checking of stutter-invariant LTL properties. (Amélioration du model checking des propriétés LTL insensibles au bégaiement)

  2014cites this paper
• Impossibility of gathering, a certification

  2014cites this paper