Towards Building the State Class Graph of the TSPN Model

• Autorzy: Abdelli A. , Badache N.
• Języki publikacji: EN

Abstrakty

EN

In this paper, we propose an enumerative approach to build the state class graph of the TSPN (Time Stream Petri Net) model. A TSPN model is a Petri net augmented with intervals on arcs and synchronization rules on transitions. It can be used to model complex systems, and it is proved to be more expressive than TPN (Time Petri Nets). In contrast with TPN where each class accessible in the graph is given as a pair (M,D) where M is a marking and D is a system of DBM inequalities, a TSPN class in this form is much complex to compute. To tackle this issue, we introduce a new formalism called the time distance function to define a TSPN class. This function makes it possible to determine an efficient algorithm to compute each class of the graph in a square complexity time. Finally, we show how to exploit the TSPN state class graph (when finite), to check over either linear properties of the model, or to compute minimal and maximal time distances of any firing sequence.

Słowa kluczowe

EN

Time Stream Petri Net; Time Petri Net; State class graph; time distance function; Difference bound Matrix; multimedia

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 86, nr 4
• Strony: 371--409
• Opis fizyczny: bibliogr. 39 poz., tab., wykr.

Twórcy

autor

Abdelli A.

autor

Badache N.

• Bp 32 EI Alia Bab ezzouar Algiers Algieria 16111, Alger,

Bibliografia

• [1] A.Abdelli and M.Daoudi. "Towards a SMIL document analysis using an algebraic time net". 5th Pacific Rim Conf on Multimedia, Tokyo, Japan, Nov-30- PCM 2004: LNCS - Vol 3333/2004 .
• [2] A.Abdelli and N.Badache. "A Semantic Based Pre-fetch Scheme for SMIL presentation proxy-delivery". In proc of 12th IEEE Multimedia Modeling conference, Beigin, China Jan 2006.
• [3] A.Abdelli and N.Badache. "Synchronized Transitions Preemptive Time Petri Nets: A new model towards specifying multimedia requirements". In proc of IEEE ACS/AICCSA, March 8, 2006 Page(s):17-24.
• [4] R. Alur, C. Courcoubetis, and L.DILL. "Model-Checking for real time systems". In proc 5Th IEEE Symposium on Logic in Computer Science, Pages 414-425, june 1990.
• [5] R. Alur, and, L. Dill. " A Theory of Timed Automata ". Theoretical Computer Science, 126:(183-235), 1994.
• [6] R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. "The algorithmic analysis of hybrid systems". Theoretical Computer Science, 138:3-34, 1995.
• [7] B. Berthomieu and M. Menasche. "Une approche par énumération pour l'analyse des réseaux de Petri temporels". In Actes de la conférence IFIP'83, pages 71-77, 1983.
• [8] B. Berthomieu, and M. Diaz. "Modeling and verification of time dependant systems using Time Petri Nets". IEEE Transactions on Software Engineering, 17(3):(259-273),March 1991.
• [9] B. Berthomieu and F. Vernadat. "State class construction for branching analysis of Time Petri Nets". In Proc. TACAS Warsaw, Poland, Springer LNCS 2619, pages 442-457, 2003.
• [10] B. Berthomieu. "La m'ethode des classes d'états pour l'analyse des réseaux temporels: Mise en oeuvre, extension a la multi sensibilisation". In proc (MSR'2001) Toulouse (France) Oct 2001.
• [11] H. Boucheneb, and G. Berthelot. "Toward a simplified building of Time Petri Nets reachability graph". In Proc of the IEEE CS 5th (PNPM93), pages 46-55, Toulouse, France, October 1993.
• [12] H. Boucheneb and G. Berthelot. "Composition des réseaux de Petri temporisés". Revue Hermes- TSI Volume 17, n_6 , juin 1998.
• [13] H. Boucheneb and J. Mullins. "Analyse des réseaux de Petri temporels : Calcul des classes en O(n2) et des temps de chemin en O(m x n)". Revue Techniques et Sciences Informatiques, No 4/2003.
• [14] H. Boucheneb, R. Hadjidj. "CTL* model-checking of Time Petri Nets". Journal of Theoretical Computer Science, Vol 353/1-3 pp 208-227, November 2005.
• [15] M. Boyer. "Translation from timed Petri nets with intervals on transitions to intervals on places (with urgency)". Elseiver ENTCS. 65(6):(20).
• [16] M. Boyer, and M. Diaz. "Non equivalence between time Petri nets and time stream Petri nets". Proceedings of IEEE CS 9th (PNPM'99), pages 198-207, Zaragoza, Spain, September 1999.
• [17] A. Cerone and A. Maggiolo-Schettini. "Time-base expressivity of time petri nets for system specification". Theoretical Computer Science, 216(1-2):1-53,March 1999.
• [18] Dill, D. "Timing assumptions and verification of finite-state concurrent systems". In Workshop Automatic Verification Methods for Finite-State Systems. Volume 407. (1989) 197-212.
• [19] M. Diaz, and P. Senac. "Time Stream Petri Nets: A model for timed multimedia information". In R.Valette, editor, Proceedings of the 15th ICATPN, volume 815 of LNCS, pages 219-238, Zaragosse, Spain, June 1994.
• [20] G. Gardey, O.H. Roux and, O.F.Roux. "A zone based method for computing the state space of time Petri Nets". In formal modelling and analysis of timed systems (FORMATS'03) Vol LNCS 2791, Sept 2003.
• [21] G.Gardey, D. Lime, M. Magnin, and O. (H.). "Roux: Roméo: A tool for analyzing time Petri nets". In 17th CAV'05, volume 3576 of LNCS, Edinburgh, Scotland, UK, July 2005. .
• [22] T.A Henzinger, X.Nicollin, J. Sifakis, and S.Yovine. " Symbolic model-checking for real time systems". In Proc. 7th LICS, pages 394-406. IEEE Computer Society Press 1992.
• [23] K. Khansa, J. Denat, and S. Collart-Dutilleul. "P-Time petri nets for manufacturing systems". In Proc. Of WODES'96, pages 94-102, Edimburgh, UK, 1996.
• [24] J.Lilius. "Efficient state space search for time Petri nets". In MFCS Workshop on concurrency '98 Vol 18 of Electronic Notes in Theoretical Computer Science. Elsevier,1999.
• [25] D.Lime, and O.H. Roux. "State class timed automaton of a time Petri net". In 10th International workshop on Petri Nets and PerformanceModels. (PNPM'03) IEEE computer society, september 2003.
• [26] T. Little, and A.Ghafoor. "Synchronisation and storage models for multimedia objects". IEEE Selected Areas on Communication, 8(3):413-427,March 1990.
• [27] P. Merlin. "A study of the recoverability of computer system". PhD thesis" Dep. Comput. Science, Univ. California, Irvine, 1974.
• [28] R Milner "A calculus of communicating systems". LNCS springer Verlag Vol 92 1980.
• [29] Real Player Home page Url: http://real.com.
• [30] C. Ramchandani. "Analysis of Asynchronous Concurrent Systems by Timed Petri Nets". PhD thesis, MIT, Cambridge, Feb 1974.
• [31] P.N.M.Sampaio J.P.Courtiat. "Providing consistent SMIL2.0 documents". ICME'2002, Switzland, 26-29 Aoˆut 2002, 4p.
• [32] P. Senac, M. Diaz, A. Leger, and P. de Saqui-Sannes. " Modelling logical and temporal synchronization in hypermedia systems". IEEE Journal on Selected Areas in Communications, 14(1):84-103, Januar 1996.
• [33] J.Sifakis. "Use of Petri nets for performance evaluation". In E.Beilner and E.Gelenbe, Editors, Measuring Modelling and Evaluating Computer Systems, pages 75-93, North-Holland, 1977.
• [34] SMIL 2.0: W3C Recommendations. "SMIL2.0 Specification". URL:http://www.w3.org/TR/SMIL20 1.02).
• [35] S. Tripakis, S.Yovine. "Analysis of timed Systems based on time abstracting bisimulations ". Formal method in system design Kluwer Academic Publishers 2001.
• [36] E.Vicario. "Static Analysis and Dynamic Steering of Time-Dependent Systems"; IEEE TSE. 27(8): 728-748 (2001).
• [37] B. Walter. "Timed net for modeling and analysing protocols with time". In Proceedings of the IFIP Conference on Protocol Specification Testing and Verification, North Holland, 1983.
• [38] T. Yoneda, and K. H. Ryuba. "CTL Model checking of time Petri Net Using Geometric Regions". IEEE Transaction on Information and Systems, Volume E99-D, n_3, 1998 1-10.
• [39] S.Yovine. "Kronos: A verification tool for real time systems". Springer Journal STFTT, 1(1), 1997.