Selective Mu-Calculus and Formula-Based Equivalence of Transition Systems

摘要

In model checking for temporal logic, the correctness of a system with respect to a desired behavior is verified by checking whether a structure that models the system satisfies a formula describing the behavior. Most existing verification techniques are based on a representation of the system by means of a labeled transition system. In this approach to verification, the efficiency of the model checking is essentially influenced by the number of states of the transition system. In this paper we present a new temporal logic, the selective mu-calculus, and an equivalence between transition systems based on the formulae of this logic. This property preserving equivalence can be used to reduce the size of transition systems. The equivalence (called ρ-equivalence) is based on the set, ρ, of actions occurring inside the modal operators of a selective mu-calculus formula. We prove that the ρ-equivalence coincides with the equivalence induced by the set of the selective mu-calculus formulae with occurring actions in ρ. Thus, a formula can be more efficiently checked on a transition system ρ-equivalent to the standard one, but smaller than it, since all the actions not in ρ are “discarded.”