Supervisory Control of Timed Discrete Event Systems with Logical and Timed Specifications

A novel framework is introduced for the supervisory control (SC) of timed discrete event systems, based on Time Petri nets. The method encompasses both logical (markings to reach or avoid) and temporal specifications (arrival and departure times in specific markings). It relies on the construction of a partial forward reachability graph, of the Modified State Class Graph type, and the formulation of integer linear programming problems to establish suitable firing time intervals (FTIs) for the controllable transitions. The SC algorithm provides for each enabled controllable transition the largest FTI that guarantees that the specifications are met, irrespectively of the firing times of the uncontrollable transitions.