Reactive synthesis automatically derives a strategy that satisfies a given specification. However, requiring a strategy to meet the specification in every situation is, in many cases, too hard of a requirement. Particularly in compositional synthesis of distributed systems, individual winning strategies for the processes often do not exist. Remorsefree dominance, a weaker notion than winning, accounts for such situations: dominant strategies are only required to be as good as any alternative strategy, i.e., they are allowed to violate the specification if no other strategy would have satisfied it in the same situation. The composition of dominant strategies is only guaranteed to be dominant for safety properties, though; preventing the use of dominance in compositional synthesis for liveness specifications. Yet, safety properties are often not expressive enough. In this paper, we thus introduce a new winning condition for strategies, called delay-dominance, that overcomes this weakness of remorsefree~dominance: we show that it is compositional for many safety and liveness specifications, enabling a compositional synthesis algorithm based on delay-dominance for general specifications. Furthermore, we introduce an automaton construction for recognizing delay-dominant strategies and prove its soundness and completeness. The resulting automaton is of single-exponential size in the squared length of the specification and can immediately be used for safraless synthesis procedures. Thus, synthesis of delay-dominant strategies is, as synthesis of winning strategies, in 2EXPTIME.

翻译：反应式合成能够自动推导出满足给定规约的策略。然而，要求策略在所有情况下都满足规约，在许多场合下过于严苛。尤其是在分布式系统的组合合成中，各个进程往往不存在独立的获胜策略。无悔主导性（一种比获胜更弱的概念）恰能应对此类情况：主导策略仅需与任何替代策略同样出色，即允许其违反规约——若在同一情境下其他策略也无法满足该规约。不过，仅针对安全性质可保证主导策略组合的优越性，这阻碍了将主导性用于活性规约的组合合成。然而，安全性质通常表达力不足。为此，本文提出一种新的策略获胜条件——延迟主导性，以克服无悔主导性的这一缺陷：我们证明该条件对多种安全与活性规约具有组合性，从而为一般规约设计出基于延迟主导性的组合合成算法。进一步地，我们提出用于识别延迟主导策略的自动机构造，并证明其可靠性与完备性。该自动机规模为规约长度平方的单指数级，可直接用于无安全约束合成过程。因此，延迟主导策略的合成与获胜策略合成同属2EXPTIME复杂度类。