Verification and Realizability in Finite-Horizon Multiagent Systems

TL;DR

This paper analyzes the computational complexity of verification and realizability problems in finite-horizon multiagent systems with various goal representations, revealing complexity gaps between different automata types.

Contribution

It establishes the exact complexity classes for realizability with NFA and AFA goals and compares them to verification complexities, highlighting the computational differences.

Findings

Realizability with NFA goals is EXPTIME-complete.

Realizability with AFA goals is 2EXPTIME-complete.

Verification with DFA, NFA, and AFA goals is PSPACE-complete.

Abstract

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.