[SAL] sal-smc, theory behind
petbokor at mit.bme.hu
Sun Apr 13 10:51:12 PDT 2008
Does anybody know which model checking algorithm is implemented by sal-smc?
I know its a BDD-based method, and the fact that its 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...
More information about the SAL