A Hierarchy of Polynomial-Time Computable Simulations for Automata

We define and provide algorithms for computing a natural hierarchy of simulation relations on the state-spaces of ordinary transition systems, finite automata, and Büchi automata. These simulations enrich ordinary simulation and can be used to obtain greater reduction in the size of automata by computing the automaton quotient with respect to their underlying equivalence. State reduction for Büchi automata is useful for making explicit-state model checking run faster ([EH00], [SB00], [EWS01]).

We define k-simulations, where 1-simulation corresponds to ordinary simulation and its variants for Büchi automata ([HKR97], [EWS01]), and k- simulations, for k > 1, generalize the game definition of 1-simulation by allowing the Duplicator to use k pebbles instead of 1 (to “hedge its bets”) in response to the Spoiler’s move of a single pebble. As k increases, k- simulations are monotonically non-decreasing relations. Indeed, when k reaches n, the number of states of the automaton, the n-simulations defined for finite-automata and for labeled transition systems correspond precisely to language containment and trace containment, respectively. But for each fixed k, the maximal k-simulation relation is computable in polynomial time: nO(k).

This provides a mechanism with which to trade off increased computing time for larger simulation relation size, and more potential reduction in automaton size. We provide algorithms for computing k-simulations using a natural generalization of a prior efficient algorithm based on parity games ([EWS01]) for computing various simulations.Last ly, we observe the relationship between k-simulations and a k-variable interpretation of modal logic.