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 an 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 the 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 more powerful computation platforms, the enormous scale of the NTS with millions of states and billions of transitions becomes relatively affordable. Such space complexity suggests that practical implementations should solve the infinite games in linear time at most. This motivates us to examine the gap between theoretical complexity upper bounds for solving infinite games and the run-time complexity of practical implementations of abstraction-based methods for solving temporal logic control problems. We give detailed analysis of different games such as reachability, safety, B¨uchi, co-B¨uchi, generalized B¨uchi, generalized co-B¨uchi, and Rabin from an algorithmic and implementation perspective to try to show that the theoretical upper bound is indeed too loose in practice. Better still, we implement an efficient B¨uchi solver to systematically solve for the control specifications as general as deterministic B¨uchi automata (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 methods.