The Polynomial Time Decidability of Simulation Relations for Finite State Processes: A HORNSAT Based Approach

. We present a uniform approach for proving the polynomialtime decidability of various simulation and equivalence relations for finitestate processes. Our approach involves efficient reductions to thesatisfiability problem for Horn formulas. It applies directly and naturallyto most of the simulation preorders and equivalence relations,studied in the literature. Here we illustrate our methodology by derivingefficient algorithms for a number of such relations. For some ofthese relations,...