Verification and Synthesis with Linear Temporal Logic Specifications

This talk introduces the basic principles on formal verification and synthesis for dynamical systems. The two problems lie at the intersection of control theory and computer science, and play a fundamental role in applications requiring correctness guarantees or involving complex task specifications. First, we introduce a formal specification language called Linear Temporal Logic (LTL), that can be used to encode in an unambiguous way rich temporal system properties. Next, we state the verification and synthesis problems given LTL formulae. Finally, we present an automata-based approach, where the dynamical system is represented as a finite abstraction, and the specification as a Buchi automaton. Illustrative examples are provided to highlight the introduced concepts and notation.