{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T19:22:32Z","timestamp":1776885752014,"version":"3.51.2"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031336195","type":"print"},{"value":"9783031336201","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"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":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-33620-1_20","type":"book-chapter","created":{"date-parts":[[2023,5,27]],"date-time":"2023-05-27T08:02:05Z","timestamp":1685174525000},"page":"369-392","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Symbolic Analysis and\u00a0Parameter Synthesis for\u00a0Time Petri Nets Using Maude and\u00a0SMT Solving"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3019-4902","authenticated-orcid":false,"given":"Jaime","family":"Arias","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6430-5175","authenticated-orcid":false,"given":"Kyungmin","family":"Bae","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7264-7773","authenticated-orcid":false,"given":"Carlos","family":"Olarte","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0708-3721","authenticated-orcid":false,"given":"Peter Csaba","family":"\u00d6lveczky","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3154-5268","authenticated-orcid":false,"given":"Laure","family":"Petrucci","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7545-4662","authenticated-orcid":false,"given":"Fredrik","family":"R\u00f8mming","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,5,28]]},"reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-642-00593-0_18","volume-title":"Fundamental Approaches to Software Engineering","author":"M AlTurki","year":"2009","unstructured":"AlTurki, M., Dhurjati, D., Yu, D., Chander, A., Inamura, H.: Formal specification and analysis of timing properties in software systems. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 262\u2013277. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00593-0_18"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-40229-6_1","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"\u00c9 Andr\u00e9","year":"2013","unstructured":"Andr\u00e9, \u00c9., Pellegrino, G., Petrucci, L.: Precise robustness analysis of time Petri nets with inhibitor arcs. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 1\u201315. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40229-6_1"},{"key":"20_CR3","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1016\/j.biosystems.2016.09.002","volume":"149","author":"A Andreychenko","year":"2016","unstructured":"Andreychenko, A., Magnin, M., Inoue, K.: Analyzing resilience properties in oscillatory biological systems using parametric model checking. Biosystems 149, 50\u201358 (2016)","journal-title":"Biosystems"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Arias, J., Bae, K., Olarte, C., \u00d6lveczky, P.C., Petrucci, L., R\u00f8mming, F.: Rewriting logic semantics and symbolic analysis for parametric timed automata. In: Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2022), pp. 3\u201315. ACM (2022)","DOI":"10.1145\/3563822.3569923"},{"key":"20_CR5","unstructured":"Arias, J., Bae, K., Olarte, C., \u00d6lveczky, P.C., Petrucci, L., R\u00f8mming, F.: PITPN2Maude (2023). https:\/\/depot.lipn.univ-paris13.fr\/arias\/pitpn2maude"},{"key":"20_CR6","doi-asserted-by":"publisher","unstructured":"Arias, J., Bae, K., Olarte, C., \u00d6lveczky, P.C., Petrucci, L., R\u00f8mming, F.: Symbolic analysis and parameter synthesis for time Petri nets using Maude and SMT solving (2023). https:\/\/doi.org\/10.48550\/ARXIV.2303.08929","DOI":"10.48550\/ARXIV.2303.08929"},{"key":"20_CR7","unstructured":"Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: Rewriting Techniques and Applications (RTA 2013). LIPIcs, vol. 21, pp. 81\u201396. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2013)"},{"key":"20_CR8","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/j.scico.2014.09.011","volume":"103","author":"K Bae","year":"2015","unstructured":"Bae, K., Krisiloff, J., Meseguer, J., \u00d6lveczky, P.C.: Designing and verifying distributed cyber-physical systems using Multirate PALS: an airplane turning control system case study. Sci. Comput. Program. 103, 13\u201350 (2015). https:\/\/doi.org\/10.1016\/j.scico.2014.09.011","journal-title":"Sci. Comput. Program."},{"issue":"12","key":"20_CR9","doi-asserted-by":"publisher","first-page":"1235","DOI":"10.1016\/j.scico.2010.10.002","volume":"77","author":"K Bae","year":"2012","unstructured":"Bae, K., \u00d6lveczky, P.C., Feng, T.H., Lee, E.A., Tripakis, S.: Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude. Sci. Comput. Program. 77(12), 1235\u20131271 (2012)","journal-title":"Sci. Comput. Program."},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-319-68034-7_5","volume-title":"Formal Aspects of Component Software","author":"K Bae","year":"2017","unstructured":"Bae, K., Rocha, C.: Guarded terms for rewriting modulo SMT. In: Proen\u00e7a, J., Lumpe, M. (eds.) FACS 2017. LNCS, vol. 10487, pp. 78\u201397. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68034-7_5"},{"key":"20_CR11","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1016\/j.scico.2019.03.006","volume":"178","author":"K Bae","year":"2019","unstructured":"Bae, K., Rocha, C.: Symbolic state space reduction with guarded terms for rewriting modulo SMT. Sci. Comput. Program. 178, 20\u201342 (2019)","journal-title":"Sci. Comput. Program."},{"key":"20_CR12","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-642-19170-1_28","volume-title":"Technological Innovation for Sustainability","author":"P Barbosa","year":"2011","unstructured":"Barbosa, P., et al.: SysVeritas: a framework for verifying IOPT nets and execution semantics within embedded systems design. In: Camarinha-Matos, L.M. (ed.) DoCEIS 2011. IAICT, vol. 349, pp. 256\u2013265. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19170-1_28"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Bobba, R., et al.: Survivability: design, formal modeling, and validation of cloud storage systems using Maude. In: Assured Cloud Computing, Chap. 2, pp. 10\u201348. Wiley (2018)","DOI":"10.1002\/9781119428497.ch2"},{"key":"20_CR14","doi-asserted-by":"publisher","unstructured":"Capra, L.: Canonization of reconfigurable PT nets in Maude. In: Lin, A.W., Zetzsche, G., Potapov, I. (eds.) Reachability Problems. RP 2022. LNCS, vol. 13608, pp. 160\u2013177. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19135-0_11","DOI":"10.1007\/978-3-031-19135-0_11"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-030-94876-4_9","volume-title":"Distributed Computing and Intelligent Technology","author":"L Capra","year":"2022","unstructured":"Capra, L.: Rewriting logic and\u00a0Petri nets: a natural model for\u00a0reconfigurable distributed systems. In: Bapi, R., Kulkarni, S., Mohalik, S., Peri, S. (eds.) ICDCIT 2022. LNCS, vol. 13145, pp. 140\u2013156. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94876-4_9"},{"key":"20_CR16","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6","volume-title":"Model Checking","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Amsterdam\/Cambridge (2001)"},{"key":"20_CR17","unstructured":"Clavel, M., et al.: Maude Manual (Version 3.2.1). SRI International (2022). http:\/\/maude.cs.illinois.edu"},{"key":"20_CR18","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M Clavel","year":"2007","unstructured":"Clavel, M., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-030-34968-4_7","volume-title":"Integrated Formal Methods","author":"H Coullon","year":"2019","unstructured":"Coullon, H., Jard, C., Lime, D.: Integrated model-checking for the design of safe and efficient distributed software commissioning. In: Ahrendt, W., Tapia Tarifa, S.L. (eds.) IFM 2019. LNCS, vol. 11918, pp. 120\u2013137. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-34968-4_7"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-642-15297-9_12","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"B Grabiec","year":"2010","unstructured":"Grabiec, B., Traonouez, L.-M., Jard, C., Lime, D., Roux, O.H.: Diagnosis using unfoldings of parametric time Petri nets. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 137\u2013151. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15297-9_12"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"494","DOI":"10.1007\/978-3-642-54624-2_25","volume-title":"Specification, Algebra, and Software","author":"J Grov","year":"2014","unstructured":"Grov, J., \u00d6lveczky, P.C.: Formal modeling and analysis of Google\u2019s Megastore in Real-Time Maude. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol. 8373, pp. 494\u2013519. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54624-2_25"},{"key":"20_CR22","doi-asserted-by":"publisher","unstructured":"Jensen, K., Kristensen, L.M.: Coloured Petri Nets - Modelling and Validation of Concurrent Systems. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/b95112","DOI":"10.1007\/b95112"},{"key":"20_CR23","doi-asserted-by":"publisher","unstructured":"Lee, J., Bae, K., \u00d6lveczky, P.C.: An extension of HybridSynchAADL and its application to collaborating autonomous UAVs. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning (ISoLA 2022). LNCS, vol. 13703, pp. 47\u201364. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19759-8_4","DOI":"10.1007\/978-3-031-19759-8_4"},{"issue":"6","key":"20_CR24","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1007\/s10009-022-00665-z","volume":"24","author":"J Lee","year":"2022","unstructured":"Lee, J., Bae, K., \u00d6lveczky, P.C., Kim, S., Kang, M.: Modeling and formal analysis of virtually synchronous cyber-physical systems in AADL. Int. J. Software Tools Technol. Transf. 24(6), 911\u2013948 (2022)","journal-title":"Int. J. Software Tools Technol. Transf."},{"key":"20_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-030-81685-8_23","volume-title":"Computer Aided Verification","author":"J Lee","year":"2021","unstructured":"Lee, J., Kim, S., Bae, K., \u00d6lveczky, P.C.: HybridSynchAADL: modeling and formal analysis of virtually synchronous CPSs in AADL. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 491\u2013504. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_23"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Lee, J., Kim, S., Bae, K.: Bounded model checking of PLC ST programs using rewriting modulo SMT. In: Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2022), pp. 56\u201367. ACM (2022)","DOI":"10.1145\/3563822.3568016"},{"key":"20_CR27","doi-asserted-by":"crossref","unstructured":"Lien, E., \u00d6lveczky, P.C.: Formal modeling and analysis of an IETF multicast protocol. In: Seventh IEEE International Conference on Software Engineering and Formal Methods (SEFM 2009), pp. 273\u2013282. IEEE Computer Society (2009)","DOI":"10.1109\/SEFM.2009.11"},{"key":"20_CR28","doi-asserted-by":"publisher","unstructured":"Lime, D., Roux, O.H., Seidner, C.: Cost problems for parametric time Petri nets. Fundam. Informaticae 183(1-2), 97\u2013123 (2021). https:\/\/doi.org\/10.3233\/FI-2021-2083","DOI":"10.3233\/FI-2021-2083"},{"key":"20_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-642-00768-2_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Lime","year":"2009","unstructured":"Lime, D., Roux, O.H., Seidner, C., Traonouez, L.-M.: Romeo: a parametric model-checker for Petri nets with stopwatches. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 54\u201357. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_6"},{"key":"20_CR30","unstructured":"Merlin, P.M.: A study of the recoverability of computing systems. Ph.D. thesis, University of California, Irvine, CA, USA (1974)"},{"issue":"1","key":"20_CR31","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theor. Comput. Sci."},{"issue":"7\u20138","key":"20_CR32","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/j.jlap.2012.06.003","volume":"81","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Log. Algebraic Methods Program. 81(7\u20138), 721\u2013781 (2012)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"20_CR33","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: Generalized rewrite theories, coherence completion, and symbolic methods. J. Log. Algebraic Methods Program. 110 (2020)","DOI":"10.1016\/j.jlamp.2019.100483"},{"issue":"2","key":"20_CR34","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/0890-5401(90)90013-8","volume":"88","author":"J Meseguer","year":"1990","unstructured":"Meseguer, J., Montanari, U.: Petri nets are monoids. Inform. Comput. 88(2), 105\u2013155 (1990)","journal-title":"Inform. Comput."},{"key":"20_CR35","doi-asserted-by":"publisher","unstructured":"Nigam, V., Talcott, C.L.: Automating safety proofs about cyber-physical systems using rewriting modulo SMT. In: Bae, K. (ed.) Rewriting Logic and Its Applications (WRLA 2022). LNCS, vol. 13252, pp. 212\u2013229. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-12441-9_11","DOI":"10.1007\/978-3-031-12441-9_11"},{"key":"20_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-642-24933-4_19","volume-title":"Formal Modeling: Actors, Open Systems, Biological Systems","author":"PC \u00d6lveczky","year":"2011","unstructured":"\u00d6lveczky, P.C.: Semantics, simulation, and formal analysis of modeling languages for embedded systems in Real-Time Maude. In: Agha, G., Danvy, O., Meseguer, J. (eds.) Formal Modeling: Actors, Open Systems, Biological Systems. LNCS, vol. 7000, pp. 368\u2013402. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24933-4_19"},{"key":"20_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-319-12904-4_3","volume-title":"Rewriting Logic and Its Applications","author":"PC \u00d6lveczky","year":"2014","unstructured":"\u00d6lveczky, P.C.: Real-Time Maude and its applications. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 42\u201379. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12904-4_3"},{"key":"20_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-642-13464-7_5","volume-title":"Formal Techniques for Distributed Systems","author":"PC \u00d6lveczky","year":"2010","unstructured":"\u00d6lveczky, P.C., Boronat, A., Meseguer, J.: Formal semantics and analysis of behavioral AADL models in Real-Time Maude. In: Hatcliff, J., Zucca, E. (eds.) FMOODS\/FORTE -2010. LNCS, vol. 6117, pp. 47\u201362. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13464-7_5"},{"key":"20_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/11693017_26","volume-title":"Fundamental Approaches to Software Engineering","author":"PC \u00d6lveczky","year":"2006","unstructured":"\u00d6lveczky, P.C., Caccamo, M.: Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude. In: Baresi, L., Heckel, R. (eds.) FASE 2006. LNCS, vol. 3922, pp. 357\u2013372. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11693017_26"},{"issue":"2","key":"20_CR40","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1016\/S0304-3975(01)00363-2","volume":"285","author":"PC \u00d6lveczky","year":"2002","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Specification of real-time and hybrid systems in rewriting logic. Theor. Comput. Sci. 285(2), 359\u2013405 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"20_CR41","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Abstraction and completeness for Real-Time Maude. In: 6th International Workshop on Rewriting Logic and its Applications (WRLA 2006). Electronic Notes in Theoretical Computer Science, vol. 174, pp. 5\u201327. Elsevier (2006)","DOI":"10.1016\/j.entcs.2007.06.005"},{"issue":"1\u20132","key":"20_CR42","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10990-007-9001-5","volume":"20","author":"PC \u00d6lveczky","year":"2007","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. High. Order Symb. Comput. 20(1\u20132), 161\u2013196 (2007)","journal-title":"High. Order Symb. Comput."},{"key":"20_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-540-78800-3_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PC \u00d6lveczky","year":"2008","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: The Real-Time Maude tool. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 332\u2013336. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_23"},{"issue":"3","key":"20_CR44","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/s10703-006-0015-0","volume":"29","author":"PC \u00d6lveczky","year":"2006","unstructured":"\u00d6lveczky, P.C., Meseguer, J., Talcott, C.L.: Specification and analysis of the AER\/NCA active network protocol suite in Real-Time Maude. Formal Methods Syst. Des. 29(3), 253\u2013293 (2006)","journal-title":"Formal Methods Syst. Des."},{"key":"20_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-319-40530-8_4","volume-title":"Graph Transformation","author":"J Padberg","year":"2016","unstructured":"Padberg, J., Schulz, A.: Model checking reconfigurable Petri nets with Maude. In: Echahed, R., Minas, M. (eds.) ICGT 2016. LNCS, vol. 9761, pp. 54\u201370. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40530-8_4"},{"key":"20_CR46","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-319-53946-1_8","volume-title":"Formal Techniques for Safety-Critical Systems","author":"B Parquier","year":"2017","unstructured":"Parquier, B., et al.: Applying parametric model-checking techniques for reusing real-time critical systems. In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS 2016. CCIS, vol. 694, pp. 129\u2013144. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-53946-1_8"},{"issue":"1","key":"20_CR47","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/j.jlamp.2016.10.001","volume":"86","author":"C Rocha","year":"2017","unstructured":"Rocha, C., Meseguer, J., Mu\u00f1oz, C.A.: Rewriting modulo SMT and open system analysis. J. Log. Algebraic Methods Program. 86(1), 269\u2013297 (2017)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"20_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45541-8_9","volume-title":"Unifying Petri Nets","author":"M-O Stehr","year":"2001","unstructured":"Stehr, M.-O., Meseguer, J., \u00d6lveczky, P.C.: Rewriting logic as a unifying framework for Petri nets. In: Ehrig, H., Padberg, J., Juh\u00e1s, G., Rozenberg, G. (eds.) Unifying Petri Nets. LNCS, vol. 2128, pp. 250\u2013303. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45541-8_9"},{"key":"20_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-85778-5_20","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"L-M Traonouez","year":"2008","unstructured":"Traonouez, L.-M., Lime, D., Roux, O.H.: Parametric model-checking of time Petri nets with stopwatches using the state-class graph. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 280\u2013294. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85778-5_20"},{"issue":"17","key":"20_CR50","first-page":"3273","volume":"15","author":"L Traonouez","year":"2009","unstructured":"Traonouez, L., Lime, D., Roux, O.H.: Parametric model-checking of stopwatch Petri nets. J. Univers. Comput. Sci. 15(17), 3273\u20133304 (2009)","journal-title":"J. Univers. Comput. Sci."},{"key":"20_CR51","doi-asserted-by":"crossref","unstructured":"Vernadat, F., Berthomieu, B.: State space abstractions for time Petri nets. In: Son, S.H., Lee, I., Leung, J.Y. (eds.) Handbook of Real-Time and Embedded Systems. Chapman and Hall\/CRC (2007)","DOI":"10.1201\/9781420011746.pt6"},{"key":"20_CR52","doi-asserted-by":"crossref","unstructured":"Wang, J.: Time Petri nets. In: Timed Petri Nets: Theory and Application, pp. 63\u2013123. Springer, Cham (1998)","DOI":"10.1007\/978-1-4615-5537-7_4"},{"key":"20_CR53","unstructured":"Yu, G., Bae, K.: Maude-SE: a tight integration of Maude and SMT solvers. In: Preliminary Proceedings of WRLA@ETAPS, pp. 220\u2013232 (2020)"}],"container-title":["Lecture Notes in Computer Science","Application and Theory of Petri Nets and Concurrency"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-33620-1_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,17]],"date-time":"2023-06-17T23:09:39Z","timestamp":1687043379000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-33620-1_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031336195","9783031336201"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-33620-1_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"28 May 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"PETRI NETS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Applications and Theory of Petri Nets and Concurrency","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 June 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 June 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"44","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"apn2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/petrinets2023.deec.fct.unl.pt\/","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":"47","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":"21","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":"0","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":"45% - 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":"4","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":"5","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)"}}]}}