{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T21:36:58Z","timestamp":1775684218155,"version":"3.50.1"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030296612","type":"print"},{"value":"9783030296629","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-29662-9_5","type":"book-chapter","created":{"date-parts":[[2019,8,19]],"date-time":"2019-08-19T19:03:06Z","timestamp":1566241386000},"page":"79-95","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["A State Class Construction for Computing the Intersection of Time Petri Nets Languages"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1514-8166","authenticated-orcid":false,"given":"\u00c9ric","family":"Lubat","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6002-2696","authenticated-orcid":false,"given":"Silvano","family":"Dal Zilio","sequence":"additional","affiliation":[]},{"given":"Didier","family":"Le Botlan","sequence":"additional","affiliation":[]},{"given":"Yannick","family":"Pencol\u00e9","sequence":"additional","affiliation":[]},{"given":"Audine","family":"Subias","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,8,13]]},"reference":[{"issue":"1\/2","key":"5_CR1","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1504\/IJCCBS.2014.059593","volume":"5","author":"Nouha Abid","year":"2014","unstructured":"Abid, N., Dal Zilio, S., Le Botlan, D.: A formal framework to specify and verify real-time properties on critical systems. Int. J. Crit. Comput. Based Syst. (IJCCBS) 5(1\/2) (2014). \n                      https:\/\/doi.org\/10.1504\/IJCCBS.2014.059593","journal-title":"International Journal of Critical Computer-Based Systems"},{"issue":"2","key":"5_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"Rajeev Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2) (1994). \n                      https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theoretical Computer Science"},{"issue":"1-2","key":"5_CR3","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/S0304-3975(02)00006-3","volume":"281","author":"Andr\u00e9 Arnold","year":"2002","unstructured":"Arnold, A.: Nivat\u2019s processes and their synchronization. Theor. Comput. Sci. 281(1\u20132) (2002). \n                      https:\/\/doi.org\/10.1016\/S0304-3975(02)00006-3","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"5_CR4","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1145\/506147.506151","volume":"49","author":"Eugene Asarin","year":"2002","unstructured":"Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. J. ACM 49(2) (2002). \n                      https:\/\/doi.org\/10.1145\/506147.506151","journal-title":"Journal of the ACM"},{"issue":"3","key":"5_CR5","doi-asserted-by":"publisher","first-page":"1384","DOI":"10.1109\/TAC.2016.2588736","volume":"62","author":"Francesco Basile","year":"2017","unstructured":"Basile, F., Cabasino, M.P., Seatzu, C.: Diagnosability analysis of labeled time Petri net systems. IEEE Trans. Autom. Control 62(3) (2017). \n                      https:\/\/doi.org\/10.1109\/TAC.2016.2588736","journal-title":"IEEE Transactions on Automatic Control"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: Software Engineering and Formal Methods (SEFM). IEEE (2006). \n                      https:\/\/doi.org\/10.1109\/SEFM.2006.27","DOI":"10.1109\/SEFM.2006.27"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/11603009_17","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"B B\u00e9rard","year":"2005","unstructured":"B\u00e9rard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: Comparison of the expressiveness of timed automata and time Petri nets. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 211\u2013225. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/11603009_17"},{"issue":"3","key":"5_CR8","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 Trans. Softw. Eng. 17(3) (1991). \n                      https:\/\/doi.org\/10.1109\/32.75415","journal-title":"IEEE Transactions on Software Engineering"},{"key":"5_CR9","unstructured":"Berthomieu, B., Menasche, M.: An enumerative approach for analyzing time Petri nets. In: Proceedings IFIP (1983)"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/11867340_7","volume-title":"Formal Modeling and Analysis of Timed Systems","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. 4202, pp. 82\u201397. Springer, Heidelberg (2006). \n                      https:\/\/doi.org\/10.1007\/11867340_7"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1007\/978-3-540-75596-8_37","volume-title":"Automated Technology for Verification and Analysis","author":"B Berthomieu","year":"2007","unstructured":"Berthomieu, B., Peres, F., Vernadat, F.: Model checking bounded prioritized time Petri nets. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 523\u2013532. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-75596-8_37"},{"issue":"14","key":"5_CR12","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-construction of abstract state spaces for Petri nets and time Petri nets. Int. J. Prod. Res. 42(14), 2741\u20132756 (2004)","journal-title":"Int. J. Prod. Res."},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/3-540-36577-X_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","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. 2619, pp. 442\u2013457. Springer, Heidelberg (2003). \n                      https:\/\/doi.org\/10.1007\/3-540-36577-X_33"},{"key":"5_CR14","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/j.scico.2016.08.008","volume":"132","author":"Pierre-Alain Bourdil","year":"2016","unstructured":"Bourdil, P.A., Berthomieu, B., Dal Zilio, S., Vernadat, F.: Symmetry reduction for time Petri net state classes. Sci. Comput. Program. 132(2) (2016). \n                      https:\/\/doi.org\/10.1016\/j.scico.2016.08.008","journal-title":"Science of Computer Programming"},{"issue":"2-3","key":"5_CR15","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1016\/j.tcs.2008.03.030","volume":"403","author":"B. B\u00e9rard","year":"2008","unstructured":"B\u00e9rard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: When are timed automata weakly timed bisimilar to time Petri nets? Theoret. Comput. Sci. 403(2\u20133) (2008). \n                      https:\/\/doi.org\/10.1016\/j.tcs.2008.03.030","journal-title":"Theoretical Computer Science"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11867340_5","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"B B\u00e9rard","year":"2006","unstructured":"B\u00e9rard, B., Gastin, P., Petit, A.: Intersection of regular signal-event (timed) languages. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 52\u201366. Springer, Heidelberg (2006). \n                      https:\/\/doi.org\/10.1007\/11867340_5"},{"issue":"12","key":"5_CR17","doi-asserted-by":"publisher","first-page":"3104","DOI":"10.1109\/TAC.2012.2200372","volume":"57","author":"M. P. Cabasino","year":"2012","unstructured":"Cabasino, M.P., Giua, A., Lafortune, S., Seatzu, C.: A new approach for diagnosability analysis of Petri nets using verifier nets. IEEE Trans. Autom. Control 57(12) (2012). \n                      https:\/\/doi.org\/10.1109\/TAC.2012.2200372","journal-title":"IEEE Transactions on Automatic Control"},{"key":"5_CR18","unstructured":"Cabasino, M.P., Giua, A., Seatzu, C.: Discrete event diagnosis using Petri nets. In: ICINCO-ICSO (2009)"},{"issue":"10","key":"5_CR19","doi-asserted-by":"publisher","first-page":"1456","DOI":"10.1016\/j.jss.2005.12.021","volume":"79","author":"Franck Cassez","year":"2006","unstructured":"Cassez, F., Roux, O.H.: Structural translation from time Petri nets to timed automata. J. Syst. Softw. 79(10) (2006). \n                      https:\/\/doi.org\/10.1016\/j.jss.2005.12.021","journal-title":"Journal of Systems and Software"},{"key":"5_CR20","unstructured":"Cimatti, A., Pecheur, C., Cavada, R.: Formal verification of diagnosability via symbolic model checking. In: IJCAI (2003)"},{"key":"5_CR21","unstructured":"Dal Zilio, S.: TWINA: a realtime model-checker for analyzing Twin-TPN (2019). \n                      https:\/\/projects.laas.fr\/twina\/"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/11513988_41","volume-title":"Computer Aided Verification","author":"G Gardey","year":"2005","unstructured":"Gardey, G., Lime, D., Magnin, M., Roux, O.H.: Romeo: a tool for analyzing time Petri nets. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 418\u2013423. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/11513988_41"},{"issue":"1","key":"5_CR23","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10626-016-0234-5","volume":"27","author":"Houssam-Eddine Gougam","year":"2016","unstructured":"Gougam, H.E., Pencol\u00e9, Y., Subias, A.: Diagnosability analysis of patterns on bounded labeled prioritized Petri nets. Discrete Event Dyn. Syst. 27(1) (2017). \n                      https:\/\/doi.org\/10.1007\/s10626-016-0234-5","journal-title":"Discrete Event Dynamic Systems"},{"issue":"8","key":"5_CR24","doi-asserted-by":"publisher","first-page":"1318","DOI":"10.1109\/9.940942","volume":"46","author":"Shengbing Jiang","year":"2001","unstructured":"Jiang, S., Huang, Z., Chandra, V., Kumar, R.: A polynomial algorithm for testing diagnosability of discrete-event systems. IEEE Trans. Autom. Control 46(8) (2001). \n                      https:\/\/doi.org\/10.1109\/9.940942","journal-title":"IEEE Transactions on Automatic Control"},{"issue":"2","key":"5_CR25","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"Orna Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM (JACM) 47(2) (2000). \n                      https:\/\/doi.org\/10.1145\/333979.333987","journal-title":"Journal of the ACM"},{"key":"5_CR26","unstructured":"Merlin, P.M.: A study of the recoverability of computing systems. Ph.D. thesis, Department of Information and Computer Science, University of California (1974)"},{"issue":"3","key":"5_CR27","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/s10626-011-0102-2","volume":"21","author":"Florent Peres","year":"2011","unstructured":"Peres, F., Berthomieu, B., Vernadat, F.: On the composition of time Petri nets. Discrete Event Dyn. Syst. 21(3) (2011). \n                      https:\/\/doi.org\/10.1007\/s10626-011-0102-2","journal-title":"Discrete Event Dynamic Systems"},{"issue":"1","key":"5_CR28","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1109\/5.21072","volume":"77","author":"PJ Ramadge","year":"1989","unstructured":"Ramadge, P.J., Wonham, W.M.: The control of discrete event systems. Proc. IEEE 77(1), 81\u201398 (1989). \n                      https:\/\/doi.org\/10.1109\/5.21072","journal-title":"Proc. IEEE"},{"issue":"9","key":"5_CR29","doi-asserted-by":"publisher","first-page":"1555","DOI":"10.1109\/9.412626","volume":"40","author":"M Sampath","year":"1995","unstructured":"Sampath, M., Sengupta, R., Lafortune, S., Sinnamohideen, K., Teneketzis, D.: Diagnosability of discrete-event systems. IEEE Trans. Autom. Control 40(9), 1555\u20131575 (1995). \n                      https:\/\/doi.org\/10.1109\/9.412626","journal-title":"IEEE Trans. Autom. Control"},{"key":"5_CR30","doi-asserted-by":"publisher","unstructured":"Toussaint, J., Simonot-Lion, F., Thomesse, J.P.: Time constraint verification methods based on time Petri nets. In: Workshop on Future Trends of Distributed Computing Systems. IEEE (1997). \n                      https:\/\/doi.org\/10.1109\/FTDCS.1997.644736","DOI":"10.1109\/FTDCS.1997.644736"},{"key":"5_CR31","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/3-540-45739-9_14","volume-title":"Lecture Notes in Computer Science","author":"Stavros Tripakis","year":"2002","unstructured":"Tripakis, S.: Fault diagnosis for timed automata. In: Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT) (2002). \n                      https:\/\/doi.org\/10.1007\/3-540-45739-9_14"},{"key":"5_CR32","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-642-15297-9_12","volume-title":"Lecture Notes in Computer Science","author":"Bartosz Grabiec","year":"2010","unstructured":"Wang, X., Mahulea, C., Silva, M.: Diagnosis of time Petri nets using fault diagnosis graph. IEEE Trans. Autom. Control 60(9) (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-642-15297-9_12"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-29662-9_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,19]],"date-time":"2019-08-19T19:03:35Z","timestamp":1566241415000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-29662-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030296612","9783030296629"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29662-9_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"13 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FORMATS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Modeling and Analysis of Timed Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Amsterdam","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"The Netherlands","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 August 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 August 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"formats2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/lipn.univ-paris13.fr\/formats2019\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"42","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"36% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.1","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4.4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}