Efficient enforcement of state invariant requirements in databased synthesis

In the following paper it is shown how to perform databased synthesis more efficiently when there are (many) state invariants present in the specification: "Efficiently enforcing mutual state exclusion requirements in symbolic supervisor synthesis", 2021, Sander Thuijsman, Michel Reniers, Dennis Hendriks (link). Instead of encoding all state invariant requirements in the nonblocking predicate that is continuously updated throughout synthesis, the state invariant requirements are encoded as much as possible in the guards of the edges directly. Implementing the suggested algorithm could greatly reduce required time/memory to perform databased synthesis for models that contain many state invariant requirements.