Loading Events

« All Events

  • This event has passed.

Spring 2013 GRASP Seminar: Calin Belta, Boston University, “Formal Methods for Discrete-Time Linear Systems”

February 15, 2013 @ 11:00 am - 12:00 pm

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
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.


- Learn More

Calin Belta is an Associate Professor in the Department of Mechanical
Engineering, Department of Electrical and Computer Engineering, and the
Division of Systems Engineering at Boston University, where he is also
affiliated with the Center for Information and Systems Engineering
(CISE), the Bioinformatics Program, and the Center for Biodynamics
(CBD). His research focuses on dynamics and control theory, with
particular emphasis on hybrid and cyber-physical systems, formal
synthesis and verification, and applications in robotics and systems
biology. Calin Belta is a Senior Member of the IEEE and an Associate
Editor for the SIAM Journal on Control and Optimization (SICON). He
received the Air Force Office of Scientific Research Young Investigator
Award and the National Science Foundation CAREER Award.


February 15, 2013
11:00 am - 12:00 pm
Event Category: