*********************************
There is now a CONTENT FREEZE for Mercury while we switch to a new platform. It began on Friday, March 10 at 6pm and will end on Wednesday, March 15 at noon. No new content can be created during this time, but all material in the system as of the beginning of the freeze will be migrated to the new platform, including users and groups. Functionally the new site is identical to the old one. webteam@gatech.edu
*********************************
Atlanta, GA | Posted: February 16, 2018
Summary Sentence:
What can formal methods do for you?: Verifying and synthesizing control systems
Full Summary:
What can formal methods do for you?: Verifying and synthesizing control systems
Sam CooganAbstract:
Formal methods were originally developed for specifying and verifying the correct behavior of software and hardware systems. This behavior can be specified, for example, using linear temporal logic (LTL). The power of LTL comes from its ability to concisely and intuitively express a wide range of relevant properties for system behavior. For example, a LTL formula may specify that some observation always holds (invariance), that some observation eventually holds (reachability), that some observation holds infinitely often (liveness), or that some particular observation always follows another observation (sequentiality). It is often straightforward to convert a plain English statement directly to a LTL formula.
An important research objective now is to ensure these formal methods are scalable, adaptable, and reliable when applied to physical control systems. The main challenge is that formal methods are designed for discrete systems and do not directly apply to systems with continuous state spaces. A common approach is to convert a continuous system into a finite abstraction that over-approximates the behavior of the original system. This abstraction is usually computed by partitioning the state-space into a finite set of regions, and at the heart of the abstraction algorithms are reachability computations. Computing reachable sets is generally a computationally expensive task, but efficient over-approximations lead to sound verification and synthesis algorithms that are translatable to the original control system. This talk will discuss the main ideas behind these abstraction-based approaches. We will discuss their strengths and weaknesses and highlight promising research directions.
Bio:
Sam Coogan received the B.S. degree in Electrical Engineering from Georgia Tech and the M.S. and Ph.D. degrees in Electrical Engineering from the University of California, Berkeley. In 2015, he was a postdoctoral research engineer at Sensys Networks, Inc., and in 2012 he was a research intern at NASA's Jet Propulsion Lab. Before joining Georgia Tech in 2017, he was an assistant professor in the Electrical Engineering department at UCLA from 2015–2017. He received a NSF CAREER award in 2018, the IEEE Transactions on Control of Network Systems Outstanding Paper Award in 2017, and the best student paper award at the 2015 Hybrid Systems: Computation and Control conference.
