The polynomial time decidability of simulation relations for finite state processes: A HORNSAT based approach
Sandeep K. Shukla, Daniel J. Rosenkrantz, Harry T. Hunt, Richard Edwin Stearns · DIMACS series in discrete mathematics and theoretical computer science · 1997
We present a uniform approach for proving the polynomial time decidability of various simulation and equivalence relations for finite state processes. Our approach involves efficient reductions to the satisfiability problem for Horn formulas. It applies directly and naturally to most of the simulation preorders and equivalence relations, studied in the literature. Here we illustrate our methodology by deriving efficient algorithms for a number of such relations. For some of these relations, we present polynomial time algorithms for the first time in the literature. We also present a HORNSAT based interpretation of the existing bottom-up algorithm for bisimulation equivalence [KS90] to provide a better understanding of such bottom-up partition based methods [KS90, PT87]. Corollaries of our results include an NC algorithm for bisimulation equivalence for deterministic transition system (posed as an open problem in [GHR95]), an easy algorithm for computing simulations on finite graphs [...