Computing (bi)simulation relations preserving CTL*x. for ordinary and fair Kripke structures.

Abstract

The main goal of model checking is to verify whether a model of a given program satisfies some given specification. In this paper models are regarded as fair or ordinary Kripke structures whereas specifications are represented by formulae branching-time temporal logics (CTL*x or ACTL*x). Model checking can be substantially enhanced by reducing the size of models under consideration. Usually this is achieved by using binary relations on the set of Kripke structures that preserve the satisfiability of temporal formulae. It is known that stuttering bisimulation (simulation) relation preserves CTL*x (respectively ACTL*x) for ordinary Kripke structures. In this paper we present a fair game stuttering bisimulation(simulation) relation which preserves CTL*x (ACTL*x) for fair Kripke structures, and algorithms for computing stuttering (bi)simulation which utilize usual and parity games. If n is the number of states and m the number of transitions in a finite states transition system then our algorithms for computing stuttering simulation and bisimulation for ordinary Kripke structures is proved to have O(m^2) time and space complexity, and our algorithms for computing the same relations for fair Kripke structures appear to have O(m^2n^2) time and O(m^2) space complexity. Thus the verification of CTL*x-formulae on a model M (ordinary or fair) can be reduced to the verification of these formulae on a smaller model.