Supervisory control of time Petri nets using net unfoldings

We define a method for the automatic generation of supervisory controllers that force a software system to perform a given computation by a given deadline. The computation must be executed by a prespecified delay with respect to the previous execution of the computation. Although supervisor generation occurs off-line with respect to software system execution, the resulting controllers automatically take into account variable task durations in an effort to increase the flexibility of computation schedules in the controlled software system.;We model the controlled software system as a time Petri net. Our new unfolding algorithm then produces a so-called Petri net unfolding, in order to analyze explicitly the causal relationships on the execution of transitions in the underlying net. Based on the unfolding, we generate automatically a controlled model which extends the original net by the addition of a supervisory controller. The controlled net is guaranteed to fire a target transition with the given frequency.