Thursday, October 5, 2017 - 4:30pm
Event Calendar Category
LIDS & Stats Tea
Cristian Ioan Vasile
Building and Room Number
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.