We provide a learning-based technique for guessing a winning strategy in a parity game originating from an LTL synthesis problem. A cheaply obtained guess can be useful in several applications. Not only can the guessed strategy be applied as best-effort in cases where the game's huge size prohibits rigorous approaches, but it can also increase the scalability of rigorous LTL synthesis in several ways. Firstly, checking whether a guessed strategy is winning is easier than constructing one. Secondly, even if the guess is wrong in some places, it can be fixed by strategy iteration faster than constructing one from scratch. Thirdly, the guess can be used in on-the-fly approaches to prioritize exploration in the most fruitful directions. In contrast to previous works, we (i)~reflect the highly structured logical information in game's states, the so-called semantic labelling, coming from the recent LTL-to-automata translations, and (ii)~learn to reflect it properly by learning from previously solved games, bringing the solving process closer to human-like reasoning.

翻译：我们提出了一种基于学习的技术，用于猜测来自LTL综合问题的对局游戏中获胜策略。通过廉价方式获得的猜测在多种应用中具有价值：不仅可以在游戏规模过大导致严格方法不可行时作为最佳努力策略应用，还能通过多种方式提升严格LTL综合的可扩展性。首先，验证猜测策略是否获胜比从头构建策略更容易；其次，即使猜测在某些位置有误，通过策略迭代修正也比重新构建更高效；第三，该猜测可用于在线方法中，将探索导向最有前景的方向。与先前工作相比，我们（i）反映了游戏状态中高度结构化的逻辑信息——即来自近期LTL到自动机翻译的所谓语义标注，并且（ii）通过从已解决游戏中学习来正确反映这种信息，使求解过程更接近人类推理方式。