Synthesis with rational environments
Synthesis with rational environments
复制标题
DOI：
10.1007/s10472-016-9508-8
复制
发表时间：
2016-09-01
影响因子：
1.2
通讯作者：
Vardi, Moshe Y.
中科院分区：
文献类型：
--
作者：
Kupferman, Orna;Perelli, Giuseppe;Vardi, Moshe Y.
综合是根据系统规范自动构建系统。系统必须在所有可能的环境中满足其规范。环境通常由有自己目标的代理人组成。因此，软化对环境行为的普遍量化并考虑其潜在代理人的目标是有意义的。Fisman等人介绍了理性综合：理性主体背景下的综合问题。问题的输入包括指定系统目标和构成环境的代理的时间逻辑公式，以及解决方案概念（例如，Nash equilibrium）。输出是一个配置文件的战略，为系统和代理，使系统的目标是满足计算的结果的战略，和配置文件是稳定的，根据解决方案的概念;也就是说，代理，构成环境没有动机偏离的战略建议给他们。在本文中，我们继续研究理性综合。首先，我们提出了一个替代的定义，合理的合成，其中的代理人是理性的，但不合作。我们称这样的问题为强理性综合。在强理性综合的背景下，我们不能假设构成环境的主体会考虑向它们建议的策略。因此，输出仅是用于系统的策略，并且系统的目标必须在作为系统遵循该策略的稳定简档的结果的所有组合中得到满足。我们证明了强有理综合是2 EXPTIME-COMPLEX，因此它并不比传统综合或有理综合复杂。其次，我们研究了一个更丰富的规范形式主义，系统和代理的目标不是布尔的，而是定量的。在这种情况下，系统和代理人的目标是最大化他们的结果。定量设置大大扩展了理性综合的范围，使博弈论方法更具相关性。最后，我们丰富的设置，允许联盟的代理，构成系统或环境。
Synthesis is the automated construction of a system from its specification. The system has to satisfy its specification in all possible environments. The environment often consists of agents that have objectives of their own. Thus, it makes sense to soften the universal quantification on the behavior of the environment and take the objectives of its underlying agents into an account. Fisman et al. introduced rational synthesis: the problem of synthesis in the context of rational agents. The input to the problem consists of temporal logic formulas specifying the objectives of the system and the agents that constitute the environment, and a solution concept (e.g., Nash equilibrium). The output is a profile of strategies, for the system and the agents, such that the objective of the system is satisfied in the computation that is the outcome of the strategies, and the profile is stable according to the solution concept; that is, the agents that constitute the environment have no incentive to deviate from the strategies suggested to them. In this paper we continue to study rational synthesis. First, we suggest an alternative definition to rational synthesis, in which the agents are rational but not cooperative. We call such problem strong rational synthesis. In the strong rational synthesis setting, one cannot assume that the agents that constitute the environment take into account the strategies suggested to them. Accordingly, the output is a strategy for the system only, and the objective of the system has to be satisfied in all the compositions that are the outcome of a stable profile in which the system follows this strategy. We show that strong rational synthesis is 2EXPTIME-COMPLETE, thus it is not more complex than traditional synthesis or rational synthesis. Second, we study a richer specification formalism, where the objectives of the system and the agents are not Boolean but quantitative. In this setting, the objective of the system and the agents is to maximize their outcome. The quantitative setting significantly extends the scope of rational synthesis, making the game-theoretic approach much more relevant. Finally, we enrich the setting to one that allows coalitions of agents that constitute the system or the environment.