Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> State-Transition Formalisms <s> The automata-theoretic approach to linear temporal logic uses the theory of automata as a unifying paradigm for program specification, verification, and synthesis. Both programs and specifications are in essence descriptions of computations. These computations can be viewed as words over some alphabet. Thus, programs and specifications can be viewed as descriptions of languages over some alphabet. The automata-theoretic perspective considers the relationships between programs and their specifications as relationships between languages. By translating programs and specifications to automata, questions about programs and their specifications can be reduced to questions about automata. More specifically, questions such as satisfiability of specifications and correctness of programs with respect to their specifications can be reduced to questions such as nonemptiness and containment of automata. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> State-Transition Formalisms <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> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> State-Transition Formalisms <s> Programming the behavior of multi-robot systems is a challenging task which has a key role in developing effective systems in many application domains. In this paper, we present Petri Net Plans (PNPs), a language based on Petri Nets (PNs), which allows for intuitive and effective robot and multi-robot behavior design. PNPs are very expressive and support a rich set of features that are critical to develop robotic applications, including sensing, interrupts and concurrency. As a central feature, PNPs allow for a formal analysis of plans based on standard PN tools. Moreover, PNPs are suitable for modeling multi-robot systems and the developed behaviors can be executed in a distributed setting, while preserving the properties of the modeled system. PNPs have been deployed in several robotic platforms in different application domains. In this paper, we report three case studies, which address complex single robot plans, coordination and collaboration. <s> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> State-Transition Formalisms <s> We model the dynamics of self-organized robot aggregation inspired by a study on the aggregation of gregarious arthropods. In swarms of German cockroaches, aggregation into clusters emerges solely from local interactions between the individuals, whereas the probabilities of joining or leaving a cluster are a function of the cluster size. We propose a non-spatial population dynamics model that keeps track of the number of robots in clusters of specific size using control parameters of the individual robots and the probability of detecting another robot in the environment. The model is able to quantitatively and qualitatively predict the dynamics observed in extensive realistic multi-robot simulation, and provides qualitative agreement with data obtained from aggregation of Blattela germanica larvae. In particular, we show by analysis, numerical and realistic simulation that the emergence of a single aggregate requires a minimal communication range between individuals. <s> BIB004 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> State-Transition Formalisms <s> The effective use of autonomous robot teams in highly-critical missions depends on being able to establish performance guarantees. However, establishing a guarantee for the behavior of an autonomous robot operating in an uncertain environment with obstacles is a challenging problem. This paper addresses the challenges involved in building a software tool for verifying the behavior of a multi-robot waypoint mission that includes uncertain environment geometry as well as uncertainty in robot motion. One contribution of this paper is an approach to the problem of a-priori specification of uncertain environments for robot program verification. A second contribution is a novel method to extend the Bayesian Network formulation to reason about random variables with different subpopulations, introduced to address the challenge of representing the effects of multiple sensory histories when verifying a robot mission. The third contribution is experimental validation results presented to show the effectiveness of this approach on a two-robot, bounding overwatch mission. <s> BIB005 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> State-Transition Formalisms <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> BIB006 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> State-Transition Formalisms <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> BIB007
Petri Nets, FSMs, and Finite-State Automata (FSA) are approaches to specifying behavior as a state-transition system. Formalisms for discrete-event systems include those capturing time (e.g., TA or Timed Petri Nets) and probabilistic transitions (e.g., PFSM or Generalized Stochastic Petri Net (GSPN)). State-transition systems specify behavior during the design phase, which is checked for properties like deadlock freedom or used as an input to a tool that usually checks them for properties described in another formal language (e.g., a temporal logic; see Section 5.3.1). There is a close link between varieties of temporal logic and varieties of FSA BIB001 , and many works combine both. Petri Nets have had some use in modeling robotic systems. The work in BIB002 uses them to capture the abstract architecture of multiple reactive agents and they are analyzed for deadlock freedom. In BIB003 , Ziparo et al. extend Petri Nets to capture robot plans. This extension to Petri Nets is a set, G, of Goal Markings, which is a proper subset of the reachable markings for the Petri Net that represents the desired result of the plan. The Petri Net Plans can be executed to find a sequence of transitions from the initial to the goal markings. Costelha and Lima  use four layers of Petri Nets to model a robot's task plans; each layer describes a distinct element at a different level of abstraction. They use Marked Ordinary Petri Nets (MOPNs) to specify the robot's environment to enable a more realistic model. Then they capture the actions that a robot can take, the task plans, and the roles of various robots working together, using GSPNs. These models can be analyzed for deadlocks and resource usage. The Uppaal model checker uses networks of TA to describe input models, which are checked against temporal logic properties. The work in BIB007 targets the ROS middleware framework, capturing the communication between nodes using TA. The low-level information (e.g., queue sizes and timeouts) allows the verification of safety and liveness properties with Uppaal. In  , TAs are used to model a decentralized traffic monitoring system and TCTL to describe system invariants and correctness properties of the system's self-adaptive behavior, which are verified using Uppaal. The work in BIB005 uses FSA and a Gaussian model of the environment, based on a probability distribution of obstacle positions. These models are combined in MissionLab, a graphical robot mission designer. The robot FSA models are automatically translated into MissionLab's internal process algebra, Process Algebra for Robot Schemas (PARS), which will be discussed in Section 5.4. As described in Section 4.1, Hoffmann et al. BIB006 extend PFSMs with a weight function to map weights onto actions, which they call an APFSM. Because of the addition of the weight function, an APFSM is a discrete-time Markov chain. They use this formalism to describe autonomous behavior and PRISM to verify properties about a pilotless aircraft on a foraging mission, with probabilistic modeling used to capture the physical environment. Markov chains have also been used to build models for predicting the likelihood of a robot swarm aggregating BIB004 . Each robot is represented by a Markov chain, where the probabilities to join or leave an aggregate are a function of the size of the aggregate (larger aggregates are preferred). The authors of BIB004 find that their model correlates closely with results from simulations.