Abstract: 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 infinite-space 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. The focus of this talk is on discrete-time
linear systems, for which 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. 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.
- This event has passed.