In this paper, we study LTLf synthesis under environment specifications for
arbitrary reachability and safety properties. We consider both kinds of
properties for both agent tasks and environment specifications, providing a
complete landscape of synthesis algorithms. For each case, we devise a specific
algorithm (optimal wrt complexity of the problem) and prove its correctness.
The algorithms combine common building blocks in different ways. While some
cases are already studied in literature others are studied here for the first
time.

本文研究了针对任意可达性和安全性属性的环境规范下的 LTLf 综合，考虑了代理任务和环境规范的两种属性，提供了一系列完整的综合算法。针对每种情况，我们设计了一个特定算法（关于问题复杂性最优），并证明了其正确性。这些算法通过不同的方式组合了常见的构建模块。虽然一些情况已经在文献中得到研究，但其他情况本文首次进行了研究。

LTLf 合成关于可达性和安全性质的环境规范

LTLf Synthesis Under Environment Specifications for Reachability and  Safety Properties

Most of the synthesis literature has focused on studying how to synthesize a
strategy to fulfill a task. This task is a duty for the agent. In this paper,
we argue that intelligent agents should also be equipped with rights, that is,
tasks that the agent itself can choose to fulfill (e.g., the right of
recharging the battery). The agent should be able to maintain these rights
while acting for its duties. We study this issue in the context of LTLf
synthesis: we give duties and rights in terms of LTLf specifications, and
synthesize a suitable strategy to achieve the duties that can be modified
on-the-fly to achieve also the rights, if the agent chooses to do so. We show
that handling rights does not make synthesis substantially more difficult,
although it requires a more sophisticated solution concept than standard LTLf
synthesis. We also extend our results to the case in which further duties and
rights are given to the agent while already executing.

本文研究了智能代理应该如何配备权利以满足它可以选择执行的任务，并通过 LTLf 合成进行了实现。我们证明了处理权利并不会使合成过程变得更加困难，但需要一个比标准 LTLf 合成更复杂的解决方案概念。

履行职责，保障权益

Act for Your Duties but Maintain Your Rights

LTLf synthesis is the automated construction of a reactive system from a
high-level description, expressed in LTLf, of its finite-horizon behavior. So
far, the conversion of LTLf formulas to deterministic finite-state automata
(DFAs) has been identified as the primary bottleneck to the scalabity of
synthesis. Recent investigations have also shown that the size of the DFA state
space plays a critical role in synthesis as well.
Therefore, effective resolution of the bottleneck for synthesis requires the
conversion to be time and memory performant, and prevent state-space explosion.
Current conversion approaches, however, which are based either on
explicit-state representation or symbolic-state representation, fail to address
these necessities adequately at scale: Explicit-state approaches generate
minimal DFA but are slow due to expensive DFA minimization. Symbolic-state
representations can be succinct, but due to the lack of DFA minimization they
generate such large state spaces that even their symbolic representations
cannot compensate for the blow-up.
This work proposes a hybrid representation approach for the conversion. Our
approach utilizes both explicit and symbolic representations of the
state-space, and effectively leverages their complementary strengths. In doing
so, we offer an LTLf to DFA conversion technique that addresses all three
necessities, hence resolving the bottleneck. A comprehensive empirical
evaluation on conversion and synthesis benchmarks supports the merits of our
hybrid approach.

本文提出了一种混合表示方法，利用显式和符号表示状态空间，并有效地利用它们的互补优势，从而提供了一种解决 LTLf 到 DFA 转换过程中三个必要条件的技术，从而解决合成中的瓶颈问题。

有限时间范围下基于混合组合推理的反应合成

Hybrid Compositional Reasoning for Reactive Synthesis from  Finite-Horizon Specifications

LTLf synthesis is the process of finding a strategy that satisfies a linear
temporal specification over finite traces. An existing solution to this problem
relies on a reduction to a DFA game. In this paper, we propose a symbolic
framework for LTLf synthesis based on this technique, by performing the
computation over a representation of the DFA as a boolean formula rather than
as an explicit graph. This approach enables strategy generation by utilizing
the mechanism of boolean synthesis. We implement this symbolic synthesis method
in a tool called Syft, and demonstrate by experiments on scalable benchmarks
that the symbolic approach scales better than the explicit one.

本文提出了一种基于符号技术的 LTLf 综合的框架，利用布尔合成的机制实现了策略生成，并在可扩展的基准测试中通过实验证明了符号方法比显式方法更具可扩展性。