Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Teams. <s> This article deals with the problem of dynamic role-playing in Multi-Agent organisations. The approach presented uses a formal specification notation and is based upon a formal framework which defines the concepts of role, interaction and organisation. Within this framework the problem of dynamic role-playing specification is related to the merging of specifications. The formal notation used composes Object-Z and Statecharts. The main features of this approach are: enough expressive power to represent Multi-Agents dynamic aspects, tools for specification analysis and mechanisms allowing the refinement of a high level specification into a low level specification which can be easily implemented. The last part of this paper presents an application with the specification of a reactive and cooperative MAS model named Satisfaction Altruism. An analysis of the specification validates the agents' behaviours. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Teams. <s> In this paper, we develop a computational framework for fully automatic deployment of a team of unicycles from a global specification given as an LTL formula over some regions of interest. Our hierarchical approach consists of four steps: (i) the construction of finite abstractions for the motions of each robot, (ii) the parallel composition of the abstractions, (iii) the generation of a satisfying motion of the team; (iv) mapping this motion to individual robot control and communication strategies. The main result of the paper is an algorithm to reduce the amount of inter-robot communication during the fourth step of the procedure. <s> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Teams. <s> Beliefs play an important role in human-robot teaming scenarios, where the robots must reason about other agents' intentions and beliefs in order to inform their own plan generation process, and to successfully coordinate plans with the other agents. In this paper, we cast the evolving and complex structure of beliefs, and inference over them, as a planning and plan recognition problem. We use agent beliefs and intentions modeled in terms of predicates in order to create an automated planning problem instance, which is then used along with a known and complete domain model in order to predict the plan of the agent whose beliefs are being modeled. Information extracted from this predicted plan is used to inform the planning process of the modeling agent, to enable coordination. We also look at an extension of this problem to a plan recognition problem. We conclude by presenting an evaluation of our technique through a case study implemented on a real robot. <s> BIB003
A robot team is similar to a swarm but contains robots with different capabilities or behaviors to one another. For example, a search-and-rescue robot team might contain an autonomous aircraft to search the area, a wheeled robot to carry equipment, and a robot with caterpillar tracks that is capable of moving obstacles. The heterogeneity of the robot's capabilities and behavior increases the likelihood that they will each need different formal methods during verification. Linking verification at the micro-level to the macro-level is therefore challenging. We discuss the use of integrated formal methods in more detail in Section 6.4. The work in BIB002 presents a methodology for automating the development of robot teams, using a version of Linear Time Logic without the "next" operator (LTL-X). They model-check a transition system describing the behavior of the robot team for execution traces that satisfy an LTL-X formula. This trace is mapped to the communication and control strategy for each robot. Büchi Automata (BA) then produce a communication strategy that reduces the number of "stop and wait" synchronizations that the team has to perform. Robot teams often include robots with different capabilities, which produce different patterns of interaction. The work in BIB001 captures part of the Satisfaction-Altruism Model  to provide a formal model of the different and changing roles that different agents in a team can play. Each role defines a pattern of interaction. They propose using their model for specification and verification of a robotic team, and eventual refinement to code. Their model is formalized using an integrated formal method (discussed in Section 6.4) that combines Object-Z and Statecharts  . Previous work in this area has assumed that a robot and a human are in close contact and that the robot can continually observe the human's behavior, allowing it to predict the human's plan. Talamadupula et al. BIB003 describe a First-Order Logic (FOL) formalization of beliefs and intentions that allows a robot to predict another agent's plan. They explore a human-robot cooperation task where the robot must predict a human's plan based on mutually understood beliefs and intentions. The FOL predicates representing the beliefs and intentions of another agent (human or robotic) are input to the robot's planning system, which predicts the other agent's plan. An extension caters to incomplete knowledge of the other agent's goals.