Verification and Synthesis with Linear Temporal Logic Specifications

Thursday, October 5, 2017 - 4:30pm

Event Calendar Category

LIDS & Stats Tea

Speaker Name

Cristian Ioan Vasile

Affiliation

LIDS

Building and Room Number

LIDS Lounge

Abstract

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.

Biography