ABSTRACT:

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: