화학공학소재연구정보센터
IEEE Transactions on Automatic Control, Vol.63, No.1, 196-202, 2018
Mode-Target Games: Reactive Synthesis for Control Applications
In this paper, we introduce a class of linear temporal logic (LTL) specifications for which the problem of synthesizing controllers can be solved in polynomial time. The newclass of specifications is an LTL fragment that we term Mode Target (MT) and is inspired by numerous control applications where there are modes and corresponding (possibly multiple) targets for each mode. We formulate the problem of synthesizing a controller enforcing an MT specification as a game and provide an algorithm that requires O(Sigma(i) t(i)n(2)) symbolic steps, where n is the number of states in the game graph, and t(i) is the number of targets corresponding to mode i.