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 development 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 systems 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 illustrate 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 (2 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. 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.

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 (2) a reasoning agent based on a Jason architecture that operates on-board an AV and interacts  with a model of the environment using (3) multi-input multi-output adaptive control system.  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 logic rules and perception-based beliefs 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 adopts the Jason agent paradigm to design the reasoning and the decision making process. The Robot Operating System (ROS) and the Gazebo Simulator are used 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.