Formal Methods for Dynamical Systems
In control theory, “complex” models of physical processes, such as systems of differential equations, are usually checked against “simple” specifications, such as stability and set invariance. In formal methods, “rich” specifications, such as languages and formulae of temporal logics, are checked against “simple” models of software programs and digital circuits, such as finite transition graphs. 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.
The formal verification and synthesis problems have been shown to be undecidable even for very simple classes of infinitespace continuous and hybrid systems. However, provably correct but conservative approaches, in which the satisfaction of a property by a dynamical system is implied by the satisfaction of the property by a finite over-approximation (abstraction) of the system, have received a lot of attention in recent years.
Some classes of systems allowing for computationally efficient verification and control from temporal logic specifications are reviewed. For continuous and discrete-time linear systems and continuous-time multi-linear systems, it is shown that finite abstractions can be constructed through polyhedral operations only. By using techniques from model checking and automata games, this allows for verification and control from specifications given as Linear Temporal Logic (LTL) formulae over linear predicates in the state variables. A connection between the existence of Lyapunov functions and finite bisimulations is established for discrete-time linear and switched linear systems. Finally, optimality and correctness requirements are combined in a model predictive approach to generate control strategies for discrete-time linear systems.
The usefulness of these computational tools is illustrated with various examples such as verification and synthesis of biological circuits in synthetic biology and motion planning and control in robotics.
Alessio R. Lomuscio
Advances in symbolic model checking for multi-agent systems.
Multi-agent systems (MAS) are distributed autonomous systems
in which the components, or agents, act autonomously or collectively
in order to reach private or common goals. Logic-based specifications
for MAS typically do not only involve their temporal evolution, but
also other agent attitudes, including their knowledge, intentions,
their strategic abilities, etc.
This talk will survey some of our work on model checking MAS against
agent-based specifications. Serial and parallel algorithms for
symbolic model checking against temporal-epistemic specifications as
well as bounded-model checking procedures will be discussed. MCMAS, an
open-source model checker, developed in the VAS group at Imperial
College London, will be briefly demonstrated. A case study concerning
the verification of diagnosability and fault-tolerance of an autonomous
underwater vehicles will be discussed.
I will conclude by considering the case of open MAS where the number of
agents is unbounded. In this context I will report recent results that
enable us to establish a cut-off of a MAS, i.e., the maximal number of
agents that need to be verified for conclusions to be drawn on any
system of any number of components.