{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T21:36:59Z","timestamp":1775684219070,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540755951","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75596-8_37","type":"book-chapter","created":{"date-parts":[[2007,11,3]],"date-time":"2007-11-03T14:03:37Z","timestamp":1194098617000},"page":"523-532","source":"Crossref","is-referenced-by-count":20,"title":["Model Checking Bounded Prioritized Time Petri Nets"],"prefix":"10.1007","author":[{"given":"Bernard","family":"Berthomieu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florent","family":"Peres","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fran\u00e7ois","family":"Vernadat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"37_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/BFb0084802","volume-title":"CONCUR 1992","author":"R. Alur","year":"1992","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Dill, D.L., Wong-Toi, H.: Minimization of timed transition systems. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol.\u00a0630, pp. 340\u2013354. Springer, Heidelberg (1992)"},{"key":"37_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/11603009_17","volume-title":"FORMATS 2005","author":"B. B\u00e9rard","year":"2005","unstructured":"B\u00e9rard, B., Cassez, F., Haddad, S., Roux, O.H., Lime, D.: Comparison of the Expressiveness of Timed Automata and Time Petri Nets. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol.\u00a03829, pp. 211\u2013225. Springer, Heidelberg (2005)"},{"issue":"3","key":"37_CR3","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1109\/32.75415","volume":"17","author":"B. Berthomieu","year":"1991","unstructured":"Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Tr. on Soft. Eng.\u00a017(3), 259\u2013273 (1991)","journal-title":"IEEE Tr. on Soft. Eng."},{"key":"37_CR4","doi-asserted-by":"crossref","unstructured":"Boucheneb, H., Hadjidj, R.: Using inclusion abstraction to construct atomic state class graphs for time petri nets. International Journal of Embedded Systems\u00a02(1\/2) (June 2006)","DOI":"10.1504\/IJES.2006.010171"},{"key":"37_CR5","first-page":"41","volume":"9","author":"B. Berthomieu","year":"1983","unstructured":"Berthomieu, B., Menasche, M.: An enumerative approach for analyzing time Petri nets. IFIP Congress Series\u00a09, 41\u201346 (1983)","journal-title":"IFIP Congress Series"},{"key":"37_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/11867340_7","volume-title":"FORMATS 2006","author":"B. Berthomieu","year":"2006","unstructured":"Berthomieu, B., Peres, F., Vernadat, F.: Bridging the gap between timed automata and bounded time petri nets. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol.\u00a04202, pp. 82\u201397. Springer, Heidelberg (2006)"},{"issue":"14","key":"37_CR7","doi-asserted-by":"publisher","first-page":"2741","DOI":"10.1080\/00207540412331312688","volume":"42","author":"B. Berthomieu","year":"2004","unstructured":"Berthomieu, B., Ribet, P.-O., Vernadat, F.: The tool TINA \u2013 construction of abstract state spaces for Petri nets and time Petri nets. International Journal of Production Research\u00a042(14), 2741\u20132756 (2004)","journal-title":"International Journal of Production Research"},{"key":"37_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"442","DOI":"10.1007\/3-540-36577-X_33","volume-title":"TACAS 2003","author":"B. Berthomieu","year":"2003","unstructured":"Berthomieu, B., Vernadat, F.: State class constructions for branching analysis of time Petri nets. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 442\u2013457. Springer, Heidelberg (2003)"},{"key":"37_CR9","volume-title":"Handbook of Real-Time and Embedded Systems","author":"B. Berthomieu","year":"2007","unstructured":"Berthomieu, B., Vernadat, F.: State Space Abstractions for Time Petri Nets. In: Lee, I., Leung, J.Y.T., Son, S. (eds.) Handbook of Real-Time and Embedded Systems, CRC Press, Boca Raton (2007)"},{"key":"37_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/11867340_10","volume-title":"FORMATS 2006","author":"A. David","year":"2006","unstructured":"David, A., H\u00e5kansson, J., Larsen, K.G., Pettersson, P.: Model checking timed automata with priorities using DBM subtraction. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol.\u00a04202, pp. 128\u2013142. Springer, Heidelberg (2006)"},{"key":"37_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"314","DOI":"10.1007\/978-3-540-30101-1_15","volume-title":"FMCO 2003","author":"G. Goessler","year":"2004","unstructured":"Goessler, G., Sifakis, J.: Priority systems. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2003. LNCS, vol.\u00a03188, pp. 314\u2013329. Springer, Heidelberg (2004)"},{"key":"37_CR12","unstructured":"Hadjidj, R.: Analyse et validation formelle des syst\u00e8mes temps r\u00e9el. PhD Thesis, Ecole Polytechnique de Montr\u00e9al, Univ. de Montr\u00e9al (February 2006)"},{"key":"37_CR13","series-title":"Lecture Notes in Computer Science","first-page":"370","volume-title":"ATVA 2005","author":"S.-W. Lin","year":"2005","unstructured":"Lin, S.-W., Hsiung, P.-A., Huang, C.-H., Chen, Y.-R.: Model checking prioritized timed automata. In: Peled, D.A., Tsay, Y.K. (eds.) ATVA 2005. LNCS, vol.\u00a03707, pp. 370\u2013384. Springer, Heidelberg (2005)"},{"key":"37_CR14","doi-asserted-by":"crossref","unstructured":"Merlin, P.M.: A Study of the Recoverability of Computing Systems. PhD Thesis, Irvine (1974)","DOI":"10.1145\/800272.810899"},{"key":"37_CR15","unstructured":"Rokicki, T.G.: Representing and Modeling Circuits. PhD Thesis, Stanford Univ. Stanford, CA (1993)"},{"issue":"3","key":"37_CR16","first-page":"1","volume":"E99-D","author":"T. Yoneda","year":"1998","unstructured":"Yoneda, T., Ryuba, H.: CTL model checking of Time Petri nets using geometric regions. IEEE Trans. on Inf. and Systems\u00a0E99-D(3), 1\u201310 (1998)","journal-title":"IEEE Trans. on Inf. and Systems"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75596-8_37.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,14]],"date-time":"2023-05-14T16:09:03Z","timestamp":1684080543000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75596-8_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540755951"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75596-8_37","relation":{},"subject":[]}}