In Costas Courcoubetis, editor, Computer-Aided Verification, number 697 in Lecture Notes in Computer Science, pages 479-490. Springer-Verlag, 1993.
In the first part of the paper, we present an algorithm for the construction of a quotient model under the equivalence induced by ACTL, the universal fragment of CTL. As this equivalence coincides with simulation equivalence, the achieved reduction is better than reductions achieved by methods based on bisimulation. Simulation equivalence is also the equivalence that is induced by ACTL*, hence, the reduced model allows model checking of any ACTL* formula. Furthermore it provides diagnostic information. In the second part, we restict our attention to single ACTL* formulae. An algorithm is given that constructs a model which is reduced w.r.t. a specific formula.
The reduced models are constructed directly, without intermediate need for the full models. The approach, splitting of states w.r.t. formulae, yields a sequence of successively more refined models which at any stage preserve truth of formulae.