In this paper, we study opacity-enforcing supervisory control of discrete event systems. We consider the case that the secrete behavior of the system is specified by multiple secret languages, and synthesize a maximally permissive supervisor that enforces opacity for all secret languages. We prove that, under a certain assumption on observable and uncontrollable events, a maximally permissive opacity-enforcing supervisor can be synthesized in a modular fashion.

This paper develops a modular synthesis algorithm for timed circuits that is dramatically accelerated by partial order reduction. This algorithm synthesizes each module in a hierarchical design individually. It utilizes partial order reduction to reduce the state space explored for the other modules by considering a single interleaving of concurrently enabled transitions. This approach better manages the state explosion problem resulting in a more than 2 order of magnitude reduction in synthesis time. The improved synthesis time enables the synthesis of a larger class of timed circuits than was previously possible.