Abstract by Michel Reniers:
We propose a method to show how model checking may be used to verify that a synthesized supervisor indeed is safe (w.r.t. safety requirements used in the synthesis procedure), nonblocking and controllable. To achieve this we propose a method for transforming networks of extended finite automata that interact through shared events, in the form of a CIF model, into an mCRL2 specification.
The approach is illustrated using a case dealing with the coordination of maintenance procedures for a high-end printer.