[SAL] sal-smc, theory behind

Peter Bokor petbokor at mit.bme.hu
Sun Apr 13 10:51:12 PDT 2008

Hi everybody,


Does anybody know which model checking algorithm is implemented by sal-smc? 


I know it’s a BDD-based method, and the fact that it’s an LTL model checker
refers to some tableau-based technique with fixpoint calculation. However,
there is a translation of the input LTL formula into a Büchi automaton. Does
the analysis check language containment as well?





-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.csl.sri.com/pipermail/sal/attachments/20080413/be03f395/attachment.html

More information about the SAL mailing list