Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Related Work <s> This paper studies a general methodology and an associated tool for translating AADL (Architecture Analysis and Design Language) and annex behavior specification into the BIP (Behavior Interaction Priority) language. This allows simulation of systems specified in AADL and application to these systems of formal verification techniques developed for BIP, e.g. deadlock detection. We present a concise description of AADL and BIP followed by the presentation of the translation methodology illustrated by a Flight Computer example. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Related Work <s> While autonomous systems offer great promise in terms of capability and flexibility, their reliability is particularly hard to assess. This paper describes research to apply formal verification methods to languages used to develop autonomy software. In particular, we describe tools that automatically convert autonomy software into formal models that are then verified using model checking. This approach has been applied to MPL code for the Livingstone fault diagnosis system and to TDL task descriptions for mobile robot systems. Our long-term objective is to create tools that enable engineers and roboticists to use formal verification as part of the normal software development cycle. <s> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Related Work <s> In this paper, we propose a novel policy for steering multiple vehicles between assigned start and goal configurations, ensuring collision avoidance. The policy rests on the assumption that all agents are cooperating by implementing the same traffic rules. However, the policy is completely decentralized, as each agent decides its own motion by applying those rules only on the locally available information, and scalable, in the sense that the amount of information processed by each agent and the computational complexity of the algorithms do not increase with the number of agents in the scenario. The proposed policy applies to systems in which new vehicles may enter the scene and start interacting with existing ones at any time, while others may leave. Under mild conditions on the initial configurations, the policy is shown to be safe, i.e., it guarantees collision avoidance throughout the system evolution. In the paper, conditions are discussed on the desired configurations of agents, under which the ultimate convergence of all vehicles to their goals can also be guaranteed. To show that such conditions are actually necessary and sufficient, which turns out to be a challenging liveness-verification problem for a complex hybrid automaton, we employ a probabilistic verification method. The paper finally presents and discusses simulations for systems of several tens of vehicles, and reports on some experimental implementation showing the practicality of the approach. <s> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Related Work <s> The development of theoretical-based methods for the assessment of multi-agent systems properties is of critical importance. This work is a preliminary investigation on methodologies for modeling, analysis and design of multi-agent systems. Multi-agent systems are regarded as discrete-event dynamic systems and Petri nets are used as a modeling tool to assess the structural properties of the multi-agent system. Our methodology consists of defining a simple multi-agent system based on the abstract architecture for intelligent agents. The abstract architecture is modeled as a discrete-event system using Petri nets and structural analysis of the net provides an assessment of the communication and coordination properties of the multi-agent system. Deadlock avoidance in the multi-agent system is considered as an initial key property, and it is evaluated using liveness and boundedness properties of the Petri net model. <s> BIB004 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Related Work <s> Autonomous robots are complex systems that require the interaction/cooperation of numerous heterogeneous software components. Nowadays, robots are critical systems and must meet safety properties including in particular temporal and real-time constraints. We present a methodology for modeling and analyzing a robotic system using the BIP component framework integrated with an existing framework and architecture, the LAAS Architecture for Autonomous System, based on GenoM. The BIP componentization approach has been successfully used in other domains. In this study, we show how it can be seamlessly integrated in the preexisting methodology. We present the componentization of the functional level of a robot, the synthesis of an execution controller as well as validation techniques for checking essential “safety” properties. <s> BIB005 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Related Work <s> We describe an architecture-centric design and implementation approach for building self-adapting and self-managing robotics systems. The basis of our approach is the concept of meta-level components, which facilitate adaptation and management of application-level components. Our approach applies two key enhancements to the traditional usage of meta-level components: (1) we utilize three distinct, specialized meta-level components for the three fundamental activities of a robotics system: sensing, computation, and control, and (2) we allow meta-level components to themselves be monitored, managed and adapted by other (higher layer) meta-level components. In this way, our approach flexibly supports adaptive layered architectures of arbitrary depth, the specification of arbitrary system adaptation policies, and the provision of intelligent facilities for constructing adaptation plans on-the-fly. We showcase our approach using a team of autonomous mobile robots that engage in a leader-follower scenario and experience a wide variety of failures, activating distinct recovery mechanisms. <s> BIB006 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Related Work <s> Self-adaptive systems have the capability to autonomously modify their behaviour at run-time in response to changes in their environment. Self-adaptation is particularly necessary for applications that must run continuously, even under adverse conditions and changing requirements; sample domains include automotive systems, telecommunications, and environmental monitoring systems. While a few techniques have been developed to support the monitoring and analysis of requirements for adaptive systems, limited attention has been paid to the actual creation and specification of requirements of self-adaptive systems. As a result, self-adaptivity is often constructed in an ad-hoc manner. In this paper, we argue that a more rigorous treatment of requirements explicitly relating to self-adaptivity is needed and that, in particular, requirements languages for self-adaptive systems should include explicit constructs for specifying and dealing with the uncertainty inherent in self-adaptive systems. We present RELAX, a new requirements language for self-adaptive systems and illustrate it using examples from the smart home domain. <s> BIB007 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Related Work <s> A practical text suitable for an introductory or advanced course in formal methods, this book presents a mathematical approach to modelling and designing systems using an extension of the B formal method: Event-B. Based on the idea of refinement, the author's systematic approach allows the user to construct models gradually and to facilitate a systematic reasoning method by means of proofs. Readers will learn how to build models of programs and, more generally, discrete systems, but this is all done with practice in mind. The numerous examples provided arise from various sources of computer system developments, including sequential programs, concurrent programs and electronic circuits. The book also contains a large number of exercises and projects ranging in difficulty. Each of the examples included in the book has been proved using the Rodin Platform tool set, which is available free for download at www.event-b.org. <s> BIB008 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Related Work <s> The verification of evasive maneuvers for autonomous vehicles driving with constant velocity is considered. Modeling uncertainties, uncertain measurements, and disturbances can cause substantial deviations from an initially planned evasive maneuver. From this follows that the maneuver, which is safe under perfect conditions, might become unsafe. In this work, the possible set of deviations is computed with methods from reachability analysis, which allows to verify evasive maneuvers under consideration of the mentioned uncertainties. Since the presented approach has a short response time, it can be applied for real time safety decisions. The methods are presented for a numerical example where two autonomous cars plan a coordinated evasive maneuver in order to prevent a collision with a wrong-way driver. <s> BIB009 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Related Work <s> Robot swarms provide a way for a number of simple robots to work together to carry out a task. While swarms have been found to be adaptable, fault-tolerant and widely applicable, designing individual robot algorithms so as to ensure effective and correct swarm behaviour is very difficult. In order to assess swarm effectiveness, either experiments with real robots or computational simulations of the swarm are usually carried out. However, neither of these involve a deep analysis of all possible behaviours. In this paper we will utilise automated formal verification techniques, involving an exhaustive mathematical analysis, in order to assess whether our swarms will indeed behave as required. <s> BIB010 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Related Work <s> In this paper we assess the feasibility of using formal methods, and model checking in particular, for the certification of Unmanned Aircraft Systems (UAS) within civil airspace. We begin by modelling a basic UAS control system in PROMELA, and verify it against a selected subset of the CAA's Rules of the Air using the SPIN model checker. Next we build a more advanced UAS control system using the autonomous agent language Gwendolen, and verify it against the small subset of the Rules of the Air using the agent model checker AJPF. We introduce more advanced autonomy into the UAS agent and show that this too can be verified. Finally we compare and contrast the various approaches, discuss the paths towards full certification, and present directions for future research. <s> BIB011 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Related Work <s> In this paper, we propose a new workflow for the design of composite systems. Contrary to existing approaches, which build on traditional techniques for single-component systems, our methodology is incremental in terms of both the design and the verification process. The approach exploits the hierarchy between components and can detect errors at an early stage of the design. As a second contribution of the paper, we apply our methodology to automatically generate C code to coordinate the various modules of an autonomous robot. To the best of our knowledge, this is the first time that such a coordination code is generated automatically. <s> BIB012 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Related Work <s> We present a computational framework for automatic synthesis of control and communication strategies for a robotic team from task specifications that are given as regular expressions about servicing requests in an environment. We assume that the location of the requests in the environment and the robot capacities and cooperation requirements to service the requests are known. Our approach is based on two main ideas. First, we extend recent results from formal synthesis of distributed systems to check for the distributability of the task specification and to generate local specifications, while accounting for the service and communication capabilities of the robots. Second, by using a technique that is inspired by linear temporal logic model checking, we generate individual control and communication strategies. We illustrate the method with experimental results in our robotic urban-like environment. <s> BIB013 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Related Work <s> We have recently started an effort to combine a state of the art tool for developing functional modules of robotic systems (G^e^noM) with a component based framework for implementing embedded real-time systems (BIP). Unlike some works which study the connection between formal approaches and the highest (decisional) level of the robot software architecture, where deliberative activities such as planning, diagnostics, and execution control are conducted, we tackle the problem of using formal methods for developing modules of the functional level of robots. Little attention has been drawn to the development of these modules whose robustness is paramount to the robustness of the overall platform. To this end, we have successfully developed the G^e^noM/BIP component based design approach and applied it to the functional level of a complex exploration rover. Here, we report on this work, and show how we: (i) produce a very fine grained formal computational model of the robot functional level; (ii) run the BIP engine on the real robot, which executes and enforces the model semantics at runtime; and (iii) check the model offline for deadlock-freedom, as well as other safety properties. Moreover, we also extended this paradigm in a number of promising directions: (i) introduced a real-time BIP engine which can now use and control a timed BIP model; (ii) distributed the model and the engine over multiple CPUs; (iii) proposed a user-friendly language for specifying constraints on the model; and (iv) linked the model with a temporal plan execution controller. Interestingly, although our approach was initially proposed for the lowest level of robot architectures, these more recent extensions now allow us to model and manage the deliberation taking place at the decisional layer. <s> BIB014 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Related Work <s> I l l u S t r a t I o n b y a l I C I a k u b I S t a /a n D r I J b o r y S a S S o C I a t e S in This arTiCle we consider the question: How should autonomous systems be analyzed? in particular, we describe how the confluence of developments in two areas—autonomous systems architectures and formal verification for rational agents—can provide the basis for the formal verification of autonomous systems behaviors. We discuss an approach to this question that involves: 1. Modeling the behavior and describing the interface (input/output) to an agent in charge of making decisions within the system; 2. Model checking the agent within an unrestricted environment representing the “real world” and those parts of the systems external to the agent, in order to establish some property, j; 3. Utilizing theorems or analysis of the environment, in the form of logical statements (where necessary), to derive properties of the larger system; and 4. if the agent is refined, modify (1), but if environmental properties are clarified, modify (3). Autonomous systems are now being deployed in safety, mission, or business critical scenarios, which means a thorough analysis of the choices the core software might make becomes crucial. But, should the analysis and verification of autonomous software be treated any differently than traditional software used in critical situations? Or is there something new going on here? Autonomous systems are systems that decide for themselves what to do and when to do it. Such systems might seem futuristic, but they are closer than we might think. Modern household, business, and industrial systems increasingly incorporate autonomy. There are many examples, all varying in the degree of autonomy used, from almost pure human control to fully autonomous activities with minimal human interaction. Application areas are broad, ranging from healthcare monitoring to autonomous vehicles. But what are the reasons for this increase in autonomy? Typically, autonomy is used in systems that: 1. must be deployed in remote environments where direct human control is infeasible; 2. must be deployed in hostile environments where it is dangerous for humans to be nearby, and so difficult for humans to assess the possibilities; 3. involve activity that is too lengthy Verifying autonomous systems Doi:10.1145/2494558 <s> BIB015 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Related Work <s> We applied quantified differential-dynamic logic (QdL) to analyze a control algorithm designed to provide directional force feedback for a surgical robot. We identified problems with the algorithm, proved that it was in general unsafe, and described exactly what could go wrong. We then applied QdL to guide the development of a new algorithm that provides safe operation along with directional force feedback. Using \KeYmaeraD (a tool that mechanizes QdL), we created a machine-checked proof that guarantees the new algorithm is safe for all possible inputs. <s> BIB016 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Related Work <s> Human‐robot teams are likely to be used in a variety of situations wherever humans require the assistance of robotic systems. Obvious examples include healthcare and manufacturing, in which people need the assistance of machines to perform key tasks. It is essential for robots working in close proximity to people to be both safe and trustworthy. In this paper we examine formal verification of a high-level planner/scheduler for autonomous personal robotic assistants such as CareO-bot R . We describe how a model of Care-O-bot and its environment was developed using Brahms, a multiagent workflow language. Formal verification was then carried out by translating this to the input language of an existing model checker. Finally we present some formal verification results and describe how these could be complemented by simulation-based testing and realworld end-user validation in order to increase the practical and perceived safety and trustworthiness of robotic assistants. <s> BIB017 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Related Work <s> Before autonomous robotics can be used for dangerous or critical missions, performance guarantees should be made available. This paper overviews a software system for the verification of behavior-based controllers in context of chosen hardware and environmental models. Robotic controllers are automatically translated to a process algebra. The system comprising both the robot and the environment are then evaluated by VIPARS, a verification software module in development, and compared to specific performance criteria. The user is returned a probability that the performance criteria will hold in the uncertainty of real-world conditions. Experimental results demonstrate accurate verification for a mission related to the search for a biohazard. <s> BIB018 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Related Work <s> Safety is a key challenge in robotics, in particular for mobile robots operating in an open and unpredictable environment. To address the safety challenge, various software-based approaches have been proposed, but none of them provide a clearly specified and isolated safety layer. In this paper, we propose that safety-critical concerns regarding the robot software be explicitly declared separately from the main program, in terms of externally observable properties of the software. Concretely, we use a Domain-Specific Language (DSL) to declaratively specify a set of safety-related rules that the software must obey, as well as corresponding corrective actions that trigger when rules are violated. Our DSL, integrated with ROS, is shown to be capable of specifying safety-related constraints, and is experimentally demonstrated to enforce safety behaviour in existing robot software. We believe our approach could be extended to other fields to similarly simplify safety certification. <s> BIB019 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Related Work <s> Abstract Developing advanced robotics applications is now facing the safety issue for users, the environment, and the robot itself, which is a main limitation for their deployment in real life. This safety could be justified by the use of dependability techniques as it is done in other safety-critical applications. However, due to specific robotic properties (such as continuous human–robot physical interaction or non deterministic decisional layer), many techniques need to be adapted or revised. This paper reviews the main issues, research work and challenges in the field of safety-critical robots, linking up dependability and robotics concepts. <s> BIB020
To our knowledge, there is no survey of the recent literature for formal specification and verification of autonomous robotic systems. This section differentiates related work from ours. Robotic systems often have safety-critical consequences. A survey on safety-critical robotics BIB020 identified seven focus areas for the development of robots that can safely work alongside humans and other robots, in unstructured environments. These areas are (1) modeling and simulation of the physical environment to enable better safety analysis, BIB008 formal verification of robot systems, BIB019 controllers that are correct by construction, BIB019 identification and monitoring of hazardous situations, (5) models of human-robot interaction,  online safety monitoring that BIB017 SPIN, Brahms modelling language (BrahmsToPromela translator), LTL. Care-O-Bot robotic assistant in a Robot House Environment. BIB015 Gwendolen, AJPF, MCAPL, LTL. RoboCup rescue scenario, autonomous satellite scenario, autonomous pilotless aircraft scenario. BIB016 Quantified differential dynamic logic (QdL) and proof using KeYmaeraD. Formally verified control algorithms for surgical robots. BIB009 Reachability analysis. A wrong-way driver threatens two autonomously driving vehicles on a road with three lanes. BIB010 PCTL models of Probabilistic State Machines, PRISM. The foraging (swarm) robot scenario  . BIB018 Process Algebra for Robotic Systems (PARS) and MissionLab. Search for a Biohazard . [178] Z model for self-adaptive systems, CZT. MAPE-K reference model  and Layered self-adaptive robotics software BIB006 . [125] KeYmaera, dynamic differential logic for hybrid systems. Robotic ground vehicle navigation. BIB011 Gwendolen, SPIN, AJPF, LTL. Model checking for certification of autonomous pilotless aircraft systems. BIB005 BIP (Behaviour-Interaction-Priority) component framework, Evaluator model-checker (temporal logic properties) and monitors. DALA (iRobot ATRV). BIB013 Theoretical work inspired by LTL and model-checking, computational framework where task specifications are regular expressions. Finite State Automata. Car-like robots operating in an urban-like environment. [138] Quartz (synchronous language),model-checking LTL/CTL specifications using Beryl model-checker in the Averest verification framework. Behaviour-based control network of mobile outdoor robot RAVON. BIB001 A metamodel-based translation from AADL to BIP. Aldebaran model-checker (in BIP) for deadlock detection and observers for monitoring safety properties. Flight computer. BIB003 Probabilistic verification using Monte Carlo approach (no tool support, theorems and proofs in paper). Collision avoidance management of a large and changing number of autonomous vehicles. [50] SPIN to verify Ach (novel interprocess (IPC) communication mechanism and library). Implementation of Ach on Golem Kang humanoid robot. [51] Timed Automata and Timed CTL (TCTL) to verify MAPE-K templates for the development of self adaptive systems, and Uppaal. Traffic monitoring, outdoor learning robot, transportation and, storytelling robot. [129] Hybrid system modelling using natural language programming (sEnglish) which is translated to Stateflow and verified using MCMAS. Autonomous underwater vehicles. [30] (Extended Abstract) Brahms modelling framework translated into Jason agent code and model-checking temporal logic properties. Astronaut-robot collaboration. [88] Systems of differential equations and manoeuvrer automata generated using reachability analysis. Collision avoidance of road vehicles. [141] LTL, extension to LTLMoP toolkit for robot mission planning. Fire fighting scenario. BIB012 BIP framework, DFinder model-checker. DALA autonomous rover. [146] Extensible Agent Behaviour Specification Language (XABSL) -language for describing state machines. Robot Soccer. [138] Synchronous language Quartz and verification using model-checking techniques of the Averest verification framework (Beryl). Mobile outdoor robot RAVON. (Continued)  Timed Automata (TA) for modelling and Timed Computation Tree Logic (TCTL) for safety and correctness properties for an adaptive autonomous system. Distributed network of traffic monitoring cameras that reorganise to coordinate data transmission. [66] RV-BIP, a tool that produces runtime monitors for robots the BIP framework from formal descriptions of the system and monitor. Autonomous rover. [98] TA for modelling different modes of operation, and a module that enables them to be swapped during their execution on a Virtual Machine (VM). Turtlebot robots navigating a map, representing a goods-transportation system. [182] Probabilistic Finite-State Machine (PFSM), transition probabilities are estimated and then validated by simulation in Player/Stage. Swarm navigating with the alpha algorithm. [49] Layered modelling of a robot's task plans using Petri Nets. Robot Soccer. [179] Reference model for building verifiable self-adaptive systems (FORMS). Traffic monitoring system. BIB004 Modelling an abstract architecture for reactive multi-agent systems, which are then analysed for deadlock freedom. Small example with two agents cooperating to move objects. [186] Modelling plans as Petri nets with an additional set of Goal Markings for single-and multi-robot systems. Multi-robot foraging and object passing. [123] Bio-PEPA process algebra to model the Marco and Micro level behaviour of robot swarms. These are analysed using the Bio-PEPA Tool Suite and PRISM. Swarm foraging, where a team of three robots is needed to carry each object. [108] LTL-X (LTL without "next" operator) and Büchi Automata to give a robot control and communications strategy with reduced 'stop-and-wait' synchronisations. A team of unicycle robots with distributed control. [117] Specifies robot behaviour in Z, then links Z animator Jaza to the Java debugger jdb to monitor the running program without alterations or additions. Robot assembly system, for building robots for the NASA ANTS project a . [6] Derives a specification of a real-time system (in CSP+T) from a UML-RT Model for design-time schedulability and dependability analysis. Two-armed industrial robot and mechanical press. [80] Methodology for verifying three cooperative robots with distributed control using the formal language Klaim, and its extension for stochastic analysis. Three cooperative robots transporting an object to a goal area. [11] Ontology-based (Web Ontology Language (OWL)) reconfiguration agent in a manufacturing environment. [115] Fragment of temporal logic called General Reactivity BIB014 . Search and rescue style missions. [18] Behaviour Interaction Priority (BIP) framework. DALA iROBOT ATRV. [25] BIP and LAAS frameworks. DALA iROBOT ATRV. [83] Büchi Automata (BA) modelling the environment and LTL task specifications. A surveillance robot. [48] Markov chains to predict swarm aggregation. Cockroach aggregation. [89] Integration of Object-Z and Statecharts, SAL model checker, and STeP theorem prover. N/A BIB007 Requirements language for dynamically adaptive systems (RELAX) whose semantics is defined in terms of temporal fuzzy logic. Adaptive assisted living smart home. [81] Restore Invariant Approach (RIA), Microsoft Robotics Studio simulator, JADEX multi-agent framework, Alloy, class diagrams and OCL. Adaptive production cell. [55] LTL and Agent Java PathFinder (AJPF). Three pilotless civilian aircraft examples: brake failure, eratic intruder aircraft, and low fuel. [57] LTL and AJPF. Ethical scenario of a robot trying to stop humans from falling down a hole. [95] LTL. LandShark rover robot. [1] BIP models to generate G en oM controllers, and D-Finder tool. Dala rover navigating to a target position, taking a picture, and returning to the initial position. [111] Discrete-Time Markov Chain (DTMC) to model the foraging algorithm, Probabilistic Computation Tree Logic (PCTL) for safety properties, PRISM. Foraging robot swarm. [36] DTMCs to model the aggregation algorithm, Probabilistic Computation Tree Logic* (PCTL*) specifications, and PRISM for checking. Aggregation in robot swarm. [61] Finite-State Machines (FSMs), Probabilistic Temporal Logic (PTL) for specification, checked in NuSMV. Alpha algorithm for robot swarms. [62] FSMs, PTL for specification, checked in NuSMV. Also a NetLogo simulation. Alpha algorithm for robot swarms. [41] An update of BIB013 that uses JFLAP and MatLab. Formal Specification and Verification of Autonomous Robotic Systems 100:7 adapts to the robot's context, and (7) certification evidence. In contrast, our survey focuses on the application of formal methods to any type of autonomous robotic system. Nordmann et al.  present a detailed survey of Domain-Specific Modeling Languages for robotics. Their study focusses on nonformal modeling but was influential to the depth and organization of our survey. They analyze languages by both the applicable domain and development phase. The use of model-driven engineering approaches in building robotic systems seems too prevalent to ignore, as we discuss in Section 2. In applying formal verification methods to programming languages for autonomous software, Simmons et al. BIB002 identified three challenges for the automatic verification of autonomous systems: (1) "special purpose languages use special-purpose interpreters or compilers" that must be verified, (2) "application-specific programs written in these languages need to be verified for internal correctness" (safety, liveness, etc.), and (3) "programs need to be verified for external correctness" (how they interact with the overall software system). Weyns et al.  present a survey of formal methods for self-adaptive systems. While robotic systems may be required to adapt themselves, this behavior is not required of all robotic systems and so it is somewhat tangential to our survey. We discuss the specific challenges of formally specifying and verifying self-adaptive robotic systems in Section 4.3. Rouff et al.   survey formal methods for intelligent swarms. As we discuss in Section 4.2.1, the challenges posed by robot swarms are an extension of those of single autonomous robotic systems. They compare a wide range of formalisms, covering process algebras, modelbased notations, and various logics, among others. They conclude that no single formalism is suitable to the range of challenges posed by intelligent robot swarms. Their focus is, again, narrower than ours and Section 4.2.1 offers a more recent perspective on formal methods for robot swarms.