摘要：AbstractTimed Petri nets and max-plus automata are well known modelling frameworks for timed discrete-event systems. In this paper we present an iterative procedure that constructs a max-plus automaton from a timed Petri net while retaining the timed behaviour. Regarding the Petri net, we essentially impose three assumptions. First, the reachability graph must be finite; i.e., the Petri net must be bounded. Second, the Petri net operates according to the so called race policy. And third, we interpret the Petri net with single server semantics. Under these assumptions we show that the proposed procedure terminates with a finite deterministic max-plus automaton that realises the same timed behaviour as the Petri net. We demonstrate by example how our procedure can be applied in the context of supervisor controller design for timed discrete-event systems.
关键词：KeywordsPetri netsmax-plus automatatimed discrete-event systemssupervisory control
