{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:51:42Z","timestamp":1750308702260,"version":"3.41.0"},"reference-count":20,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["CNS-0435060CCR-0325197EN-CS-0329609"],"award-info":[{"award-number":["CNS-0435060CCR-0325197EN-CS-0329609"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-0435060CCR-0325197EN-CS-0329609"],"award-info":[{"award-number":["CNS-0435060CCR-0325197EN-CS-0329609"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2013,1]]},"abstract":"<jats:p>The main problem of verification techniques based on exploration of (reachable) state space is the state explosion problem. In timed models, abstract states reached by different interleavings of the same set of transitions are, in general, different and their union is not necessarily an abstract state. To attenuate this state explosion, it would be interesting to reduce the redundancy caused by the interleaving semantics by agglomerating all these abstract states whenever their union is an abstract state.<\/jats:p>\n          <jats:p>This article considers the time Petri net model and establishes some sufficient conditions that ensure that this union is an abstract state. In addition, it proposes a procedure to compute this union without computing beforehand intermediate abstract states. Finally, it shows how to use this result to improve the reachability analysis.<\/jats:p>","DOI":"10.1145\/2406336.2406343","type":"journal-article","created":{"date-parts":[[2013,1,29]],"date-time":"2013-01-29T16:20:55Z","timestamp":1359476455000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Reducing Interleaving Semantics Redundancy in Reachability Analysis of Time Petri Nets"],"prefix":"10.1145","volume":"12","author":[{"given":"Hanifa","family":"Boucheneb","sequence":"first","affiliation":[{"name":"Laboratoire VeriForm, \u00c9cole Polytechnique de Montr\u00e9al"}]},{"given":"Kamel","family":"Barkaoui","sequence":"additional","affiliation":[{"name":"Laboratoire CEDRIC, Conservatoire National des Arts et M\u00e9tiers"}]}],"member":"320","published-online":{"date-parts":[[2013,1]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-005-0190-0"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_31"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.75415"},{"volume":"2619","volume-title":"Proceedings of the 9th International Conference onTools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science","author":"Berthomieu B.","key":"e_1_2_1_5_1"},{"volume":"4762","volume-title":"Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201907)","author":"Berthomieu B.","key":"e_1_2_1_6_1"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.11.002"},{"key":"e_1_2_1_8_1","first-page":"469","article-title":"A more efficient time Petri net state space abstraction useful to model checking timed linear properties","volume":"88","author":"Boucheneb H.","year":"2008","journal-title":"J. Fundamenta Informaticae"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.05.037"},{"volume-title":"Proceedings of the 3rd International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS\u201909)","author":"Boucheneb H.","key":"e_1_2_1_10_1"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exp036"},{"volume-title":"Clock Matrix Diagrams. Bachelors Thesis","author":"Fass D.","key":"e_1_2_1_12_1"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Gardey G. Roux O. H. and \n      Roux O. F\n  . \n  2004\n  . Using zone graph method for computing the state space of a time Petri net. In Proceedings of the 1st International Workshop on Formal Modeling and Analysis of Timed Systems Lecture Notes in Computer Science vol. \n  2791\n  . \n  Springer\n  .  Gardey G. Roux O. H. and Roux O. F. 2004. Using zone graph method for computing the state space of a time Petri net. In Proceedings of the 1st International Workshop on Formal Modeling and Analysis of Timed Systems Lecture Notes in Computer Science vol. 2791. Springer.","DOI":"10.1007\/978-3-540-40903-8_20"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0040-3"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.24143"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Penczek W.\n     and \n      P\u00f3lrola A\n  . \n  2001\n  . Abstraction and partial order reductions for checking branching properties of time Petri nets. In Proceedings of the 22nd International Conference on Applications and Theory of Petri Nets Lecture Notes in Computer Science vol. \n  2075 Springer 323--342.   Penczek W. and P\u00f3lrola A. 2001. Abstraction and partial order reductions for checking branching properties of time Petri nets. In Proceedings of the 22nd International Conference on Applications and Theory of Petri Nets Lecture Notes in Computer Science vol. 2075 Springer 323--342.","DOI":"10.1007\/3-540-45740-2_19"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Penczek W.\n     and \n      P\u00f3lrola A\n  . \n  2004\n  . Specification and model checking of temporal properties in time Petri nets and timed automata. In Proceedings of the 25th International Conference on Applications and Theory of Petri Nets Lecture Notes in Computer Science vol. \n  3099\n  . \n  Springer\n  .  Penczek W. and P\u00f3lrola A. 2004. Specification and model checking of temporal properties in time Petri nets and timed automata. In Proceedings of the 25th International Conference on Applications and Theory of Petri Nets Lecture Notes in Computer Science vol. 3099. Springer.","DOI":"10.1007\/978-3-540-27793-4_4"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1093\/ietisy\/e88-d.7.1646"},{"volume":"2529","volume-title":"Proceedings of the International Conference on Formal Techniques for Networked and Distributed Systems. Lecture Notes in Computer Science.","author":"Ribet P. O.","key":"e_1_2_1_20_1"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008682131325"},{"key":"e_1_2_1_22_1","first-page":"1","article-title":"CTL model checking of Time Petri Nets using geometric regions. IEICE","volume":"3","author":"Yoneda T.","year":"1998","journal-title":"Trans. Inf. Syst. E99-D"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2406336.2406343","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2406336.2406343","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:13:55Z","timestamp":1750277635000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2406336.2406343"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1]]},"references-count":20,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,1]]}},"alternative-id":["10.1145\/2406336.2406343"],"URL":"https:\/\/doi.org\/10.1145\/2406336.2406343","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2013,1]]},"assertion":[{"value":"2010-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}