Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Temporal Logics. <s> It is a characteristic of swarm robotics that specifying overall emergent swarm behaviours in terms of the low-level behaviours of individual robots is very difficult. Yet if swarm robotics is to make the transition from the laboratory to real-world engineering realisation we need such specifications. This paper explores the use of temporal logic to formally specify, and possibly also prove, the emergent behaviours of a robotic swarm. The paper makes use of a simplified wireless connected swarm as a case study with which to illustrate the approach. Such a formal approach could be an important step toward a disciplined design methodology for swarm robotics. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Temporal Logics. <s> Michigan/AFRL Collaborative Center on Control Sciences, AFOSR (grant no. FA 8650-07-2-3744) <s> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Temporal Logics. <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> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Temporal Logics. <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> BIB004 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Temporal Logics. <s> Recent work in robotics has applied formal verification tools to automatically generate correct-by-construction controllers for autonomous robots. However, when it is not possible to create such a controller, these approaches do not provide the user with feedback on the source of failure, making the experience of debugging a specification somewhat ad hoc and unstructured, and a source of frustration for the user. This paper describes an extension to the LTLMoP toolkit for robot mission planning that encloses the control-generation process in a layer of automated reasoning to identify the cause of failure, and targets the users attention to flawed portions of the specification. <s> BIB005 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Temporal Logics. <s> A robot swarm is a collection of simple robots designed to work together to carry out some task. Such swarms rely on the simplicity of the individual robots; the fault tolerance inherent in having a large population of identical robots; and the self-organised behaviour of the swarm as a whole. Although robot swarms present an attractive solution to demanding real-world applications, designing individual control algorithms that can guarantee the required global behaviour is a difficult problem. In this paper we assess and apply the use of formal verification techniques for analysing the emergent behaviours of robotic swarms. These techniques, based on the automated analysis of systems using temporal logics, allow us to analyse whether all possible behaviours within the robot swarm conform to some required specification. In particular, we apply model-checking, an automated and exhaustive algorithmic technique, to check whether temporal properties are satisfied on all the possible behaviours of the system. We target a particular swarm control algorithm that has been tested in real robotic swarms, and show how automated temporal analysis can help to refine and analyse such an algorithm. <s> BIB006 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Temporal Logics. <s> We propose a methodology for decentralized multi-agent control from Linear Temporal Logic (LTL) specifications. Each agent receives an independent specification to formally synthesize its own hybrid controller. Mutual satisfiability is not a priori guaranteed. Due to limited communication, the agents utilize meeting events to exchange their controller automata and verify satisfiability through model checking. Local interaction only when common atomic propositions exist reduces the overall computational cost, facilitating scalability. Provably correct collision avoidance and convergence is ensured by Decentralized Multi-Agent Navigation Functions. <s> BIB007 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Temporal Logics. <s> In this paper we propose a generic framework for real-time motion planning based on model-checking and revision. The task specification is given as a Linear Temporal Logic formula over a finite abstraction of the robot motion. A preliminary motion plan is first generated based on the initial knowledge of the system model. Then real-time information obtained during the runtime is used to update the system model, verify and further revise the motion plan. The implementation and revision of the motion plan are performed in real-time. This framework can be applied to partially-known workspaces and workspaces with large uncertainties. Computer simulations are presented to demonstrate the efficiency of the framework. <s> BIB008 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Temporal Logics. <s> The use of unmanned aircraft for civil applications is expected to increase over the next decade, particularly in so-called dull, dirty, and dangerous missions. Unmanned aircraft will undoubtedly require some form of autonomy to ensure safe operations for all airspace users. However, to be used for civil applications, unmanned aircraft must gain regulatory approval in a process known as “certification”. This paper presents a proof-of-concept approach to the generation of certification evidence for autonomous unmanned aircraft based on a combination of formal verification and flight simulation. In particular, a class of autonomous systems controlled by rational agents is examined, and we give examples of 23 different properties, based on the rules of the air and notions of airmanship, which can be used in the formal model checking of rational agents controlling autonomous unmanned aircraft. Our techniques can be based on either 1) implicit models of the aircraft’s physical environment specified in terms of... <s> BIB009 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Temporal Logics. <s> Ensuring that safety requirements are respected is a critical issue for the deployment of hazardous and complex reactive systems. We consider a separate safety channel, called a monitor, that is able to partially observe the system and to trigger safety-ensuring actuations. We address the issue of correctly specifying such a monitor with respect to safety and liveness requirements. Two safety requirement synthesis programs are presented and compared. Based on a formal model of the system and its hazards, they compute a monitor behavior that ensures system safety without unduly compromising system liveness. The first program uses the model-checker NuSMV to check safety requirements. These requirements are automatically generated by a branch-and-bound algorithm. Based on a game theory approach, the second program uses the TIGA extension of UPPAAL to synthesize safety requirements, starting from an appropriately reformulated representation of the problem. <s> BIB010 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Temporal Logics. <s> A new agent architecture called Limited Instruction Set Agent (LISA) is introduced for autonomous control. The new architecture is based on previous implementations of AgentSpeak and it is structurally simpler than its predecessors with the aim of facilitating design-time and run-time verification methods. The process of abstracting the LISA system to two different types of discrete probabilistic models (DTMC and MDP) is investigated and illustrated. The LISA system provides a tool for complete modelling of the agent and the environment for probabilistic verification. The agent program can be automatically compiled into a Discrete-Time Markov Chain (DTMC) or a Markov Decision Process (MDP) model for verification with PRISM. The automatically generated PRISM model can be used for both design-time and run-time verification. The run-time verification is investigated and illustrated in the LISA system as an internal modelling mechanism for prediction of future outcomes. <s> BIB011 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Temporal Logics. <s> Currently, the control software of swarm robotics systems is created by ad hoc development. This makes it hard to deploy these systems in real-world scenarios. In particular, it is difficult to maintain, analyse, or verify the systems. Formal methods can contribute to overcome these problems. However, they usually do not guarantee that the implementation matches the specification, because the system’s control code is typically generated manually. Also, there is cultural resistance to apply formal methods; they may be perceived as an additional step that does not add value to the final product. To address these problems, we propose supervisory control theory for the domain of swarm robotics. The advantages of supervisory control theory, and its associated tools, are a reduction in the amount of ad hoc development, the automatic generation of control code from modelled specifications, proofs of properties over generated control code, and the reusability of formally designed controllers between different robotic platforms. These advantages are demonstrated in four case studies using the e-puck and Kilobot robot platforms. Experiments with up to 600 physical robots are reported, which show that supervisory control theory can be used to formally develop state-of-the-art solutions to a range of problems in swarm robotics. <s> BIB012 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Temporal Logics. <s> It is essential for robots working in close proximity to people to be both safe and trustworthy. We present a case study on formal verification for a high-level planner/scheduler for the Care-O-bot, an autonomous personal robotic assistant. We describe how a model of the Care-O-bot and its environment was developed using Brahms, a multiagent workflow language. Formal verification was then carried out by automatically translating this model to the input language of an existing model checker. Four sample properties based on system requirements were verified. We then refined the environment model three times to increase its accuracy and the persuasiveness of the formal verification results. The first refinement uses a user activity log based on real-life experiments, but is deterministic. The second refinement uses the activities from the user activity log nondeterministically. The third refinement uses “conjoined activities” based on an observation that many user activities can overlap. The four samples properties were verified for each refinement of the environment model. Finally, we discuss the approach of environment model refinement with respect to this case study. <s> BIB013 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Temporal Logics. <s> Abstract Autonomous systems such as unmanned vehicles are beginning to operate within society. All participants in society are required to follow specific regulations and laws. An autonomous system cannot be an exception. Inevitably an autonomous system will find itself in a situation in which it needs to not only choose to obey a rule or not, but also make a complex ethical decision. However, there exists no obvious way to implement the human understanding of ethical behaviour in computers. Even if we enable autonomous systems to distinguish between more and less ethical alternatives, how can we be sure that they would choose right? We consider autonomous systems with a hybrid architecture in which the highest level of reasoning is executed by a rational (BDI) agent. For such a system, formal verification has been used successfully to prove that specific rules of behaviour are observed when making decisions. We propose a theoretical framework for ethical plan selection that can be formally verified. We implement a rational agent that incorporates a given ethical policy in its plan selection and show that we can formally verify that the agent chooses to execute, to the best of its beliefs, the most ethical available plan. <s> BIB014 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Temporal Logics. <s> Software is an essential part of robotic systems. As robots and autonomous systems are more and more deployed in human environments, we need to use elaborate validation and verification techniques in order to gain a higher level of trust in our systems. This motivates our determination to apply formal verification methods to robotics software. In this paper, we describe our results obtained using model-checking on the functional layer of an autonomous robot. We implement an automatic translation from GenoM, a robotics model-based software engineering framework, to the formal specification language Fiacre. This translation takes into account the semantics of the robotics middleware. TINA, our model-checking toolbox, can be used on the synthesized models to prove real-time properties of the functional modules implementation on the robot. We illustrate our approach using a realistic autonomous navigation example. <s> BIB015 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Temporal Logics. <s> A major challenge towards large scale deployment of autonomous mobile robots is to program them with formal guarantees and high assurance of correct operation. To this end, we present a framework for building safe robots. Our approach for validating the end-to-end correctness of robotics system consists of two parts: (1) a high-level programming language for implementing and systematically testing the reactive robotics software via model checking; (2) a signal temporal logic (STL) based online monitoring system to ensure that the assumptions about the low-level controllers (discrete models) used during model checking hold at runtime. Combining model checking with runtime verification helps us bridge the gap between software verification (discrete) that makes assumptions about the low-level controllers and the physical world, and the actual execution of the software on a real robotic platform in the physical world. To demonstrate the efficacy of our approach, we build a safe adaptive surveillance system and present software-in-the-loop simulations of the application. <s> BIB016 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Temporal Logics. <s> The Care-O-bot is an autonomous robotic assistant that can support people in domestic and other environments. The behaviour of the robot can be defined by a set of high level control rules. The adoption and further development of such robotic assistants is inhibited by the absence of assurances about their safety. In previous work, formal models of the robot behaviour and its environment were constructed by hand and model checkers were then used to check whether desirable formal temporal properties were satisfied for all possible system behaviours. In this paper we describe the details of the software CRutoN, that provides an automatic translation from sets of robot control rules into input for the model checker NuSMV. We compare our work with previous attempts to formally verify the robot control rules, discuss the potential applications of the approach, and consider future directions of research. <s> BIB017 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Temporal Logics. <s> Robotic technologies are continuously transforming the domestic and the industrial environments. Recently the Robotic Operating System (ROS), has been widely adopted both by industry and academia, becoming one of the most popular middleware frameworks for developing robot applications. Guaranteeing the correct behaviour of robotic systems is, however, challenging due to their potential for parameterization and heterogeneity. Although different approaches exist, focusing on concrete domain spaces for specific scenarios, no general approach to reason about ROS systems has yet arisen. This paper proposes an approach to model and verify ROS systems using real time properties, focusing on one of the main features of ROS, the communication between nodes. It takes low-level parameters into account, such as queue sizes and timeouts, and uses timed automata as the modelling language. The robot Kobuki is used as a complex case study, over which properties are automatically verified using the UPPAAL model checker, enabling the identification of problematic parameter combinations. <s> BIB018 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Temporal Logics. <s> Work in swarm robotics typically focuses on the bottom-up design of local rules for individual robots that create emergent swarm behaviors. In this paper, we take a top-down approach and consider the following problem: how can we specify a desired collective behavior and automatically synthesize decentralized controllers that can be distributed over robots to achieve the collective objective in a provably correct way? We propose a formal specification language for the high-level description of swarm behaviors on both swarm and individual levels. We present algorithms for automated synthesis of decentralized controllers and synchronization skeletons that describe how groups of robots must coordinate to satisfy the specification. We demonstrate our algorithms on a case study. <s> BIB019
Temporal logics are used for specifying dynamic properties about a system over linear or branching time, which feature heavily in the literature ( Table 2 ). There are a variety of temporal logics: Linear-time Temporal Logic (LTL) and Computation Tree Logic (CTL) deal with events occuring next, globally, or eventually; extensions like Probabilistic Temporal Logic (PTL) and Probabilistic Computation Tree Logic (PCTL) add notions of probability. Temporal logics have been used extensively to address the challenges that we identified in Section 3 and Section 4. Modeling a robot's environment is a key challenge when building robotic systems (Section 3.1). One approach BIB008 uses a BA to model the environment and synthesizes a motion controller by model-checking it to find an accepting path that satisfies an LTL task specification. The BA is updated at runtime with new environmental information and checked again to revise the motion controller. The work in BIB011 presents a probabilistic approach to modeling a BDI robotic agent and its environment. The agent can be captured as either a Discrete-Time Markov Chain (DTMC) or a Markov Decision Process (MDP). Then, they use PCTL to specify properties, which are modelchecked, using PRISM. They apply this technique to an autonomous mine detector, showing how their approach can be used for both design-time checking and runtime monitoring (which we discuss in Section 6.3). The runtime safety monitors for autonomous systems presented in BIB010 are specified in CTL. The work in BIB016 , aimed generally at safe robotics, captures assumptions about the real world using Signal Temporal Logic (STL) and uses them for runtime monitoring. Another example, this time aimed at robot swarms BIB012 , models the system's potential behavior and constrains it according to Supervisory Control Theory (SCT) specifications of safe behavior. Several approaches use temporal logic to provide certification evidence or build public trust in autonomous robotic systems. The work in BIB009 BIB004 captures air safety rules and assumptions using LTL (extended to capture BDI agent beliefs), which are used to verify that an autonomous pilotless aircraft follows the rules of the air in the same way as a pilot. Similarly,  and BIB017 present an approach for automatically building PTL models of the safety rules and environment of a robotic domestic assistant. These models are checked against a probabilistic description of the robot's environment (a sensor-equipped house in the United Kingdom) to ensure that the rules are sufficient to keep a human safe. An extension BIB013 checks models of the rules against environment models based on data collected from a person living in the house for several days. These verification results improve the confidence in the safety of the robot's high-level decision making. Enabling robots to deal with ethical choices is a current open challenge. One approach presents a BDI language, ETHAN BIB014 , for reasoning about ethical principles. It can be verified, using AJPF, that when an ETHAN agent chooses a plan, all other such plans are ethically worse. Another popular approach is synthesizing behavioral models that satisfy temporal logic properties. For example, in BIB002 , motion plans are built incrementally that guide the robot to its goal position while satisfying properties that are specified in a deterministic subset of μ-calculus. There is potential for using this approach at runtime; a plan can be built from a system of over 1,000 states in ∼3.5 seconds. In  , LTL specifications are used to synthesize robot motion automata. This approach mediates state explosion by planning a short distance ahead, repeating after each plan is complete. The work in BIB005 presents a tool that generates hybrid robot controllers from LTL specifications, which can be used in simulation or with real robots. Temporal logics have also been used to verify particular robotic software frameworks. The existing tool chain for G en oM has been extended to generate Fiacre models of a system, which can then be model-checked against LTL properties BIB015 . Another approach models ROS nodes, and the communication between them, as TA, which are checked against TCTL properties in Uppaal BIB018 . They verify the lack of message buffer overflows for a selection of queue sizes in the open-source robotic application Kobuki. Temporal logics have been used to help overcome some of the challenges in developing swarm robotic systems. Winfield et al. describe a dependable swarm BIB001 : a distributed multirobot system, based on the principles of swarm intelligence, that we can rely on the behavior of. They advocate the use of temporal logic for specifying both safety and liveness properties of a simple wireless connected swarm. As part of their approach, they discretize the robot's environment to a grid to simplify its specification. This is a common approach taken when using formal methods, since modeling continuous elements of the system is difficult. In a companion paper BIB006 , they apply model-checking techniques to the alpha swarm navigation algorithm. As mentioned in Section 4.2.1, swarm robotic systems exhibit both macroscopic and microscopic properties. The authors of BIB019 propose a novel specification language to allow the explicit specification both of the behavior of the whole swarm and of individual robots. Their language captures the swarm's environment as a region graph, describes the swarm's movement using region propositions, and specifies the swarm's macroscopic and microscopic behavior (separately) using LTL. These components are combined to produce decentralized controllers for the robot swarm. In contrast, BIB007 presents a technique for dealing with decentralized control in multiagent systems that keeps the specifications local to each robotic agent. Each local specification is written in LTL, with their mutual satisfiability not guaranteed beforehand. The local specifications are exchanged by the robots at physical meeting points and model-checked for mutual satisfiability. However, this technique assumes that dependencies between robotic agents are sparse, so it may not scale well in robot swarms or teams with a larger number of dependencies. Probabilistic temporal logics have proved useful in modeling robot swarms  . The work in BIB003 models the probabilistic state machine from  , which is checked in PRISM for satisfaction of PCTL properties. Since each robot in the swarm is characterized by the same state machine, a counting abstraction is used to reduce the state space, but this abstraction only works for homogeneous swarms. The work in  presents a top-down swarm development methodology that begins with a PCTL specification of the swarm's macroscopic requirements. Successively, more concrete models of the swarm are developed, including simulation and field-test implementations. Each step is checked against the previous steps to ensure that the swarm's behavior matches the initial specification. However, this approach only focuses on the macroscopic level of the behavior of the swarm; other approaches consider the microscopic level as well.