{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T17:55:49Z","timestamp":1790877349822,"version":"4.1.0"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2006,4,1]],"date-time":"2006-04-01T00:00:00Z","timestamp":1143849600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2006,4]]},"DOI":"10.1007\/s10626-006-8133-9","type":"journal-article","created":{"date-parts":[[2006,5,1]],"date-time":"2006-05-01T13:44:25Z","timestamp":1146491065000},"page":"179-205","source":"Crossref","is-referenced-by-count":63,"title":["Model Checking of Time Petri Nets Using the State Class Timed Automaton"],"prefix":"10.1007","volume":"16","author":[{"given":"Didier","family":"Lime","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Olivier H.","family":"Roux","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2006,5,5]]},"reference":[{"key":"8133_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla PA, Nyl\u00e9n A (2001). Timed petri nets and bqos. In 22nd International Conference on Application and Theory of Petri Nets (ICATPN'01), Newcastle upon Tyne, United Kingdom, Vol. 2075 of Lecture Notes in Computer Science. Springer, Berlin Heidelberg New York, pp 53\u201372.","DOI":"10.1007\/3-540-45740-2_5"},{"issue":"1","key":"8133_CR2","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur R, Courcoubetis C, Dill DL (1993). Model-checking in dense real-time, Information and Computation, 104(1): 2\u201334.","journal-title":"Information and Computation"},{"key":"8133_CR3","unstructured":"Arnold A (1994). Finite Transition System. Prentice Hall."},{"key":"8133_CR4","unstructured":"Berthomieu B (2001). La m\u00e9thode des classes d'\u00e9tats pour l'analyse des r\u00e9seaux temporels. In 3e congr\u00e8s Mod\u00e9lisation des Syst\u00e8mes R\u00e9actifs (MSR'2001) Hermes France: Toulouse, pp. 275\u2013290."},{"issue":"3","key":"8133_CR5","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1109\/32.75415","volume":"17","author":"B Berthomieu","year":"1991","unstructured":"Berthomieu B, Diaz M (1991). Modeling and verification of time dependent systems using time petri nets, IEEE Transactions on Software Engineering, 17(3): 259\u2013273.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"8133_CR6","doi-asserted-by":"crossref","unstructured":"Berthomieu B, Vernadat F (2003). State class constructions for branching analysis of time Petri nets. In 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'2003) Springer, Berlin Heidelberg New York, pp. 442\u2013457.","DOI":"10.1007\/3-540-36577-X_33"},{"key":"8133_CR7","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/3-540-49213-5_5","volume":"1536","author":"S Bornot","year":"1998","unstructured":"Bornot S, Sifakis J, Tripakis S (1998). Modeling urgency in timed systems, Lecture Notes in Computer Science, 1536: 103\u2013129.","journal-title":"Lecture Notes in Computer Science"},{"key":"8133_CR8","unstructured":"Bowden F DJ (1996). Modelling time in petri nets. In 2nd Australia\u2013Japan Workshop on Stochastic Models in Engineering, Technology and Management. Australia: Gold Coast."},{"key":"8133_CR9","unstructured":"Dantzig GB (1963). Linear programming and extensions. IEICE Transactions on Information and Systems."},{"key":"8133_CR10","doi-asserted-by":"crossref","unstructured":"Daws C, Yovine S (1996). Reducing the number of clock variables of timed automata. In 1996 IEEE Real-Time Systems Symposium (RTSS'96). Washington, District of Columbia: IEEE Computer Society, pp 73\u201381.","DOI":"10.1109\/REAL.1996.563702"},{"key":"8133_CR11","unstructured":"de Frutos Escrig D, Valero Rui, V, Marroqu\u00edn Alonso O (2000). Decidability of properties of timedarc petri nets. In 21st International Conference on Application and Theory of Petri Nets (ICATPN'00),Aarhus, Denmark, Vol. 1825 of Lecture Notes in Computer Science. Springer, Berlin Heidelberg New York, pp. 187\u2013206."},{"key":"8133_CR12","doi-asserted-by":"crossref","unstructured":"Delfieu D, Molinaro P, Roux OH (2000). Analyzing temporal constraints with binary decision diagrams. In 25th IFAC Workshop on Real-Time Programming (WRTP'00). Palma, Spain, pp. 131\u2013136.","DOI":"10.1016\/S1474-6670(17)39943-3"},{"key":"8133_CR13","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/3-540-58152-9_13","volume":"815","author":"M Diaz","year":"1994","unstructured":"Diaz M, Senac P (1994). Time stream Petri nets: a model for timed multimedia information, Lecture Notes in Computer Science, 815: 219\u2013238.","journal-title":"Lecture Notes in Computer Science"},{"key":"8133_CR14","doi-asserted-by":"crossref","unstructured":"Gardey G, Roux OH, Roux OF (2006). State space computation and analysis of time Petri nets. Theory and Practice of Logic Programming (TPLP). Special Issue on Specification Analysis and Verification of Reactive Systems, (to appear).","DOI":"10.1017\/S147106840600264X"},{"issue":"2","key":"8133_CR15","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"TA Henzinger","year":"1994","unstructured":"Henzinger TA, Nicollin X, Sifakis J, Yovine S (1994). Symbolic model checking for real-time systems, Information and Computation, 111(2): 193\u2013244.","journal-title":"Information and Computation"},{"key":"8133_CR16","unstructured":"Khansa W, Denat J-P, Collart-Dutilleul S (1996). P-Time Petri Nets for manufacturing systems. In International Workshop on Discrete Event Systems, WODES'96. UK: Edinburgh, pp 94\u2013102."},{"key":"8133_CR17","doi-asserted-by":"crossref","unstructured":"Larsen KG, Pettersson P, Yi W (1995). Model-checking for real-time systems. In Fundamentals of Computation Theory, pp 62\u201388.","DOI":"10.1007\/3-540-60249-6_41"},{"issue":"1\u20132","key":"8133_CR18","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen KG, Pettersson P, Yi W (1997). UPPAAL in a nutshell, International Journal on Software Tools for Technology Transfer, 1(1\u20132): 134\u2013152.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"8133_CR19","unstructured":"Lilius J (1999). Efficient state space search for time petri nets. In MFCS Workshop on Concurrency '98. Vol. 18 of ENTCS. Elsevier."},{"key":"8133_CR20","unstructured":"Lime D, Roux OH (2004). http:\/\/romeo.rts-software.org."},{"key":"8133_CR21","unstructured":"Menasche M (1982) Analyse des r\u00e9seaux de Petri temporis\u00e9s et application aux syst\u00e8mes distribu\u00e9s. PhD thesis. Universit\u00e9 Paul Sabatier. France: Toulouse"},{"key":"8133_CR22","unstructured":"Merlin PM (1974). A study of the recoverability of computing systems, PhD thesis, Department of Information and Computer Science, University of California, Irvine, California."},{"key":"8133_CR23","doi-asserted-by":"crossref","unstructured":"Penczek W, Polrola A (2004). Specification and model checking of temporal properties in time Petri nets and timed automata. In The 25th International Conference on Application and Theory of Petri Nets, (ICATPN 2004). Vol. 3099 of Lecture Notes in Computer Science, Italy, Bologna. Springer, Berlin Heidelberg New York.","DOI":"10.1007\/978-3-540-27793-4_4"},{"key":"8133_CR24","unstructured":"Pezze M, Toung M (1999). Time Petri nets: a primer introduction. Tutorial presented at the Multi-Workshop on Formal Methods in Performance Evaluation and Applications, Zaragoza, Spain."},{"issue":"4","key":"8133_CR25","first-page":"227","volume":"27","author":"L Popova","year":"1991","unstructured":"Popova L (1991). On time petri nets, Journal Information Processing and Cybernetics, EIK, 27(4): 227\u2013244.","journal-title":"Journal Information Processing and Cybernetics, EIK"},{"key":"8133_CR26","unstructured":"Ramchandani C (1974). Analysis of asynchronous concurrent systems by timed Petri nets. PhD thesis. Massachusetts Institute of Technology. Cambridge, Massachusetts. Project MAC Report MAC-TR-120."},{"key":"8133_CR27","unstructured":"Roux O H, D\u00e9planche A-M (2002). A t-time petri net extension for real time-task scheduling modeling, European Journal of Automation (JESA)."},{"key":"8133_CR28","unstructured":"Sava AT (2001). Sur la synth\u00e8se de la commande des syst\u00e8mes \u00e0 \u00e9v\u00e8nements discrets temporis\u00e9s, PhD thesis, Institut National polytechnique de Grenoble, Grenoble, France."},{"key":"8133_CR29","unstructured":"Sifakis J, Yovine S (1996). Compositional specification of timed systems (extended abstract). In 13th Syposium on Theoretical Aspects of Computer Science, France: Grenoble, Springer, Berlin Heidelberg New York, pp 347\u2013359."},{"key":"8133_CR30","doi-asserted-by":"crossref","unstructured":"Toussaint J, Simonot-Lion F, Thomesse Jean-Pierre (1997). Time constraint verifications methods based time petri nets. In 6th Workshop on Future Trends in Distributed Computing Systems (FTDCS'97). Tunisia: Tunis, pp 262\u2013267.","DOI":"10.1109\/FTDCS.1997.644736"},{"issue":"8","key":"8133_CR31","doi-asserted-by":"crossref","first-page":"728","DOI":"10.1109\/32.940727","volume":"27","author":"E Vicario","year":"2001","unstructured":"Vicario E (2001). Static analysis and dynamic steering of time-dependent systems, IEEE Transactions on Software Engineering, 27(8): 728\u2013748.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"3","key":"8133_CR32","first-page":"297","volume":"E99-D","author":"T Yoneda","year":"1998","unstructured":"Yoneda T, Ryuba H (1998). CTL model checking of time petri nets using geometric regions, IEICE Transactions on Information and Systems, E99-D(3): 297\u2013396.","journal-title":"IEICE Transactions on Information and Systems"},{"issue":"1\u20132","key":"8133_CR33","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S Yovine","year":"1997","unstructured":"Yovine S (1997). Kronos: a verification tool for real-time systems, International Journal of Software Tools for Technology Transfer, 1(1\u20132): 123\u2013133.","journal-title":"International Journal of Software Tools for Technology Transfer"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-006-8133-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10626-006-8133-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-006-8133-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T19:58:50Z","timestamp":1559246330000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10626-006-8133-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,4]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2006,4]]}},"alternative-id":["8133"],"URL":"https:\/\/doi.org\/10.1007\/s10626-006-8133-9","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"value":"0924-6703","type":"print"},{"value":"1573-7594","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,4]]}}}