ABSTRACT. In control theory, complex models of physical processes, such as systems of differential equations, are analyzed or controlled from simple specifications, such as stability and set invariance. In formal methods, rich specifications, such as formulae of temporal logics, are checked against simple models of software programs and digital circuits, such as finite transition systems. With the devel- opment and integration of cyber physical and safety critical systems, there is an increasing need for computational tools for verification and control of complex systems from rich, temporal logic specifications. In this talk, I will discuss a set of approaches to formal synthesis of control strategies for dynamical sys- tems from temporal logic specifications. I will first show how automata games for finite systems can be extended to obtain conservative control strategies for low dimensional linear and multilinear dynamical systems. I will then present several methods to reduce conservativeness and improve the scalability of the control synthesis algorithms for more general classes of dynamics. I will illus- trate the usefulness of these approaches with examples from robotics and traffic control.

ABSTRACT. We present work-in-progress to develop a hierarchical-control architecture for distributed autonomous systems. The new architecture comprises (i) a decentralised system-level control loop that partitions the goals of the distributed autonomous system among its components under conservative assumptions, and (ii) component-level control loops responsible for achieving the component sub-goals. The operation of the two control loops is underpinned by formal models that are small enough to enable their verification at runtime. To illustrate the use of our approach, we briefly describe its application to a multi-robot search and rescue mission.

ABSTRACT. We present DAMPC, a distributed, adaptive-horizon and adaptive-neighborhood algorithm for solving the stochastic reachability problem in a distributed-flocking modeled as a Markov decision process. At each time step, DAMPC takes the following actions: First, every agent calls a centralized, adaptive-horizon model-predictive control AMPC algorithm to obtain an optimal solution for its local neighborhood. Second, the agents derive the flock-wide optimal solution through a sequence of consensus rounds. Third, the neighborhood is adaptively resized using a flock-wide, cost-based Lyapunov function V. This improves efficiency without compromising convergence. The proof of statistical global convergence is non-trivial and involves showing that V follows a monotonically decreasing trajectory despite potential fluctuations in cost and neighborhood size. We evaluate DAMPC's performance using statistical model checking. Our results demonstrate that, compared to AMPC, DAMPC achieves considerable speed-up (7.5 in some cases) with only a slightly lower rate of convergence. The smaller average neighborhood size and lookahead horizon demonstrate the benefits of the DAMPC approach for stochastic reachability problems involving any distributed controllable system that possesses a cost function.

ABSTRACT. Machine learning systems typically involve complex decision making mechanisms while lack clear and concise specifications. Demonstrating the quality of machine learning systems therefore is a challenging task. We propose an approach combining formal methods and metamorphic testing for improving the quality of machine learning systems. In particular, our framework enables the possibility of developing policing functions for runtime monitoring machine learning systems based on metamorphic relations.

ABSTRACT. This abstract considers the problem of how autonomous systems might incorporate accounting for first (and higher order) norms in their own actions and those of others, through on-the-fly symbolic model-checking of (multiple) institutional models.

ABSTRACT. Developing advanced robotics and autonomous applications is now facing the confidence issue for their acceptability in everyday life. This confidence could be justified by the use of dependability techniques as it is done in other safety- critical applications. However, due to specific robotic properties (such as continuous physical interaction or non-deterministic decisional layer), many techniques need to be adapted or revised. This presentation will introduce these major issues for autonomous systems, and focus on current research work at LAAS in France, on model-based risk analysis for physical human-robot interactions, active safety monitoring for autonomous systems, and testing in simulation of mobile robot navigation.

ABSTRACT. A new concept for railway autonomous inspection and repair is being developed for the UK’s national railway. The new system aims at reducing human interventions at highly hazardous locations such as tunnels; while simultaneously inspecting and repairing rail components autonomously. It is envisioned that the new system will be deployed using a robotic arm mounted on a road-rail vehicle. Different routes for verification and validation at different levels are being evaluated. In the first level, the new system concept design will be validated by breaking it down into sublevel components and individually assessing integration, interfacing and structure. A second level will use a “digital twin” approach to simulate appropriate outputs for the tests, e.g. simple i/o for sub-systems and if appropriate, extended work into three-dimensional views. Finally a third lower level will validate and verify the inspection capability and its robotic arm interfacing. This will use a combination of modelled data and part inspection measurements.

ABSTRACT. We describe work that was presented at the NASA Formal Methods Symposium and published in the symposium proceedings. We give an overview of the probabilistic models that we presented for autonomous agent search and retrieve missions. We summarise how probabilistic model checking and the probabilistic model checker PRISM were used for optimal strategy generation with a view to returning the generated strategies to the UAV embedded within controller software.

ABSTRACT. A new verification framework is presented for the decision making of autonomous vehicles (AVs). The overall structure of the framework consists of: (1) A perception system of sensors that feed into a (2) a reasoning agent based on a Jason architecture that operates onboard an AV and interacts with a (3) model of the environment. The agent relies on a set of rules, planners and actions to achieve its ultimate goal of driving the AV safely from a starting point to its destination. The verification framework deploys an innovative combination of two well known verification tools: (1) the model checker for multi-agent systems (MCMAS) to check the consistency and stability of the agent rules before choosing any action and (2) the PRISM probabilistic model checker to provide the agent with the probability of success when it decides to take a planned movement sequence. The agent will select the movement-actions with the highest probability of success. The planned actions are executed by a control system to control the movement of the AV on the ground using a set of primitive movement skills using its actuators. The framework uses the Robot Operating System (ROS) to implement the reasoning agent and the Gazebo Simulator to model the AV, its sensors and the surrounding environment. The agent connects to a MATLAB-based perception and control system to steer the AV.

ABSTRACT. We propose a description language for formalising the ``Rules of the Road" (e.g., the UK Highway Code). By way of example, we represent the subset of the Highway Code responsible for road junctions and represent these Rules of the Road using linear temporal logic, LTL. Our aim is to ``extract" from this generic representation a set of beliefs, goals and plans that can be used by a BDI agent to augment its universal autonomous vehicle control (e.g., route planning and obstacle avoidance capabilities) with region-specific rules for road use. We intend to target the Gwendolen agent programming language as a prototype for this system, which provides formal verification possibilities.

ABSTRACT. The range of difficulties that can occur when running an experimental study in robotics is broad. Subjects can behave in unforeseen ways, rendering the experimental scenario inconclusive, or misunderstand questionnaire items or instructions. The robot may exhibit seemingly random physical behaviors, or break down in the middle of the experiment. To increase the intricacy, imagine the experiment being reproduced in another lab, research field, or country by other researchers with a regular research publication as their only starting point. Furthermore, assume that the publication is in an interdisciplinary research field, like social robotics or HRI, in which authors from different fields often carry different levels of knowledge and disciplinary interest about the social science methodologies, the technical system, and the conceptual background of the work. Based on my experience in the field, I will introduce and discuss the ”big five” issues of reproducible robotics from both, a developer’s and also from a reviewer’s perspective. The discussed topics range from technical, to methodological, to social aspects of reproducible robotics and are motivated by applied ”real life” projects and scenarios.

ABSTRACT. We propose to demonstrate the application of RoboChart and its associated tool, RoboTool, for the verification and validation of robotic applications. In our demonstration, we will consider a few small examples for illustration, and the larger example of a transporter. It is part of a swarm and cooperates with other identical robots to push an object to a target location.

ABSTRACT. In this demo, we will illustrate our work on integrating formal verification techniques, in particular probabilistic model checking, to enable long term deployments of mobile service robots in everyday environments. Our framework is based on generating policies for Markov decision process (MDP) models of mobile robots, using (co-safe) linear temporal logic specifications. More specifically, we build MDP models of robot navigation and action execution where the probability of successfully navigating between two locations and the expected time to do so are learnt from experience. For a specification over these models, we maximise the probability of the robot satisfying it, and minimise the expected time to do so. The policy obtained for this objective can be seen as a robot plan with attached probabilistic performance guarantees.

Our proposal is to showcase this framework live during the workshop, deploying our robot in the workshop venue and having it perform tasks throughout the day (the robot is based in the Oxford Robotics Institute, hence it can be easily moved to the workshop venue). In conjunction with showing the live robot behaviour, we will, among other things, provide visualisation of the generated policies on a map of the environment; showcase how the robot keeps track of the performance guarantees calculated offline during policy execution; and show how these guarantees can be used for execution monitoring.