Bounded Model Checking of ACTL Formulae

In this paper, we give a new and improved Bounded Model Checking encoding method for the universal fragment of CTL (ACTL). More specifically, the new encoding method works for verification of ACTL properties, instead of error-hunting. Combine our verification encoding and bug-hunting encoding proposed before, we get a Bounded Model Checking procedure that works for both valid and invalid ACTL properties. The underlying idea and intuition are summarized in this paper and we implement our tool BMV (Bounded Model Verification) on top of the well-known model checker NuSMV 2, and conduct experiments that show the strength and weakness of ACTL Bounded Model Checking compared to traditional BDD-based model checking procedure.