DCL Seminar Series: Sam Coogan

What can formal methods do for you?: Verifying and synthesizing control systems

No contact information submitted.
Sidebar Content
No sidebar content submitted.

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 Coogan Sam Coogan


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.



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.

Additional Information


Decision and Control Lab (DCL)

No categories were selected.
Related Core Research Areas
No core research areas were selected.
Newsroom Topics
No newsroom topics were selected.
DCL Seminar Series
  • Created By: mamstutz3
  • Workflow Status: Published
  • Created On: Oct 18, 2018 - 12:19pm
  • Last Updated: Oct 18, 2018 - 12:19pm