[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?

 

Thanks

 

Peter

-------------- 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