Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Other Logics. <s> We present a novel formal verification approach for collective robotic systems that is based on the use of the formal language Klaim and related analysis tools. While existing approaches focus on either micro- or macroscopic views of a system, we model aspects of both the robot hardware and behaviour, as well as relevant aspects of the environment. We illustrate our approach through a robotics scenario, in which three robots cooperate in a decentralized fashion to transport an object to a goal area. We first model the scenario in Klaim. Subsequently, we introduce random aspects to the model by stochastically specifying actions execution time. Unlike other approaches, the specification thus obtained enables quantitative analysis of crucial properties of the system. We validate our approach by comparing the results with those obtained through physics-based simulations. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Other Logics. <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> BIB002
We identified a number of other logics that were not numerous enough for their own category. Dylla et al. [64] formalize the basic concepts of football theory (from a leading football theory manual) using Readylog, which is a variant of the logic programming language Golog. They use this formalization to formally describe football tactics, which they implement on football-playing robots for the RoboCup competition. Gjondrekaj et al. BIB001 use a formal language that has been designed to capture properties about distributed systems, Klaim; its stochastic extension, StoKlaim; and their related tool set. Their application domain is distributed robotic systems and they describe the modeling of three homogeneous robots, under distributed control, cooperating to transport objects. Talamadupula et al. BIB002 use FOL to capture an agent's beliefs and intentions. They use this to enable the prediction of other agents' plans.