Abstract: Computing the simulation preorder of a given Kripke structure (i.e., a directed graph with 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 matrix multiplication. We show that any -time algorithm for simulation games, even restricting to acyclic games/structures, can be used to compute boolean matrix multiplication (BMM) in time. This is the first evidence that improving the existing -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 time (where is the exponent of matrix multiplication). For both acyclic and cyclic structures, we point out the existence of natural and canonical -size certificates, that can be verified in truly subcubic time. In the acyclic case, time is sufficient, employing standard matrix product verification. In the cyclic case, a -semi-boolean matrix multiplication (MSBMM) is used, i.e., a matrix multiplication on the semi-ring where one matrix contains only 's and 's. This MSBMM is computable (hence verifiable) in truly subcubic time by reduction to -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 time.
