Professor Calin Belta from the Department of Mechanical Engineering, Department of Electrical and Computer Engineering, and the Division of Systems Engineering at Boston University, presented a seminar on formal method for dynamical systems at the UTC-IASE. Professor Belta, who is also affiliated with the Center for Information and Systems Engineering (CISE) and the Bioinformatics Program, talked about an increasing need for computational tools for verification and control of complex systems from rich, temporal logic specifications. 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. The formal verification and synthesis problems have been shown to be undecidable even for very simple classes of infinite-space continuous and hybrid systems. The focus of this talk was on discrete time linear systems, for which it was 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 was illustrated with various examples.

To view more details or a video of the seminar, please visit http://iase.engr.uconn.edu/events/sem-lib/sl2016/.