International Workshop on:
Current Trends in Applied Formal Methods, 
Boppard, Germany, 7-9 October 1998,
Lecture Notes in Computer Science, 
Springer-Verlag


Title:
A Symbolic Model Checker for ACTL

Authors:
A. Fantechi (Univ. di Firenze and IEI CNR Pisa),
S. Gnesi (IEI CNR Pisa),
F. Mazzanti (IEI CNR Pisa),
R. Pugliese (Univ. di Firenze),
E. Tronci (Univ. di L'aquila),



Abstract


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 uses 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).