{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T01:12:31Z","timestamp":1770340351797,"version":"3.49.0"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,1,29]],"date-time":"2024-01-29T00:00:00Z","timestamp":1706486400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,1,29]],"date-time":"2024-01-29T00:00:00Z","timestamp":1706486400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100009890","name":"Provincia Autonoma di Trento","doi-asserted-by":"publisher","award":["AI@TN"],"award-info":[{"award-number":["AI@TN"]}],"id":[{"id":"10.13039\/501100009890","id-type":"DOI","asserted-by":"publisher"}]},{"name":"NextGenerationEU","award":["FAIR - Future AI Research (PE00000013)"],"award-info":[{"award-number":["FAIR - Future AI Research (PE00000013)"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2024,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Stability is a fundamental requirement of dynamical systems. Most of the works concentrate on verifying stability for a given stability region. In this paper, we tackle the problem of <jats:italic>synthesizing<\/jats:italic><jats:inline-formula><jats:alternatives><jats:tex-math>$${\\mathbb {P}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>P<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-<jats:italic>stable abstractions<\/jats:italic>. Intuitively, the <jats:inline-formula><jats:alternatives><jats:tex-math>$${\\mathbb {P}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>P<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-stable abstraction of a dynamical system characterizes the transitions between stability regions in response to external inputs. The stability regions are not given\u2014rather, they are synthesized as their most precise representation with respect to a given set of predicates <jats:inline-formula><jats:alternatives><jats:tex-math>$${\\mathbb {P}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>P<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>. A <jats:inline-formula><jats:alternatives><jats:tex-math>$${\\mathbb {P}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>P<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-stable abstraction is enriched by timing information derived from the duration of stabilization. We implement a synthesis algorithm in the framework of Abstract Interpretation that allows different degrees of approximation. We show the representational power of <jats:inline-formula><jats:alternatives><jats:tex-math>$${\\mathbb {P}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>P<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-stable abstractions that provide a high-level account of the behavior of the system with respect to stability, and we experimentally evaluate the effectiveness of the algorithm in synthesizing <jats:inline-formula><jats:alternatives><jats:tex-math>$${\\mathbb {P}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>P<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-stable abstractions for significant systems.<\/jats:p>","DOI":"10.1007\/s10270-023-01145-x","type":"journal-article","created":{"date-parts":[[2024,1,29]],"date-time":"2024-01-29T05:02:00Z","timestamp":1706504520000},"page":"403-426","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["P-stable abstractions of hybrid systems"],"prefix":"10.1007","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2831-9529","authenticated-orcid":false,"given":"Anna","family":"Becchi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1315-6990","authenticated-orcid":false,"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6388-2053","authenticated-orcid":false,"given":"Enea","family":"Zaffanella","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,1,29]]},"reference":[{"issue":"2","key":"1145_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theor. Comput. Sci."},{"key":"1145_CR2","doi-asserted-by":"publisher","unstructured":"Alur, R., Dang, T., Ivancic, F.: Reachability analysis of hybrid systems via predicate abstraction. In: Tomlin, C.J., Greenstreet, M.R. (eds) Hybrid Systems: Computation and Control, 5th International Workshop, HSCC 2002, Stanford, CA, USA, March 25\u201327, 2002, Proceedings, Lecture Notes in Computer Science, vol 2289. Springer, pp 35\u201348, (2002) https:\/\/doi.org\/10.1007\/3-540-45873-5_6","DOI":"10.1007\/3-540-45873-5_6"},{"key":"1145_CR3","doi-asserted-by":"publisher","unstructured":"Alur, R., Dang, T., Ivancic, F.: Counter-example guided predicate abstraction of hybrid systems. In: Garavel, H., Hatcliff, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7\u201311, 2003, Proceedings, Lecture Notes in Computer Science, vol 2619. Springer, pp 208\u2013223, (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_15","DOI":"10.1007\/3-540-36577-X_15"},{"key":"1145_CR4","doi-asserted-by":"publisher","unstructured":"Amendola, A., Becchi, A., Cavada, R., et\u00a0al.: A model-based approach to the design, verification and deployment of railway interlocking system. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20\u201330, 2020, Proceedings, Part III, Lecture Notes in Computer Science, vol 12478. Springer, pp 240\u2013254, (2020). https:\/\/doi.org\/10.1007\/978-3-030-61467-6_16","DOI":"10.1007\/978-3-030-61467-6_16"},{"key":"1145_CR5","doi-asserted-by":"publisher","unstructured":"Amendola, A., Becchi, A., Cavada, R., et\u00a0al.: NORMA: a tool for the analysis of relay-based railway interlocking systems. In: Fisman, D., Rosu, G. (eds) Tools and Algorithms for the Construction and Analysis of Systems\u201328th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2\u20137, 2022, Proceedings, Part I, Lecture Notes in Computer Science, vol 13243. Springer, pp. 125\u2013142 (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_7","DOI":"10.1007\/978-3-030-99524-9_7"},{"issue":"1","key":"1145_CR6","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/s10009-002-0095-0","volume":"5","author":"T Ball","year":"2003","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstraction for model checking C programs. Int. J. Softw. Tools Technol. Transf. 5(1), 49\u201358 (2003). https:\/\/doi.org\/10.1007\/s10009-002-0095-0","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1145_CR7","doi-asserted-by":"publisher","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., et\u00a0al.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., et\u00a0al (eds) Handbook of Satisfiability\u2013Second Edition, Frontiers in Artificial Intelligence and Applications, vol 336. IOS Press, pp. 1267\u20131329 (2021). https:\/\/doi.org\/10.3233\/FAIA201017","DOI":"10.3233\/FAIA201017"},{"key":"1145_CR8","doi-asserted-by":"publisher","unstructured":"Becchi, A., Cimatti, A.: Abstraction modulo stability for reverse engineering. In: Shoham, S., Vizel, Y. (eds) Computer Aided Verification\u201334th International Conference, CAV 2022, Haifa, Israel, August 7\u201310, 2022, Proceedings, Part I, Lecture Notes in Computer Science, vol. 13371. Springer, pp 469\u2013489 (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_23","DOI":"10.1007\/978-3-031-13185-1_23"},{"key":"1145_CR9","doi-asserted-by":"publisher","unstructured":"Becchi, A., Zaffanella, E.: An efficient abstract domain for not necessarily closed polyhedra. In: Podelski, A. (ed) Static Analysis\u201325th International Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018, Proceedings, Lecture Notes in Computer Science, vol. 11002. Springer, pp. 146\u2013165 (2018). https:\/\/doi.org\/10.1007\/978-3-319-99725-4_11","DOI":"10.1007\/978-3-319-99725-4_11"},{"key":"1145_CR10","doi-asserted-by":"publisher","unstructured":"Becchi, A., Zaffanella, E.: Revisiting polyhedral analysis for hybrid systems. In: Chang, B.E. (ed) Static Analysis\u201326th International Symposium, SAS 2019, Porto, Portugal, October 8\u201311, 2019, Proceedings, Lecture Notes in Computer Science, vol 11822. Springer, pp. 183\u2013202 (2019). https:\/\/doi.org\/10.1007\/978-3-030-32304-2_10","DOI":"10.1007\/978-3-030-32304-2_10"},{"issue":"104","key":"1145_CR11","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1016\/j.ic.2020.104620","volume":"275","author":"A Becchi","year":"2020","unstructured":"Becchi, A., Zaffanella, E.: PPLite: Zero-overhead encoding of NNC polyhedra. Inf. Comput. 275(104), 620 (2020). https:\/\/doi.org\/10.1016\/j.ic.2020.104620","journal-title":"Inf. Comput."},{"key":"1145_CR12","doi-asserted-by":"publisher","unstructured":"Becchi, A., Cimatti, A., Zaffanella, E.: Synthesis of P-stable abstractions. In: de\u00a0Boer, F.S., Cerone, A. (eds.) Software Engineering and Formal Methods\u201318th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14-18, 2020, Proceedings, Lecture Notes in Computer Science, vol. 12310. Springer, pp. 214\u2013230 (2020). https:\/\/doi.org\/10.1007\/978-3-030-58768-0_12","DOI":"10.1007\/978-3-030-58768-0_12"},{"key":"1145_CR13","unstructured":"Becchi, A., Cimatti, A., Zaffanella, E.: Reverse engineering with P-stable abstractions. In: Monica, D.D., Pozzato, G.L., Scala, E. (eds) Proceedings of the 3rd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis hosted by the Twelfth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2021), Padua, Italy, September 22, 2021, CEUR Workshop Proceedings, vol 2987. CEUR-WS.org, pp 91\u201395 (2021). https:\/\/ceur-ws.org\/Vol-2987\/paper16.pdf"},{"key":"1145_CR14","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1016\/j.tcs.2012.10.042","volume":"493","author":"M Benerecetti","year":"2013","unstructured":"Benerecetti, M., Faella, M., Minopoli, S.: Automatic synthesis of switching controllers for linear hybrid systems: Safety control. Theor. Comput. Sci. 493, 116\u2013138 (2013). https:\/\/doi.org\/10.1016\/j.tcs.2012.10.042","journal-title":"Theor. Comput. Sci."},{"key":"1145_CR15","unstructured":"Birkhoff, G.: Lattice Theory, Colloquium Publications, vol. XXV, 3rd edn. American Mathematical Society, Providence, Rhode Island, USA (1967)"},{"key":"1145_CR16","doi-asserted-by":"publisher","unstructured":"Blanchet, B., Cousot, P., Cousot, R., et\u00a0al.: A static analyzer for large safety-critical software. In: Cytron, R., Gupta, R. (eds) Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003, San Diego, California, USA, June 9\u201311, 2003. ACM, pp 196\u2013207 (2003). https:\/\/doi.org\/10.1145\/781131.781153","DOI":"10.1145\/781131.781153"},{"key":"1145_CR17","doi-asserted-by":"publisher","unstructured":"Bogomolov, S., Mitrohin, C., Podelski, A.: Composing reachability analyses of hybrid systems for safety and stability. In: Bouajjani, A., Chin, W. (eds) Automated Technology for Verification and Analysis - 8th International Symposium, ATVA 2010, Singapore, September 21\u201324, 2010. Proceedings, Lecture Notes in Computer Science, vol 6252. Springer, pp 67\u201381 (2010). https:\/\/doi.org\/10.1007\/978-3-642-15643-4_7","DOI":"10.1007\/978-3-642-15643-4_7"},{"key":"1145_CR18","doi-asserted-by":"publisher","unstructured":"Branicky, M.: Stability of hybrid systems: State of the art. pp 120 \u2013 125 vol.1 (1998). https:\/\/doi.org\/10.1109\/CDC.1997.650600","DOI":"10.1109\/CDC.1997.650600"},{"key":"1145_CR19","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1109\/TCS.1979.1084637","volume":"26","author":"R Brayton","year":"1979","unstructured":"Brayton, R., Tong, C.: Stability of dynamical systems: A constructive approach. Circ. Syst. IEEE Trans. CAS 26, 224\u2013234 (1979). https:\/\/doi.org\/10.1109\/TCS.1979.1084637","journal-title":"Circ. Syst. IEEE Trans. CAS"},{"key":"1145_CR20","doi-asserted-by":"publisher","unstructured":"Cavada, R., Cimatti, A., Mover, S., et\u00a0al.: Analysis of relay interlocking systems via SMT-based model checking of switched multi-domain Kirchhoff networks. In: Bj\u00f8rner, N.S., Gurfinkel, A. (eds) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30\u2013November 2, 2018. IEEE, pp. 1\u20139 (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603007","DOI":"10.23919\/FMCAD.2018.8603007"},{"key":"1145_CR21","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Mover, S., Tonetta, S.: Hydi: A language for symbolic hybrid systems with discrete interaction. In: 37th EUROMICRO Conference on Software Engineering and Advanced Applications, SEAA 2011, Oulu, Finland, August 30\u2013September 2, 2011. IEEE Computer Society, pp. 275\u2013278 (2011). https:\/\/doi.org\/10.1109\/SEAA.2011.49","DOI":"10.1109\/SEAA.2011.49"},{"key":"1145_CR22","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Magnago, E., et\u00a0al.: Extending nuXmv with timed transition systems and timed temporal properties. In: Dillig, I., Tasiran, S. (eds) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15\u201318, 2019, Proceedings, Part I, Lecture Notes in Computer Science, vol 11561. Springer, pp 376\u2013386 (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_21","DOI":"10.1007\/978-3-030-25540-4_21"},{"key":"1145_CR23","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977. ACM, pp. 238\u2013252 (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"1145_CR24","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Comparing the galois connection and widening\/narrowing approaches to abstract interpretation. In: Bruynooghe M, Wirsing M (eds) Programming Language Implementation and Logic Programming, 4th International Symposium, PLILP\u201992, Leuven, Belgium, August 26\u201328, 1992, Proceedings, Lecture Notes in Computer Science, vol 631. Springer, pp. 269\u2013295, (1992). https:\/\/doi.org\/10.1007\/3-540-55844-6_142","DOI":"10.1007\/3-540-55844-6_142"},{"issue":"1","key":"1145_CR25","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1023\/A:1008649901864","volume":"6","author":"P Cousot","year":"1999","unstructured":"Cousot, P., Cousot, R.: Refining model checking by abstract interpretation. Autom. Softw. Eng. 6(1), 69\u201395 (1999). https:\/\/doi.org\/10.1023\/A:1008649901864","journal-title":"Autom. Softw. Eng."},{"key":"1145_CR26","doi-asserted-by":"publisher","unstructured":"Frehse, G.: Phaver: Algorithmic verification of hybrid systems past hytech. In: Morari M, Thiele L (eds) Hybrid Systems: Computation and Control, 8th International Workshop, HSCC 2005, Zurich, Switzerland, March 9-11, 2005, Proceedings, Lecture Notes in Computer Science, vol 3414. Springer, pp. 258\u2013273 (2005). https:\/\/doi.org\/10.1007\/978-3-540-31954-2_17","DOI":"10.1007\/978-3-540-31954-2_17"},{"issue":"4","key":"1145_CR27","doi-asserted-by":"publisher","first-page":"1663","DOI":"10.1137\/140988802","volume":"14","author":"P Giesl","year":"2015","unstructured":"Giesl, P., Hafstein, S.F.: Computation and verification of Lyapunov functions. SIAM J. Appl. Dyn. Syst. 14(4), 1663\u20131698 (2015). https:\/\/doi.org\/10.1137\/140988802","journal-title":"SIAM J. Appl. Dyn. Syst."},{"key":"1145_CR28","doi-asserted-by":"publisher","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg O (ed) Computer Aided Verification, 9th International Conference, CAV \u201997, Haifa, Israel, June 22-25, 1997, Proceedings, Lecture Notes in Computer Science, vol 1254. Springer, pp. 72\u201383 (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_10","DOI":"10.1007\/3-540-63166-6_10"},{"key":"1145_CR29","doi-asserted-by":"publisher","unstructured":"Halbwachs, N., Proy, Y., Raymond, P.: Verification of linear hybrid systems by means of convex approximations. In: Charlier BL (ed) Static Analysis, First International Static Analysis Symposium, SAS\u201994, Namur, Belgium, September 28-30, 1994, Proceedings, Lecture Notes in Computer Science, vol 864. Springer, pp. 223\u2013237 (1994). https:\/\/doi.org\/10.1007\/3-540-58485-4_43","DOI":"10.1007\/3-540-58485-4_43"},{"key":"1145_CR30","doi-asserted-by":"publisher","unstructured":"Lahiri, S.K., Bryant, R.E., Cook, B.: A symbolic approach to predicate abstraction. In: Jr. WAH, Somenzi F (eds) Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings, Lecture Notes in Computer Science, vol 2725. Springer, pp. 141\u2013153 (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_15","DOI":"10.1007\/978-3-540-45069-6_15"},{"key":"1145_CR31","doi-asserted-by":"publisher","unstructured":"Liberzon, D.: Switching in Systems and Control. Systems & Control: Foundations & Applications, Birkh\u00e4user (2003). https:\/\/doi.org\/10.1007\/978-1-4612-0017-8","DOI":"10.1007\/978-1-4612-0017-8"},{"key":"1145_CR32","unstructured":"Milner, R.: Communication and concurrency. PHI Series in computer science, Prentice Hall (1989)"},{"key":"1145_CR33","doi-asserted-by":"publisher","unstructured":"Mitra, S., Liberzon, D.: Stability of hybrid automata with average dwell time: an invariant approach. In: 43rd IEEE Conference on Decision and Control, CDC 2004, Nassau, Bahamas, December 14\u201317, 2004. IEEE, pp. 1394\u20131399 (2004). https:\/\/doi.org\/10.1109\/CDC.2004.1430238","DOI":"10.1109\/CDC.2004.1430238"},{"key":"1145_CR34","doi-asserted-by":"publisher","unstructured":"Podelski, A., Wagner, S.: Model checking of hybrid systems: From reachability towards stability. In: Hespanha, J.P., Tiwari, A. (eds) Hybrid Systems: Computation and Control, 9th International Workshop, HSCC 2006, Santa Barbara, CA, USA, March 29-31, 2006, Proceedings, Lecture Notes in Computer Science, vol. 3927. Springer, pp. 507\u2013521, (2006). https:\/\/doi.org\/10.1007\/11730637_38","DOI":"10.1007\/11730637_38"},{"key":"1145_CR35","doi-asserted-by":"publisher","unstructured":"Podelski, A., Wagner, S.: Region stability proofs for hybrid systems. In: Raskin, J., Thiagarajan, P.S. (eds) Formal Modeling and Analysis of Timed Systems, 5th International Conference, FORMATS 2007, Salzburg, Austria, October 3\u20135, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4763. Springer, pp 320\u2013335 (2007). https:\/\/doi.org\/10.1007\/978-3-540-75454-1_23","DOI":"10.1007\/978-3-540-75454-1_23"},{"key":"1145_CR36","doi-asserted-by":"publisher","unstructured":"Schupp, S., \u00c1brah\u00e1m, E., Chen, X., et\u00a0al.: Current challenges in the verification of hybrid systems. In: Berger, C., Mousavi, M.R. (eds) Cyber Physical Systems. Design, Modeling, and Evaluation - 5th International Workshop, CyPhy 2015, Amsterdam, The Netherlands, October 8, 2015, Proceedings, Lecture Notes in Computer Science, vol. 9361. Springer, pp. 8\u201324 (2015). https:\/\/doi.org\/10.1007\/978-3-319-25141-7_2","DOI":"10.1007\/978-3-319-25141-7_2"},{"key":"1145_CR37","unstructured":"Somenzi, F.: CUDD: CU Decision Diagram Package Release (1998)"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-023-01145-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-023-01145-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-023-01145-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,13]],"date-time":"2024-05-13T12:05:43Z","timestamp":1715601943000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-023-01145-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,29]]},"references-count":37,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,4]]}},"alternative-id":["1145"],"URL":"https:\/\/doi.org\/10.1007\/s10270-023-01145-x","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,29]]},"assertion":[{"value":"1 July 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 November 2023","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 December 2023","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 January 2024","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}