Supervisory Coordination of Timed Communicating Processes

We propose a synthesis-centric approach to coordination of timed discrete-event systems with data and unrestricted nondeterminism. We employ supervisory controllers to exercise the desired coordination, which are automatically synthesized based on the models of the system components and the coordination rules. We develop a timed process theory with data that supports the modeling process and we provide for time abstractions that allow us to employ standard synthesis tools. Following the synthesis of the discrete-event controller that preserves safe behavior of the supervised system, we analyze the timed behavior by employing timed model checking. To interface the synthesis tool and the model checker, we develop a compositional model transformation.