Venue: MS Teams ( for event link, please email amgrad@uwaterloo.ca)
Candidate
Zhibing Sun | Applied Mathematics, University of Waterloo
Title
Control of Non-deterministic Transition Systems for Linear Temporal Logic Specifications
Abstract
Consider the formal synthesis problem in the continuous dynamical systems. A systematic approach is the abstraction-based method: constructing the abstraction of the original continuous system in the discrete space, and then consider the control problem in the abstraction. We consider our abstraction as a Non-deterministic Transition System (NTS), and describe our control specifications as Linear Temporal Logic (LTL) formulas. The standard procedure is to convert the LTL formula as a Deterministic Automaton (DA) with a corresponding accepting condition, taking the product of NTS and DA, and then solve it as an infinite game in the product space. The winning condition of the infinite game corresponds to the accepting condition of the DA, which often has polynomial or even exponential theoretical worst case time complexity.
With the development of the computation platform, the enormous scale of the NTS becomes relatively affordable. However, practical implementations still require the infinite game being solved in linear time. This motivates us to explore the feasibility of the abstraction-based method in implementations. We give detailed analysis of each game from an algorithmic and implementation perspective to show that the theoretical upper bound is indeed too loose in practice. Better still, we implement a program to systematically solve for the control specifications as general as Deterministic B¨uchi Automaton (DBA) translatable LTL formulas. The experimental results show that the program always terminates within one or two iterations. We conclude that as a result of the huge gap between theory and implementation, we can expect a linear time complexity to solve for the infinite game in practice, thus it is feasible to solve complicated specifications efficiently using abstraction-based method.