The complexity of simulation and matrix multiplication

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 × n matrix multiplication. We show that any O(nα)-time algorithm for simulation games, even restricting to acyclic games/structures, can be used to compute n×n boolean matrix multiplication (BMM) in O(nα) time. In the acyclic case, we match this bound by presenting the first subcubic algorithm, based on fast BMM, and running in n!+o(1) time (where ! < 2:376 is the exponent of matrix multiplication). For both acyclic and cyclic structures, we point out the existence of natural and canonical O(n2)-size certificates, that can be verified in truly subcubic time by means of matrix multiplication. In the acyclic case, O(n2) time is sufficient, employing standard (+;×)-matrix product verification. In the cyclic case, a min-edge witness matrix multiplication (EWMM) is used, i.e., a matrix multiplication on the semi-ring (max;×) where one matrix contains only 0's and 1's, which is computable in truly subcubic n(3+ω)=2+o(1) time. Finally, we show a reduction from EWMM to cyclic simulation games which implies a separation between the cyclic and the acyclic cases, unless EWMM can be verified innω+o(1) time.