Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Agent-Based Systems <s> The study of computational agents capable of rational behaviour has received a great deal of attention in recent years. Theoretical formalizations of such agents and their implementations have proceeded in parallel with little or no connection between them. Tkis paper explores a particular type of rational agent, a BeliefDesire-Intention (BDI) agent. The primary aim of this paper is to integrate (a) the theoretical foundations of BDI agents from both a quantitative decision-theoretic perspective and a symbolic reasoning perspective; (b) the implementations of BDI agents from an ideal theoretical perspective and a more practical perspective; and (c) the building of large-scale applications based on BDI agents. In particular, an air-trafflc management application will be described from both a theoretical and an implementation perspective. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Agent-Based Systems <s> The Procedural Reasoning System (PRS) is the best established agent architecture currently available. It has been deployed in many major industrial applications, ranging from fault diagnosis on the space shuttle to air traffic management and business process control. The theory of PRS-like systems has also been widely studied: within the intelligent agents research community, the belief-desire-intention (BDI) model of practical reasoning that underpins PRS is arguably the dominant force in the theoretical foundations of rational agency. Despite the interest in PRS and BDI agents, no complete attempt has yet been made to precisely specify the behaviour of real PRS systems. This has led to the development of a range of systems that claim to conform to the PRS model, but which differ from it in many important respects. Our aim in this paper is to rectify this omission. We provide an abstract formal model of an idealised dMARS system (the most recent implementation of the PRS architecture), which precisely defines the key data structures present within the architecture and the operations that manipulate these structures. We focus in particular on dMARS plans, since these are the key tool for programming dMARS agents. The specification we present will enable other implementations of PRS to be easily developed, and will serve as a benchmark against which future architectural enhancements can be evaluated. <s> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Agent-Based Systems <s> Multi-agent systems provide an increasingly popular solution in problem domains that require management of uncertainty and a high degree of adaptability. Robustness is a key design criterion in building multi-agent systems. We present a novel approach for the design of robust multi-agent systems. Our approach constructs a model of the design of a multi-agent system in Alloy, a declarative language based on relations, and checks the properties of the model using the Alloy Analyzer, a fully automatic analysis tool for Alloy models. While several prior techniques exist for checking properties of multi-agent systems, the novelty of our work is that we can check properties of coordination and interaction, as well as properties of complex data structures that the agents may internally be manipulating or even sharing. This is the first application of Alloy to checking properties of multi-agent systems. Such unified analysis has not been possible before. We also introduce the use of a formal method as an integral part of testing and validation. <s> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Agent-Based Systems <s> While temporal logic in its various forms has proven essential to reason about reactive systems, agent-based scenarios are typically specified by considering high-level agents attitudes. In particular, specification languages based on epistemic logic [7], or logics for knowledge, have proven useful in a variety of areas including robotics, security protocols, web-services, etc. For example, security specifications involving anonymity [4] are known to be naturally expressible in epistemic formalisms as they explicitly state the lack of different kinds of knowledge of the principals. <s> BIB004 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Agent-Based Systems <s> The paper addresses formal systems verification of autonomous underwater vehicles (AUV). The verification process includes hybrid system modelling and formulation of the discrete representation using natural language programming (sEnglish) via compositional abstraction - employing data, perception and action abstraction methods; the translation of the discrete abstraction into interpreted script programming language (ISPL) of a mainstream multi-agent model checker (MCMAS) for reachability verification of undesirable states, and ultimately the bridging into the discrete event system representation in Stateflow formalism. Using this technique, modelling and model checking can include the complete physical system of the autonomous vehicle, its multi-agent software on board and also the human interface represented as an agent. <s> BIB005 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Agent-Based Systems <s> We here address the modelling and analysis of human-agent teamwork, specifically in the context of proposed astronaut-robot collaboration in future space missions. We are particularly interested in modelling such systems at a level that allows formal verification techniques to be applied, and hence carry out sophisticated analysis of the reliability and effectiveness of the teams before the system is deployed in real scenarios. In this paper we describe our ongoing research in this area. <s> BIB006 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Agent-Based Systems <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> BIB007 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Agent-Based Systems <s> In this paper we describe a verification system for multi-agent programs. This is the first comprehensive approach to the verification of programs developed using programming languages based on the BDI (belief-desire-intention) model of agency. In particular, we have developed a specific layer of abstraction, sitting between the underlying verification system and the agent programming language, that maps the semantics of agent programs into the relevant model-checking framework. Crucially, this abstraction layer is both flexible and extensible; not only can a variety of different agent programming languages be implemented and verified, but even heterogeneous multi-agent programs can be captured semantically. In addition to describing this layer, and the semantic mapping inherent within it, we describe how the underlying model-checker is driven and how agent properties are checked. We also present several examples showing how the system can be used. As this is the first system of its kind, it is relatively slow, so we also indicate further work that needs to be tackled to improve performance. <s> BIB008 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Agent-Based Systems <s> Deep space missions are characterized by severely constrained communication links. To meet the needs of future missions and increase their scientific return, future space systems will require an increased level of autonomy on-board. In this work, we propose a comprehensive approach to on-board autonomy relying on model-based reasoning, and encompassing many important reasoning capabilities such as plan generation, validation, execution and monitoring, FDIR, and run-time diagnosis. The controlled platform is represented symbolically, and the reasoning capabilities are seen as symbolic manipulation of such formal model. We have developed a prototype of our framework, implemented within an on-board Autonomous Reasoning Engine. We have evaluated our approach on two case-studies inspired by real-world, ongoing projects, and characterized it in terms of reliability, availability and performance. <s> BIB009 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Agent-Based Systems <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> BIB010 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Agent-Based Systems <s> The focus of the paper is how to model autonomous behaviours of heterogeneous multi-agent systems such that it can be verified that they will always operate within predefined mission requirements and constraints. This is done by using formal methods with an abstraction of the behaviours modelling and model checking for their verification. Three case studies are presented to verify the decision-making behaviours of heterogeneous multi-agent system using a convoy mission scenario. The multi-agent system in a case study has been extended by increasing the number of agents and function complexity gradually. For automatic verification, model checker for multi-agent systems (MCMAS) is adopted due to its novel capability to accommodate the multi-agent system and successfully verifies the targeting behaviours of the team-level autonomous systems. The verification results help retrospectively the design of decision-making algorithms improved by considering additional agents and behaviours during three steps of sce... <s> BIB011 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Agent-Based Systems <s> The coordination of multiple autonomous vehicles into convoys or platoons is expected on our highways in the near future. However, before such platoons can be deployed, the new autonomous behaviors of the vehicles in these platoons must be certified. An appropriate representation for vehicle platooning is as a multi-agent system in which each agent captures the "autonomous decisions" carried out by each vehicle. In order to ensure that these autonomous decision-making agents in vehicle platoons never violate safety requirements, we use formal verification. However, as the formal verification technique used to verify the agent code does not scale to the full system and as the global verification technique does not capture the essential verification of autonomous behavior, we use a combination of the two approaches. This mixed strategy allows us to verify safety requirements not only of a model of the system, but of the actual agent code used to program the autonomous vehicles. <s> BIB012 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Agent-Based Systems <s> Formal verification of agents representing robot behaviour is a growing area due to the demand that autonomous systems have to be proven safe. In this paper we present an abstract definition of autonomy which can be used to model autonomous scenarios and propose the use of small-scale simulation models representing abstract actions to infer quantitative data. To demonstrate the applicability of the approach we build and verify a model of an unmanned aerial vehicle (UAV) in an exemplary autonomous scenario, utilising this approach. <s> BIB013 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Agent-Based Systems <s> The spread of autonomous systems into safety-critical areas has increased the demand for their formal verification, not only due to stronger certification requirements but also to public uncertainty over these new technologies. However, the complex nature of such systems, for example, the intricate combination of discrete and continuous aspects, ensures that whole system verification is often infeasible. This motivates the need for novel analysis approaches that modularise the problem, allowing us to restrict our analysis to one particular aspect of the system while abstracting away from others. For instance, while verifying the real-time properties of an autonomous system we might hide the details of the internal decision-making components. In this paper we describe verification of a range of properties across distinct dimensions on a practical hybrid agent architecture. This allows us to verify the autonomous decision-making, real-time aspects, and spatial aspects of an autonomous vehicle platooning system. This modular approach also illustrates how both algorithmic and deductive verification techniques can be applied for the analysis of different system subcomponents. <s> BIB014
An agent encapsulates the system's decision-making capability into one component. This helps to provide rational autonomy (where a system can explain its reasoning), which is crucial for providing evidence to gain public trust or for certification (discussed in Section 3.2). Since the implementation of the Procedural Reasoning System (PRS)  , Belief-Desire-Intention (BDI) agents received a great deal of attention BIB001 . BDI systems can use a single or multiple agents, depending on their requirements. The BDI model of agency appears to be prevalent in the surveyed literature. The distributed Multiagent Reasoning System (dMARS) is an implementation of PRS with the BDI model operationalized by plans BIB002 . A formal Z specification of dMARS provides a formal foundation for the semantics of dMARS agents BIB002 . These agents monitor both the world and their own internal state. They are composed predominantly of a plan library, functions for intention, event and plan selection, belief domain, and goal domain BIB002 . Webster et al. BIB010 BIB007 verify an autonomous pilotless aircraft using a program model checker. The aircraft is controlled by a BDI agent, written in the GWENDOLEN language  , and verified by the AJPF model checker BIB008 . The verified agent is plugged into a flight simulator BIB010 to visualize the verified scenarios. The work in BIB012 BIB014 describes a GWENDOLEN agent controlling a driverless car in a vehicle platoon. AJPF is used to verify safety properties related to the car joining and leaving a platoon, and for maintaining a safe distance during platooning. Verification of the timing properties is handled by Uppaal. Similarly, Choi et al. model a system of nine heterogeneous agents with one representing the robot's physical environment BIB011 . They used the Model Checker for Multigent Systems (MCMAS) BIB004 to verify the system and illustrated that MCMAS performed dramatically better than SMV in this setting. Molnar and Veres also used MCMAS to verify autonomous underwater vehicles BIB005 . They use natural language programming (sEnglish), which results in an ontology that is used to represent a labeled transition system. This is then translated into Stateflow and verified with MCMAS. Interestingly, they represent the human interface as an agent, as does BIB006 . This links human behavior and the formal model that they have developed. Hoffmann et al. characterize the autonomous behavior of an agent (based on the BDI model) as a PFSM extended with a weight function to map weights onto actions, which they call an Autonomous Probabilistic Finite-State Machine (APFSM) BIB013 . Due to the addition of the weight function, an APFSM is a discrete-time Markov chain. They use this formalism of agent autonomy to verify properties about a pilotless aircraft on a foraging mission. Bozzano et al. BIB009 propose the Autonomous Reasoning Engine (ARE) for controlling spacecraft; it provides plan generation, validation, execution, monitoring, and fault detection. It communicates with the ground station, performs autonomous reasoning, receives sensor data, and sends commands to actuators. A prototype ARE, developed using NuSMV, has been used in ESA rover and satellite projects to provide a model-based approach to on-board autonomy. Podorozhny et al. BIB003 use Alloy to verify multiagent negotiations. Their work enables properties of agent coordination and interaction to be checked and properties of complex data structures (which may be shared between agents). Their work centers on a system where multiple agents cooperate to reach and negotiate to optimize achieving their common goal(s). They model agents' negotiations as Finite-State Machines (FSMs), which are then translated into an Alloy specification and verified using Alloy Analyzer. The main challenge was ensuring tractability of the Alloy models.