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).
Cite
CITATION STYLE
Fantechi, A., Gnesi, S., Mazzanti, F., Pugliese, R., & Tronci, E. (1999). A symbolic model checker for ACTL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1641, pp. 228–242). Springer Verlag. https://doi.org/10.1007/3-540-48257-1_14
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
