Supervisory Synthesis Of DEDS Based On Temporal Petri Nets

Modeling and controlling of the Discrete Event Dynamic Systems (DEDS) on the logic level are very significant aspects in the research of DEDS. Much attention of Petri Nets have been played to the research field of DEDS controlling theory, because of Petri Nets' many features, for instance, concurrent semantics, hardware implementation of logic circuit form.Nowadays, most of research are to build a transmutative Petri Nets (called Controlled Petri Nets) through adding controlling place sets, controlling arc sets and controlling policy to the basic Petri Nets, while the Controlled Petri Nets could be used to argue many controlling theory problems conveniently and to induce many logically and physically supervisory and solve the Event Feedback Controlling Problems (EFCP) and State Feedback Controlling Problem (SFCP) in DEDS supervisory theory.Sum of all, we have found some shortages of many researches as followed: First of all, most of Controlled Petri Nets method would lead into a logically supervisory because of the characteristic of Controlled Petri Nets and could only be used in a limited area. Secondly, most of the controlling specifications adopted natural language and inequality of place capacity, which are always applied to the place or token, and not the transitions. So, the low level of system reconstruction would be resulted from. Moreover, some reconstructive systems are some Petri Nets added new special arc and have changed the Extension Rule(ER) of Net Theory and this kind of reconstruction became meaningless.Meanwhile, some features of Linear Temporal Logic have been founded as follows: it could describe the static specification of stimulated object and show dynamic semantics of described object naturally.In the issue, Linear Temporal Logic Formula (LTLF) plays a very important role in the description language of the controlling specification of the DEDS supervisory synthesis based Petri Nets. We will show the process during which a source model created with basic Temporal Petri Nets will be changed into a model described by basic Petri Nets, while the latter have the same transition sets and behavior language and furthest similitude with the former through mending the extending reachability marking graph of bounded Petri Nets with the semantics of LTLF and through the transforming algorithm from Transition Systems to Petri Nets.