The Automata Model of Interval Speed CPNs

Abstract:

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.

• Periodical: Applied Mechanics and Materials (Volumes 548-549)
• Pages: 1241-1248
• DOI: https://doi.org/10.4028/www.scientific.net/AMM.548-549.1241
• Online since: April 2014
• Authors: Wei Zhi Liao*
• Keywords: Instantaneous Firing Speed, Interval Speed CPNs, Timed Automata

References

[1] R. David, H. Alla. Continuous Petri Nets, in Proceedings of the 8th Europeab Workshop on Application and Theory of Petri Nets(Saragossa, Spain), (1987), pp.275-294.

DOI: 10.1007/978-3-642-10669-9_6

[2] David, H. Alla. On Hybrid Petri Nets. Discrete Events Dynamic Systems, in Theory and Application，Vol. 11 No. 1(2001), pp.9-40.

[3] J. LE Ball, H. Alla, R. David. Asymptotic Continuous Petri Nets. Discrete Event Dynamic Systems, in Theory and Applications. Vol. (2)(1993), pp.235-263.

DOI: 10.1007/bf01797160

[4] F. Balduzzi, A. Giua and G. Menga. First-Order Hybrid Petri Nets: a Model for Optimitation and Control, In IEEE Transactions On Robotics And Automation. Vol. 16 No. 14(2000), pp.382-399.

DOI: 10.1109/70.864231

[5] T. Gu, and P.A. Bahri. A Survey of Petri Net Applications in Batch Processes, in Computer in Industry, Vol. 47 No. 1 (2002), 99-111.

DOI: 10.1016/s0166-3615(01)00142-7

[6] T. Gu, and P.A. Bahri. Development of Hybrid Petri Net for Scheduling of Mixed Batch/Continuous Process., in Proceedings of the 15th IFAC World Congress on Automatic Control(2002).

[7] Tianlong Gu, Rongsheng Dong. Novel Continuous Model to Approximate Time Petri Nets: Modeling And Analysis, in Journal of Application Mathematic and Computer Science, Vol. 15 No. 1 (2005) , pp.141-150.

[8] L.A. Cortes, P. Eles. Verification of Embedded Systems using a Petri Net based Representation, in 13th International Symposium on Systems Synthesis(ISSS'2000), (2000), pp.149-155.

DOI: 10.1109/isss.2000.874042

[9] D. Lime, O.H. Roux. State Class Timed Automaton of a Timed Petri Nets, in PNPM'03. IEEE Computer Society(2003).

DOI: 10.1109/pnpm.2003.1231549

[10] F. Cassez, O.H. Roux. Structral Translation From Time Petri Nets to Tined Automata, in Journal of Software and Systems, Vol. 79 No. 10 (2005), pp.1456-1468.

DOI: 10.1016/j.jss.2005.12.021

[11] Information on http: /www. ibisc. uni-evry. fr/Vie/TR.

[12] LIAO Weizhi, GU Tianlong. Novel Analysis Method for Reachability of Hybrid Petri Nets, in Journal of Chinese Computer Systems , Vol. 30 No. 8 (2009), pp.1651-1655.

[13] Liao Wei-Zhi, Gu Tian-Long. Effective Conflict of Interval Speed Continuous Petri Net, in. Computer science(in Chinses), Vol. 33 No. 10 (2006), pp.221-224.

[14] R. Alur, L. Fix and Henzinger T. Event-clock Automata: A Determinizable Class of Timed Automata, in Theoretical Computer Science, Vol. 211 No. 1-2 (1999), pp.253-273.

DOI: 10.1016/s0304-3975(97)00173-4