The Complexity of Simulation and Matrix Multiplication

TL;DR

This paper establishes the computational complexity of simulation preorder problems in model checking, linking their difficulty to matrix multiplication, and provides new algorithms and lower bounds for both cyclic and acyclic structures.

Contribution

It presents the first conditional lower bounds for simulation games, relates their complexity to matrix multiplication, and offers the first subcubic algorithm for acyclic cases.

Findings

Improving simulation game algorithms may require breakthroughs in matrix multiplication.

A subcubic algorithm for acyclic simulation games is developed based on fast matrix multiplication.

Certificates for simulation problems can be verified in subcubic time, with different methods for cyclic and acyclic cases.

Abstract

Computing the simulation preorder of a given Kripke structure (i.e., a directed graph with $n$ labeled vertices) has crucial applications in model checking of temporal logic. It amounts to solving a specific two-players reachability game, called simulation game. We offer the first conditional lower bounds for this problem, and we relate its complexity (for computation, verification, and certification) to some variants of $n\times n$ matrix multiplication. We show that any $O(n^{\alpha})$-time algorithm for simulation games, even restricting to acyclic games/structures, can be used to compute $n\times n$ boolean matrix multiplication (BMM) in $O(n^{\alpha})$ time. This is the first evidence that improving the existing $O(n^{3})$-time solutions may be difficult, without resorting to fast matrix multiplication. In the acyclic case, we match this lower bound presenting the first subcubic algorithm, based on fast BMM, and running in $n^{\omega+o(1)}$ time (where $\omega<2.376$ is the exponent of matrix multiplication). For both acyclic and cyclic structures, we point out the existence of natural and canonical $O(n^{2})$-size certificates, that can be verified in truly subcubic time. In the acyclic case, $O(n^{2})$ time is sufficient, employing standard matrix product verification. In the cyclic case, a $\max$-semi-boolean matrix multiplication (MSBMM) is used, i.e., a matrix multiplication on the semi-ring $(\max,\times)$ where one matrix contains only $0$'s and $1$'s. This MSBMM is computable (hence verifiable) in truly subcubic $n^{(3+\omega)/2+o(1)}$ time by reduction to $(\max,\min)$-multiplication. Finally, we show a reduction from MSBMM to cyclic simulation games which implies a separation between the cyclic and the acyclic cases, unless MSBMM can be verified in $n^{\omega+o(1)}$ time.