综合活性主导策略（完整版）

响应式合成（Reactive synthesis）自动推导满足给定规约的策略。然而，要求策略在每种情形下均满足规约，在许多情况下过于严苛。尤其在分布式系统的组合式合成中，各进程的个体获胜策略往往并不存在。无悔主导性（remorsefree dominance）作为弱于获胜性的概念，可应对此类情形：主导策略仅需不劣于任何替代策略，即若在同一情形下无其他策略能满足规约，则允许其违反规约。但主导策略的组合仅对安全性质保证为主导；这阻碍了主导性在活性规约组合式合成中的使用。然而安全性质常表达力不足。本文因此引入一种称为延迟主导性（delay-dominance）的策略新获胜条件，克服了无悔主导性的上述弱点：我们证明其对于诸多安全与活性规约具组合性，从而支持基于延迟主导性、面向一般规约的组合式合成算法。此外，我们给出识别延迟主导策略的自动机构造并证明其可靠性与完备性。所得自动机在规约长度平方上呈单指数规模，并可立即用于无 Safra 合成流程。因此，延迟主导策略的合成与获胜策略合成同处 2EXPTIME。