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.

翻译：\ emph{ 核查} 和 emph{ 真实性 的问题是分析反应系统的两个中心主题。 当考虑多试剂系统时,这些问题自然具有纯战略Nash 平衡(非空性)的存在(非空性)和纯战略Nash 平衡(纯战略Nash 平衡)的核查的相似性。 最近, 这项工作已开始包括限定和顺方时间目标。 在有限和顺方时间目标方面, 存在目标代表的自然等级, 从确定性的有限自动自动数据(DFA)到非确定性的有限自动数据(NFA), 以及交替有限的自动数据(AFA), 每一次代表之间都存在最差的指数差距。 以前的工作表明,DFA目标的可真实性问题已经完成, 而时间逻辑目标的可容性问题在2 EXPTIME。 我们研究了各种目标的可容性和核查问题。 我们首先表明,NFA目标的可真实性问题与不精确性(EFA- ) 的复杂性是真实性, 与我们无法核查目标之间, 。