The Complexity of Simulation and Matrix Multiplication

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(na)-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ω +°(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 in nω+°(1) time. Read More: http://epubs.siam.org/doi/10.1137/1.9781611974782.144