Is multicore supervisory controller synthesis in the Ramadge-Wonham framework feasible?

Supervisory control theory studies automated generation of provably-correct discrete-event control software based on formal models of the system and the control requirements. There are many computational challenges in the synthesis of software models, where parallel controller synthesis seems to be one of the few plausible alternatives in the future. Surprisingly, no parallel synthesis algorithms for the Ramadge-Wonham framework are readily available, despite the emergence of affordable multi-core machines. We propose a multi-core implementation of the core supervisor synthesis algorithm, showing almost linear improvement with respect to the number of available cores for a large class of models.