Reactive Synthesis Swen Jacobs, Martin Zimmermann


APPLY Algorithm

Written: 08.11.2017 16:33 Written By: Swen Jacobs

It was pointed out to me that the APPLY algorithm, as presented in the lecture, did not properly reflect the fact that the current root nodes of the two BDDs could be labeled with different variables. In that case, the recursion only considers the successor nodes in the BDD that is rooted in the maximal variable (and re-uses the current root node for the other BDD). I have already fixed this in the slides, thanks for pointing it out!

Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators