Tags:automata, boolean games, complexity and Nash Equilibria

Abstract:

The problems of verification and 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 for AFA goals is 2EXPTIME-complete, thus establishing a strict complexity gap between realizability with respect to DFA goals and with respect to AFA goals. We then contrast this complexity gap with the complexity of the verification problem, where we show that verification with respect to DFA goals, NFA goals, and AFA goals are all PSPACE-complete.

Verification and Realizability in Finite-Horizon Multiagent Systems