zbMATH — the first resource for mathematics

Interval timed coloured Petri net: efficient construction of its state class space preserving linear properties. (English) Zbl 1141.68045
Summary: We consider here the interval timed coloured Petri net model. This model associates with each created token a time interval specifying when the token will become available and forces enabled transitions to occur as soon as possible. This model can simulate other timed Petri nets and allows to describe large and complex real-time systems. We propose a much more efficient contraction for its generally infinite state space than those developed in the literature. Our contraction approach captures all linear properties of the model and produces finite graphs for all bounded models.
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
HyTech; Kronos; SENAC; Uppaal
Full Text: DOI
[1] Alur R, Dill D (1990) Automata for modeling real-time systems 17me ICALP, LNCS 443. Springer, Heidelberg, pp 322–335 · Zbl 0765.68150
[2] Alur R, Courcoubetis C, Dill D (1993) Model checking in dense real-time. Inf Comput 104(1):2–34 · Zbl 0783.68076 · doi:10.1006/inco.1993.1024
[3] Bengtsson J (2002) Clocks, DBMs and states in timed systems. PhD thesis, Department of Information Technology, Uppsala University
[4] Behrmann G, Bengtsson J, David A, Larsen KG, Pettersson P, Yi W (2002) UPPAAL implementation secrets. In: 7th international symposium on formal techniques in real-time and fault-tolerant systems, LNCS 2469. Springer, Heidelberg, pp 3–22
[5] Berthomieu B, Diaz M (1991) Modeling and verification of time dependent systems using time Petri nets. IEEE Trans Softw Eng 17(33):259–273, 275–290
[6] Boucheneb H, Berthelot G (2002) Contraction of the ITCPN state space. Theor Comput Sci 65(6):1–15 · Zbl 1270.68163
[7] Berthelot G, Boucheneb H (1994) Occurrence graphs for interval timed coloured nets. In: 15th international conference on application and theory of Petri nets, Zaragoza (Spain), LNCS 815. Springer, Heidelberg
[8] Christensen S, Kritensen LM, Mailand T (2001) Condensed state spaces for timed Petri nets. In: 22nd international conference on application and theory of Petri nets and 2nd international conference on application of concurrency to system design, Newcastle Upon Tyne
[9] Daws C, Olivero A, Tripakis S, Yovine S (1996) The tool Kronos. Hybrid Systems III, Verification and Control, LNCS 1066. Springer, Heidelberg
[10] Diaz M, Senac P (1994) Time stream Petri nets a model for timed multimedia information. In: 15th international conference on application and theory of Petri nets, LNCS 815. Springer, Zaragoza (Spain)
[11] Henzinger TA, Ho PH, Wong-Toi H (1997) HyTech: a model checker for hybrid systems. Softw Tools Technol Transf 1:110–122 · Zbl 1060.68603 · doi:10.1007/s100090050008
[12] Hsiung PA, Gau CH (2002) Formal synthesis of real-time embedded software by time-memory scheduling of colored time Petri nets. Theor Comput Sci 65(6):140–153 · Zbl 1270.68052
[13] Jensen K (1982) Coloured Petri nets: basic concepts, analysis methods and practical use, vols 1 and 2, EATCS Monographs on Theoretical Computer Science. Springer, Heidelberg
[14] Merlin P, Farber DJ (1976) Recoverability of communication protocols. IEEE Trans Commun 24: 1036–1042 · Zbl 0362.68096 · doi:10.1109/TCOM.1976.1093424
[15] Sifakis J (1977) In: Beilner H, Gelenbe E (eds) Use of Petri nets for performance evaluation, measuring, modeling and evaluating computer systems. North-Holland, Amsterdam
[16] Thanh CB, Klaudel H, Pommereau F (2002) Petri nets with causal time for system verification. In: 3rd international workshop on models for time-critical systems
[17] Van der Aalst WMP (1993) Interval timed coloured Petri nets and their analysis. In: 14th international conference of application and theory of Petri nets, Chicago
[18] Vicaro E (2001) Static analysis and dynamic steering of time-dependent systems. IEEE Trans Softw Eng 2(8):728–748 · Zbl 05114174 · doi:10.1109/32.940727
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.