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 综合中的获胜策略

Guessing Winning Policies in LTL Synthesis by Semantic Learning

We study the characterization and computation of general policies for
families of problems that share a structure characterized by a common reduction
into a single abstract problem. Policies $\mu$ that solve the abstract problem
P have been shown to solve all problems Q that reduce to P provided that $\mu$
terminates in Q. In this work, we shed light on why this termination condition
is needed and how it can be removed. The key observation is that the abstract
problem P captures the common structure among the concrete problems Q that is
local (Markovian) but misses common structure that is global. We show how such
global structure can be captured by means of trajectory constraints that in
many cases can be expressed as LTL formulas, thus reducing generalized planning
to LTL synthesis. Moreover, for a broad class of problems that involve integer
variables that can be increased or decreased, trajectory constraints can be
compiled away, reducing generalized planning to fully observable
non-deterministic planning.

本文研究了具有共同特征的问题集合的一般策略的特征和计算，并介绍了如何通过利用轨迹约束以及 LTL 公式来消除策略的终止条件以及降低规划的复杂度。