{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,26]],"date-time":"2026-08-26T01:50:02Z","timestamp":1787709002358,"version":"build-2784847793"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540008989","type":"print"},{"value":"9783540365778","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_33","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T17:12:04Z","timestamp":1269882724000},"page":"442-457","source":"Crossref","is-referenced-by-count":61,"title":["State Class Constructions for Branching Analysis of Time Petri Nets"],"prefix":"10.1007","author":[{"given":"Bernard","family":"Berthomieu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fran\u00e7ois","family":"Vernadat","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"33_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proc. 5th IEEE Symposium on Logic in Computer Science, pages 414\u2013425, june 1990.","DOI":"10.1109\/LICS.1990.113766"},{"key":"33_CR2","series-title":"Lect Notes Comput Sci","first-page":"340","volume-title":"CONCUR 92: Theories of Concurrency","author":"R. Alur","year":"1996","unstructured":"R. Alur, C. Courcoubetis, N. Halbwachs, D.L. Dill, and H. Wong-Toi. Minimization of timed transition systems. In CONCUR 92: Theories of Concurrency, Springer LNCS 630, pages 340\u2013354, 1996."},{"key":"33_CR3","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M. C. Browne","year":"1988","unstructured":"M. C. Browne, E. M. Clarke, and O. Gr\u00fcmberg. Characterizing finite kripke structures in propositional temporal logics. Theoretical Computer Science, 59:115\u2013131, 1988.","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"33_CR4","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1109\/32.75415","volume":"17","author":"B. Berthomieu","year":"1991","unstructured":"B. Berthomieu and M. Diaz. Modeling and verification of time dependent systems using time Petri nets. IEEE Transactions on Software Engineering, 17(3):259\u2013273, March 1991.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"33_CR5","unstructured":"B. Berthomieu. La m\u00e9thode des classes d\u2019tats pour l\u2019analyse des r\u015beaux temporels-mise en\u0153uvre, extension \u013aa multi-sensibilisation. In Proc. Mod\u00e9lisation des Syst\u00e9mes R\u00e1ctifs, Toulouse, France, October 2001."},{"key":"33_CR6","unstructured":"B. Berthomieu. The Tina V2 Toolbox. \n                    http:\/\/www.laas.fr\/tina\n                    \n                  , LAAS\/CNRS, 2001."},{"key":"33_CR7","first-page":"41","volume":"9","author":"B. Berthomieu","year":"1983","unstructured":"B. Berthomieu and M. Menasche. An enumerative approach for analyzing time Petri nets. IFIP Congress Series, 9:41\u201346, 1983.","journal-title":"IFIP Congress Series"},{"key":"33_CR8","series-title":"Lect Notes Comput Sci","volume-title":"CADP: A protocol validation and verification toolbox","author":"J.-C. Fernandez","year":"1996","unstructured":"J-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu. CADP: A protocol validation and verification toolbox. In 8th Conference on Computer-Aided Verification, CAV\u201996, Springer LNCS 1102, July 1996."},{"key":"33_CR9","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"P. K. Kanellakis","year":"1990","unstructured":"P. K. Kanellakis and S. A. Smolka. Ccs expressions, finite state processes, and three problems of equivalence. Information and Computation, 86:43\u201368, 1990.","journal-title":"Information and Computation"},{"issue":"2","key":"33_CR10","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"R. Nicola De","year":"1995","unstructured":"R. De Nicola and F. Vandrager. Three logics for branching bisimulation. Journal of the ACM, 42(2):458\u2013487, 1995.","journal-title":"Journal of the ACM"},{"key":"33_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1007\/3-540-45740-2_19","volume-title":"Abstraction and partial order reductions for checking branching properties of time petri nets","author":"W. Penczek","year":"2001","unstructured":"W. Penczek and A. P\u00f3lrola. Abstraction and partial order reductions for checking branching properties of time petri nets. In Proc. of ICATPN, Springer LNCS 2075, pages 323\u2013342, 2001."},{"issue":"6","key":"33_CR12","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"P. Paige","year":"1987","unstructured":"P. Paige and R. E. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16(6):973\u2013989, 1987.","journal-title":"SIAM Journal on Computing"},{"key":"33_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/3-540-61474-5_72","volume-title":"Analysis of timed systems based on time-abstracting bisimulations","author":"S. Tripakis","year":"1996","unstructured":"S. Tripakis and S. Yovine. Analysis of timed systems based on time-abstracting bisimulations. In 8th Conference Computer-Aided Verification, CAV\u201996, Springer LNCS 1102, pages 232\u2013243, jul 1996."},{"key":"33_CR14","doi-asserted-by":"crossref","unstructured":"S. Yovine. Kronos: A verification tool for real-time systems. International Journal of Software Tools for Technology Transfer, 1(1), 1997.","DOI":"10.1007\/s100090050009"},{"issue":"3","key":"33_CR15","first-page":"1","volume":"E99-D","author":"T. Yoneda","year":"1998","unstructured":"T. Yoneda and H. Ryuba. CTL model checking of Time Petri nets using geometric regions. IEEE Transactions on Information and Systems, E99-D(3):1\u201310, 1998.","journal-title":"IEEE Transactions on Information and Systems"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36577-X_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,24]],"date-time":"2019-02-24T08:55:54Z","timestamp":1550998554000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_33","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2003]]}}}