论文标题
有限摩托的多基因系统的验证和可实现性
Verification and Realizability in Finite-Horizon Multiagent Systems
论文作者
论文摘要
\ emph {验证}和\ emph {collizizanity}的问题是反应性系统分析中的两个中心主题。当考虑多基因系统时，这些问题具有纯净纳什均衡的存在（非空性）的天然类似物和纯构成纳什均衡的验证。最近，这项工作已经开始包括有限的摩托车时间目标。有了有限的Horizon时间目标，从确定性有限自动机（DFA）到非确定性有限自动机（NFA），到交替的有限自动机（AFA），具有自然的目标表示层次结构，并且在每个连续的表现之间都有最大的指数间隙。先前的工作表明，DFA目标的可靠性问题是PSPACE完成的，而时间逻辑目标的可变性问题是在2 Extime中。在这项工作中，我们研究了各种目标表示的可靠性和验证问题。我们首先表明，NFA目标的可实现问题是指示时间完成，并且AFA目标是2Exptime-Complete，因此在DFA，NFA和AFA目标方面建立了严格的复杂性差距。然后，我们将这些复杂性差距与验证问题的复杂性进行了对比，在该验证问题的复杂性中，我们证明了关于DFAS，NFA和AFA目标的验证是PSPACE的完整性。
The problems of \emph{verification} and \emph{realizability} are two central themes in the analysis of reactive systems. When multiagent systems are considered, these problems have natural analogues of existence (nonemptiness) of pure-strategy Nash equilibria and verification of pure-strategy Nash equilibria. Recently, this body of work has begun to include finite-horizon temporal goals. With finite-horizon temporal goals, there is a natural hierarchy of goal representation, ranging from deterministic finite automata (DFA), to nondeterministic finite automata (NFA), and to alternating finite automata (AFA), with a worst-case exponential gap between each successive representation. Previous works showed that the realizability problem with DFA goals was PSPACE-complete, while the realizability problem with temporal logic goals is in 2EXPTIME. In this work, we study both the realizability and the verification problems with respect to various goal representations. We first show that the realizability problem with NFA goals is EXPTIME-complete and with AFA goals is 2EXPTIME-complete, thus establishing strict complexity gaps between realizability with respect to DFA, NFA, and AFA goals. We then contrast these complexity gaps with the complexity of the verification problem, where we show that verification with respect to DFAs, NFA, and AFA goals is PSPACE-complete.
