Modular control of discrete-event systems with coalgebra

Modular supervisory control of discrete-event systems, where the overall system is a synchronous (parallel) product of subsystems, is considered. The main results of this paper are formulations of sufficient conditions for the compatibility between the synchronous product and various operations stemming from supervisory control as supervised product and supremal controllable sublanguages. These results are generalized to the case of modules with partial observations: e.g., modular computation of supremal normal sublanguages is studied. Coalgebraic techniques based on the coinduction proof principle are used in our main results. Sufficient conditions are derived for modular to equal global control synthesis. An algorithmic procedure for checking the new conditions is proposed and the computational benefit of the modular approach is discussed and illustrated by comparing the time complexity of modular and monolithic computation.