When: Thursday, June 11, 2020, 3pm.

Where: Google Meet, check the address in the Google Calendar Event.

Topic: Program Synthesis of Linear Temporal Logic over Finite Traces.

Speaker: Shufang Zhu

Abstract

Program synthesis is an approach of automatically designing a system that interacts continuously with an environment, using a declarative specification of the system’s behaviors. A popular language for providing such a specification is Linear Temporal Logic, or LTL for short. Standard LTL synthesis, however, is a hard problem to solve in practice. Therefore, many works have targeted on developing specific techniques for certain subclasses of LTL and obtained significant results, for example, GR(1). In this work, we focus on a new logic, Linear Temporal Logic over finite traces, or LTLf, which interprets LTL formulas semantically on finite traces. Such interpretation allows for arbitrarily long but finite executions of the system, and is adequate for finite-horizon problems in Computer Science and Artificial Intelligence. In particular, we study here the problem of LTLf synthesis. The contributions of this dissertation are summarized as follows:

  • We introduce a symbolic LTLf synthesis framework;
  • We present a comprehensive study of different encodings for the translation to DFA from LTLf formulas;
  • We investigate the power of automata minimization in LTLf synthesis;
  • We generalize our symbolic LTLf framework to LTLf synthesis with simple fairness assumptions.

Material