In this paper, we study the structure of underlying automata based constructions for solving the LTL realizability and synthesis problem. We show how to reduce the LTL realizability problem to a game with an observer that checks that the game visits a bounded number of times accepting states of a universal co-Buchi word automaton. We show that such an observer can be made deterministic and that this deterministic observer has a nice structure which can be exploited by an incremental algorithm that manipulates antichains of game positions. We have implemented this new algorithm and our first results are very encouraging.
展开▼
机译：在本文中，我们研究了基于底层自动机的结构，用于解决LTL可实现性和合成问题。我们展示了如何使用观察者将LTL可实现性问题减少到游戏中，该方法检查游戏访问通用CO-BUCHI Word Automaton的状态的有界次数。我们表明这种观察者可以确定，并且该确定性观察者具有漂亮的结构，可以通过操纵游戏位置的AntiChains的增量算法利用。我们已经实施了这种新算法，我们的第一个结果非常令人鼓舞。
展开▼
