{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T09:26:24Z","timestamp":1750843584762},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2022,12,22]],"date-time":"2022-12-22T00:00:00Z","timestamp":1671667200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,12,22]],"date-time":"2022-12-22T00:00:00Z","timestamp":1671667200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2023,2]]},"DOI":"10.1007\/s10009-022-00694-8","type":"journal-article","created":{"date-parts":[[2022,12,22]],"date-time":"2022-12-22T08:04:26Z","timestamp":1671696266000},"page":"95-114","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Leveraging polyhedral reductions for solving Petri net reachability problems"],"prefix":"10.1007","volume":"25","author":[{"given":"Nicolas","family":"Amat","sequence":"first","affiliation":[]},{"given":"Silvano","family":"Dal Zilio","sequence":"additional","affiliation":[]},{"given":"Didier","family":"Le Botlan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,12,22]]},"reference":[{"key":"694_CR1","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-030-76983-3_9","volume-title":"Application and theory of Petri nets and concurrency (Petri nets)","author":"N Amat","year":"2021","unstructured":"Amat, N., Berthomieu, B., Dal Zilio, S.: On the combination of polyhedral abstraction and SMT-based model checking for Petri nets. In: Application and theory of Petri nets and concurrency (Petri nets), pp. 164\u2013185. Springer, Cham (2021)"},{"key":"694_CR2","doi-asserted-by":"publisher","first-page":"2","DOI":"10.3233\/FI-222134","volume":"187","author":"N Amat","year":"2022","unstructured":"Amat, N., Berthomieu, B., Dal Zilio, S.: A polyhedral abstraction for Petri nets and its application to SMT-based model checking. Fundam. Inform. 187, 2\u20134 (2022)","journal-title":"Fundam. Inform."},{"key":"694_CR3","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-030-84629-9_3","volume-title":"Model checking software (SPIN)","author":"N Amat","year":"2021","unstructured":"Amat, N., Dal Zilio, S., Le Botlan, D.: Accelerating the computation of dead and concurrent places using reductions. In: Model checking software (SPIN), pp. 45\u201362. Springer (2021)"},{"key":"694_CR4","first-page":"50","volume-title":"Tools and algorithms for the construction and analysis of systems (TACAS)","author":"E Amparore","year":"2019","unstructured":"Amparore, E., Berthomieu, B., Ciardo, G., Dal Zilio, S., Gall\u00e0, F., Hillah, L.M., Hulin-Hubard, F., Jensen, P.G., Jezequel, L., Kordon, F., Le Botlan, D., Liebke, T., Meijer, J., Miner, A., Paviot-Adet, E., Srba, J., Thierry-Mieg, Y., van Dijk, T., Wolf, K.: Presentation of the 9th edition of the model checking contest. In: Tools and algorithms for the construction and analysis of systems (TACAS), pp. 50\u201368. Springer (2019)"},{"key":"694_CR5","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-540-47919-2_13","volume-title":"Petri nets: central models and their properties","author":"G Berthelot","year":"1987","unstructured":"Berthelot, G.: Transformations and decompositions of nets. In: Petri nets: central models and their properties, pp. 359\u2013376. Springer (1987)"},{"key":"694_CR6","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-319-94111-0_4","volume-title":"Model checking software (SPIN)","author":"B Berthomieu","year":"2018","unstructured":"Berthomieu, B., Le Botlan, D., Dal Zilio, S.: Petri net reductions for counting markings. In: Model checking software (SPIN), pp. 65\u201384. Springer (2018)"},{"issue":"2","key":"694_CR7","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/s10009-019-00519-1","volume":"22","author":"B Berthomieu","year":"2019","unstructured":"Berthomieu, B., Le Botlan, D., Dal Zilio, S.: Counting Petri net markings from reduction equations. Int. J. Softw. Tools Technol. Transf. 22(2), 163\u2013181 (2019)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"694_CR8","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1016\/j.jlamp.2018.09.002","volume":"102","author":"FM B\u00f8nneland","year":"2019","unstructured":"B\u00f8nneland, F.M., Dyhr, J., Jensen, P.G., Johannsen, M., Srba, J.: Stubborn versus structural reductions for Petri nets. J. Log. Algebraic Methods Program. 102, 46\u201363 (2019)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"694_CR9","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-030-76983-3_17","volume-title":"Application and theory of Petri Nets and concurrency (Petri nets)","author":"P Bouvier","year":"2021","unstructured":"Bouvier, P., Garavel, H.: Efficient algorithms for three reachability problems in safe petri nets. In: Application and theory of Petri Nets and concurrency (Petri nets), pp. 339\u2013359. Springer (2021)"},{"key":"694_CR10","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-51831-8_1","volume-title":"Application and theory of Petri nets and concurrency (Petri nets)","author":"P Bouvier","year":"2020","unstructured":"Bouvier, P., Garavel, H., Ponce-de Le\u00f3n, H.: Automatic decomposition of Petri nets into automata networks\u2014a synthetic account. In: Application and theory of Petri nets and concurrency (Petri nets), pp. 3\u201323. Springer (2020)"},{"key":"694_CR11","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1016\/j.jlamp.2018.11.005","volume":"104","author":"Hubert Garavel","year":"2019","unstructured":"Garavel, Hubert: Nested-unit Petri nets. J. Log. Algebraic Methods Program. 104, 60\u201385 (2019)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"694_CR12","unstructured":"Garavel, H.: Proposal for adding useful features to Petri-net model checkers. Research Report 03087421, Inria Grenoble-Rh\u00f4ne-Alpes (2020)"},{"key":"694_CR13","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-540-27815-3_16","volume-title":"Algebraic methodology and software technology","author":"H Garavel","year":"2004","unstructured":"Garavel, H., Serwe, W.: State space reduction for process algebra specifications. In: Algebraic methodology and software technology, pp. 164\u2013180. Springer (2004)"},{"key":"694_CR14","first-page":"974","volume-title":"IEEE international conference on systems, man, and cybernetics","author":"A Giua","year":"1992","unstructured":"Giua, A., DiCesare, F., Silva, M.: Generalized mutual exclusion contraints on nets with uncontrollable transitions. In: IEEE international conference on systems, man, and cybernetics, pp. 974\u2013979. IEEE (1992)"},{"key":"694_CR15","doi-asserted-by":"crossref","unstructured":"Hillah, L.-M., Kordon, F.: Petri nets repository: a tool to benchmark and debug Petri net tools. In: Application and theory of Petri Nets and concurrency (Petri nets), pp. 125\u2013135. Springer (2017)","DOI":"10.1007\/978-3-319-57861-3_9"},{"key":"694_CR16","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/978-3-642-13675-7_20","volume-title":"International conference on applications and theory of Petri nets","author":"L-M Hillah","year":"2010","unstructured":"Hillah, L.-M., Kordon, F., Petrucci, L., Treves, N.: PNML framework: an extendable reference implementation of the Petri Net Markup Language. In: International conference on applications and theory of Petri nets, pp. 318\u2013327. Springer (2010)"},{"key":"694_CR17","unstructured":"Hujsa, T., Berthomieu, B., Dal\u00a0Zilio, S., Le\u00a0Botlan, D.: Checking marking reachability with the state equation in Petri net subclasses. Technical Report 20278, LAAS-CNRS (2020)"},{"key":"694_CR18","unstructured":"INRIA: CADP. (2020). https:\/\/cadp.inria.fr\/"},{"key":"694_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(84)90014-8","volume":"29","author":"R Janicki","year":"1984","unstructured":"Janicki, R.: Nets, sequential components and concurrency relations. Theor. Comput. Sci. 29, 1\u20132 (1984)","journal-title":"Theor. Comput. Sci."},{"key":"694_CR20","first-page":"299","volume-title":"Application and theory of Petri nets","author":"AV Kovalyov","year":"1992","unstructured":"Kovalyov, A.V.: Concurrency relations and the safety problem for Petri nets. In: Application and theory of Petri nets, pp. 299\u2013309. Springer, Heidelberg (1992)"},{"key":"694_CR21","series-title":"Hardware design and Petri nets","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3143-9_6","volume-title":"A polynomial algorithm to compute the concurrency relation of a regular STG","author":"Andrei Kovalyov","year":"2000","unstructured":"Kovalyov, Andrei: A polynomial algorithm to compute the concurrency relation of a regular STG. Hardware design and Petri nets, Springer, Boston (2000)"},{"key":"694_CR22","unstructured":"LAAS-CNRS. Tina toolbox. (2020). http:\/\/projects.laas.fr\/tina"},{"key":"694_CR23","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"RJ Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18, 717\u2013721 (1975)","journal-title":"Commun. ACM"},{"issue":"4","key":"694_CR24","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T Murata","year":"1989","unstructured":"Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541\u2013580 (1989)","journal-title":"Proc. IEEE"},{"key":"694_CR25","unstructured":"Semenov, A., Yakovlev, A.: Combining partial orders and symbolic traversal for efficient verification of asynchronous circuits. In: Proceedings of ASP-DAC\u201995\/CHDL\u201995\/VLSI\u201995 with EDA Technofair (1995)"},{"key":"694_CR26","first-page":"309","volume-title":"Lectures on Petri nets I: basic models: advances in Petri nets","author":"M Silva","year":"1996","unstructured":"Silva, M., Terue, E., Colom, J.M.: Linear algebraic and linear programming techniques for the analysis of place\/transition net systems. In: Lectures on Petri nets I: basic models: advances in Petri nets, pp. 309\u2013373. Springer (1996)"},{"key":"694_CR27","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-030-51831-8_15","volume-title":"Application and theory of Petri nets and concurrency (Petri nets)","author":"Y Thierry-Mieg","year":"2020","unstructured":"Thierry-Mieg, Y.: Structural reductions revisited. In: Application and theory of Petri nets and concurrency (Petri nets), pp. 303\u2013323. Springer (2020)"},{"issue":"2","key":"694_CR28","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1109\/TCST.2017.2692204","volume":"26","author":"R Wisniewski","year":"2018","unstructured":"Wisniewski, R., Karatkevich, A., Adamski, M., Costa, A., Gomes, L.: Prototyping of Concurrent Control Systems with Application of Petri Nets and Comparability Graphs. IEEE Trans. Control Syst. Technol. 26(2), 575\u2013586 (2018)","journal-title":"IEEE Trans. Control Syst. Technol."},{"key":"694_CR29","doi-asserted-by":"publisher","first-page":"13510","DOI":"10.1109\/ACCESS.2019.2893284","volume":"7","author":"R Wi\u015bniewski","year":"2019","unstructured":"Wi\u015bniewski, R., Wi\u015bniewska, M., Jarnut, M.: C-exact hypergraphs in concurrency and sequentiality analyses of cyber-physical systems specified by safe Petri nets. IEEE Access 7, 13510\u201313522 (2019)","journal-title":"IEEE Access"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00694-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-022-00694-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00694-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,8]],"date-time":"2023-03-08T17:08:17Z","timestamp":1678295297000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-022-00694-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12,22]]},"references-count":29,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,2]]}},"alternative-id":["694"],"URL":"https:\/\/doi.org\/10.1007\/s10009-022-00694-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,12,22]]},"assertion":[{"value":"29 November 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 December 2022","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}