The Automata Model of Interval Speed CPNs

Continuous Petri Nets(CPNs) has been a useful tool not only to approximate a discrete system but also to model a continuous process. In this paper, we consider a general CPNs----Interval speed CPNs(ICPNs). An approach to translate Interval speed CPNs to event clock automata is proposed. Since the instantaneous firing speed (IFS) vector is one of key parameters in behavior analysis for ICPN, an efficient way to determine the IFS of ICPNs was presented firstly. Then an algorithm of constructing evolution graph for ICPNs was developed, which offers all information for constructing automata for ICPNs. Furthermore, a procedure to transform a state evolution graph of ICPNs into an event clock automata is build. After having constructed the associated event clock automaton, we show that classical approaches of verification of event clock logic formulas can be applied to prove that the ICPNs model satisfies a particular property.