Study on real-time discrete event systems by using controlled temporal timed-Petri-nets

In this paper, the framework of hybrid model of controlled timed Petri nets (CTPN) with propositional temporal logic (PTL) is studied for modelling and analyzing real-time discrete event dynamic systems (DEDS). The properties of system and its expectation specification are described by proposition temporal logic. Controller of discrete event dynamic systems is designed according to the specification of PTL formulas. An illustrative example of biochemistry process is given to show the design procedures of controller driven the evolution of DEDS according to the expected behavior.