UTRC CDS Lecture: Calin Belta, "Formal Methods for Dynamical Systems"

Friday, September 12, 2014
2:00 p.m.
1146 AV Williams Building

United Technologies Research Center
Invited Lectures on Control and Dynamical Systems

Formal Methods for Dynamical Systems

Calin Belta
Associate Professor
Department of Mechanical Engineering, Department of Electrical and Computer Engineering, and the Division of Systems Engineering
Boston University

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.

Biography
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) and the IEEE Transactions on Automatic Control. He received the Air Force Office of Scientific Research Young Investigator Award and the National Science Foundation CAREER Award.

Audience: Graduate  Undergraduate  Post-Docs  Alumni  Corporate 

remind we with google calendar

 

October 2024

SU MO TU WE TH FR SA
29 30 1 2 3 4 5
6 7 8 9 10 11 12
13 14 15 16 17 18 19
20 21 22 23 24 25 26
27 28 29 30 31 1 2
Submit an Event