A Symbolic Model Checker for ACTL*

A b s t r a c t. We present SAM, a symbolic model checker for ACTL, the action-based version of CTL. SAM relies on implicit representations of Labeled Transition Systems (LTSs), the semantic domain for ACTL for-mulae, and uses symbolic manipulation cilgorithms. SAM has been re-alized by translating (networks of) LTSs and, possibly recursive, ACTL formulae into BSP (Boolean Symbolic Programming), a programming language aiming at defining computations on booleein functions, and by using the BSP interpreter to ccirry out computations (i.e. verifications).