A Symbolic Model Checker for ACTL

. 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 formulae, and makes use of symbolic manipulation algorithms. SAM has been realized by translating (networks of) LTSs and, possibly recursive, ACTL formulae into BSP (Boolean Symbolic Programming), a programming language aiming at defining computations on boolean functions, and by using the BSP interpreter to carry out computations (i.e. verifications) . 1 Introduction The increasing reliance of many aspects of human society on highly complex computer systems requires the adoption of innovative validation techniques. In the validation of software difficulties arise from the discontinuous nature of the software behaviour. This behaviour is based on sequences of discrete transitions, with such a high number of possible evolution paths and failure modes, that exhaustive testing becomes impos..