by Dennis Dams, Rob Gerth, Gert Döhmen, Ronald Herrmann, Peter Kelb, and Hergen Pargmann.
In David L. Dill, editor, Computer-Aided Verification, number 818 in Lecture Notes in Computer Science. Springer-Verlag, 1994.
We present a partitioning algorithm for checking ACTL specifications that distinguishes between states only if this is necessary to ascertain the specification. This algorithm is then generalized to also abstract from the variable values in the states. Here, too, the values between which the algorithm distinguishes are determined by what is needed to decide whether or not the specification holds. The resulting algorithm is being implemented in an ROBDD based model checker for VHDL/S.
Keywords: model checking, ACTL, abstract interpretation, state partitioning, binary decision diagrams (BDDs)