{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T09:06:32Z","timestamp":1784797592311,"version":"3.55.0"},"publisher-location":"Cham","reference-count":51,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325259","type":"print"},{"value":"9783032325266","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>In many verification tasks, system models do not correspond to the focused and idealized models that appear in research literature. In practice, models usually contain components and execution paths that are irrelevant to the property being verified or have only a limited effect on it. Compositional verification presents a practical method for coping with the larger and less targeted models found in such settings. In this paper, we present an automated compositional framework for verifying timed safety properties in networks of timed automata. We show as a main result that the weakest environment assumption, commonly used in compositional reasoning, may in general fail to be recognizable within the timed automata formalism. This negative result motivates shifting the focus to the complement language of violation-inducing timed words, for which we establish recognizability using timed automata with silent transitions. We provide an algorithm for its construction and reduce its size by retaining only the parts directly relevant to the property. The synthesized assumption is later applied to verify the original system. This provides a sound and complete basis for compositional verification of timed automata, including the novel ability to handle automata with multiple clocks and non-deterministic behavior. Our results broaden the applicability of assume\u2013guarantee verification techniques in timed automata and show substantial reductions in the size of the state-space, outperforming monolithic methods on a range of case studies.<\/jats:p>","DOI":"10.1007\/978-3-032-32526-6_16","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:46:31Z","timestamp":1784796391000},"page":"331-355","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Compositional Verification of\u00a0Timed Automata via\u00a0Violation Assumptions"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-9208-0659","authenticated-orcid":false,"given":"Mehran","family":"Moeini Jam","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-3123-3450","authenticated-orcid":false,"given":"Hamed","family":"Kalantari","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5278-5442","authenticated-orcid":false,"given":"Ehsan","family":"Khamespanah","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5478-0987","authenticated-orcid":false,"given":"Marjan","family":"Sirjani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6803-6750","authenticated-orcid":false,"given":"Ali","family":"Movaghar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Lamport, L.: An old-fashioned recipe for real time. ACM Trans. Program. Lang. Syst. 16(5), 1543\u20131571 (1994). https:\/\/doi.org\/10.1145\/186025.186058","DOI":"10.1145\/186025.186058"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Abbasi, R., Ghassemi, F., Khosravi, R.: Verification of asynchronous systems with an unspecified component. Acta Informatica 56(2), 161\u2013203 (2019). https:\/\/doi.org\/10.1007\/s00236-018-0317-x","DOI":"10.1007\/s00236-018-0317-x"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117\u2013126 (1987). https:\/\/doi.org\/10.1007\/BF01782772","DOI":"10.1007\/BF01782772"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L., Halbwachs, N., Wong-Toi, H.: An implementation of three algorithms for timing verification based on automata emptiness. In: Proceedings of the Real-Time Systems Symposium - 1992, Phoenix, Arizona, USA, December 1992, pp. 157\u2013166. IEEE Computer Society (1992). https:\/\/doi.org\/10.1109\/REAL.1992.242667","DOI":"10.1109\/REAL.1992.242667"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/BFb0032042","volume-title":"Automata, Languages and Programming","author":"R Alur","year":"1990","unstructured":"Alur, R., Dill, D.: Automata for modeling real-time systems. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322\u2013335. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0032042"},{"key":"16_CR6","doi-asserted-by":"crossref","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","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Alur, R., Fix, L., Henzinger, T.A.: Event-clock automata: a determinizable class of timed automata. Theor. Comput. Sci. 211(1-2), 253\u2013273 (1999). https:\/\/doi.org\/10.1016\/S0304-3975(97)00173-4","DOI":"10.1016\/S0304-3975(97)00173-4"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87\u2013106 (1987). https:\/\/doi.org\/10.1016\/0890-5401(87)90052-6","DOI":"10.1016\/0890-5401(87)90052-6"},{"key":"16_CR9","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press (2008)"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-75632-5_1","volume-title":"Lectures on Runtime Verification","author":"E Bartocci","year":"2018","unstructured":"Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 1\u201333. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_1"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Bouyer, P., Larsen, K.G., Pel\u00e1nek, R.: Lower and upper bounds in zone-based abstractions of timed automata. Int. J. Softw. Tools Technol. Transf. 8(3), 204\u2013215 (2006). https:\/\/doi.org\/10.1007\/S10009-005-0190-0","DOI":"10.1007\/s10009-005-0190-0"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Behrmann, G., et al.: UPPAAL 4.0. In: Third International Conference on the Quantitative Evaluation of Systems (QEST 2006), Riverside, California, USA, 11\u201314 September 2006, pp. 125\u2013126. IEEE Computer Society (2006). https:\/\/doi.org\/10.1109\/QEST.2006.59","DOI":"10.1109\/QEST.2006.59"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"B\u00e9rard, B., Petit, A., Diekert, V., Gastin, P.: Characterization of the expressive power of silent transitions in timed automata. Fundam. Informaticae 36(2-3), 145\u2013182 (1998). https:\/\/doi.org\/10.3233\/FI-1998-36233","DOI":"10.3233\/FI-1998-36233"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Bouyer, P.: Timed automata. In: Pin, J. (ed.) Handbook of Automata Theory, pp. 1261\u20131294. European Mathematical Society Publishing House, Z\u00fcrich, Switzerland (2021). https:\/\/doi.org\/10.4171\/AUTOMATA-2\/12","DOI":"10.4171\/automata-2\/12"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Bouyer, P., Gastin, P., Herbreteau, F., Sankur, O., Srivathsan, B.: Zone-based verification of timed automata: extrapolations, simulations and what next? In: Bogomolov, S., Parker, D. (eds.) Formal Modeling and Analysis of Timed Systems - 20th International Conference, FORMATS 2022, Warsaw, Poland, 13\u201315 September 2022, Proceedings, pp. 16\u201342. LNCS. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-15839-1_2","DOI":"10.1007\/978-3-031-15839-1_2"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Bouyer, P., Haddad, S., Reynier, P.: Undecidability results for timed automata with silent transitions. Fundam. Informaticae 92(1-2), 1\u201325 (2009). https:\/\/doi.org\/10.3233\/FI-2009-0063","DOI":"10.3233\/FI-2009-0063"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/BFb0028779","volume-title":"Computer Aided Verification","author":"M Bozga","year":"1998","unstructured":"Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: a model-checking tool for real-time systems. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 546\u2013550. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0028779"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Chen, H., Su, Y., Zhang, M., Liu, Z., Mi, J.: Learning assumptions for compositional verification of timed automata. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, 17\u201322 July 2023, Proceedings, Part I. LNCS, pp. 40\u201361. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_3","DOI":"10.1007\/978-3-031-37706-8_3"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Cheng, A.M.K.: Real-Time Systems - Scheduling, Analysis, and Verification. Wiley (2002)","DOI":"10.1002\/0471224626"},{"key":"16_CR21","unstructured":"Clarke, E.M., Grumberg, O., Kroening, D., Peled, D.A., Veith, H.: Model Checking, 2nd edn. MIT Press (2018). https:\/\/mitpress.mit.edu\/books\/model-checking-second-edition"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35746-6_1","volume-title":"Tools for Practical Software Verification","author":"EM Clarke","year":"2012","unstructured":"Clarke, E.M., Klieber, W., Nov\u00e1\u010dek, M., Zuliani, P.: Model checking and the state explosion problem. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol. 7682, pp. 1\u201330. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35746-6_1"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Cobleigh, J.M., Avrunin, G.S., Clarke, L.A.: Breaking up is hard to do: an investigation of decomposition for assume-guarantee reasoning. In: Pollock, L.L., Pezz\u00e8, M. (eds.) Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2006, Portland, Maine, USA, 17\u201320 July 2006, pp. 97\u2013108. ACM (2006). https:\/\/doi.org\/10.1145\/1146238.1146250","DOI":"10.1145\/1146238.1146250"},{"key":"16_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-36577-X_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JM Cobleigh","year":"2003","unstructured":"Cobleigh, J.M., Giannakopoulou, D., P\u0102s\u0102reanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331\u2013346. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_24"},{"key":"16_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-78800-3_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Farzan","year":"2008","unstructured":"Farzan, A., Chen, Y.-F., Clarke, E.M., Tsay, Y.-K., Wang, B.-Y.: Extending\u00a0automated\u00a0compositional\u00a0verification to the full class of omega-regular languages. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 2\u201317. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_2"},{"key":"16_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-642-24372-1_40","volume-title":"Automated Technology for Verification and Analysis","author":"L Feng","year":"2011","unstructured":"Feng, L., Han, T., Kwiatkowska, M., Parker, D.: Learning-based compositional verification for synchronous probabilistic systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 511\u2013521. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24372-1_40"},{"key":"16_CR27","doi-asserted-by":"publisher","unstructured":"Giannakopoulou, D., Namjoshi, K.S., P\u0103s\u0103reanu, C.S.: Compositional reasoning. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 345\u2013383. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_12","DOI":"10.1007\/978-3-319-10575-8_12"},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Pasareanu, C.S., Barringer, H.: Component verification with automatically generated assumptions. Autom. Softw. Eng. 12(3), 297\u2013320 (2005). https:\/\/doi.org\/10.1007\/S10515-005-2641-Y","DOI":"10.1007\/s10515-005-2641-y"},{"key":"16_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69850-0","volume-title":"25 Years of Model Checking","year":"2008","unstructured":"Grumberg, O., Veith, H. (eds.): 25 Years of Model Checking. LNCS, vol. 5000. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-69850-0"},{"key":"16_CR30","doi-asserted-by":"crossref","unstructured":"Havelund, K., Rosu, G.: Monitoring programs using rewriting. In: 16th IEEE International Conference on Automated Software Engineering (ASE 2001), Coronado Island, San Diego, CA, USA, 26\u201329 November 2001, pp. 135\u2013143. IEEE Computer Society (2001). https:\/\/doi.org\/10.1109\/ASE.2001.989799","DOI":"10.1109\/ASE.2001.989799"},{"key":"16_CR31","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. 111(2), 193\u2013244 (1994). https:\/\/doi.org\/10.1006\/INCO.1994.1045","DOI":"10.1006\/inco.1994.1045"},{"key":"16_CR32","unstructured":"Herbreteau, F., Point, G.: The TChecker tool and libraries. https:\/\/github.com\/ticktac-project\/tchecker"},{"key":"16_CR33","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969). https:\/\/doi.org\/10.1145\/363235.363259","DOI":"10.1145\/363235.363259"},{"key":"16_CR34","doi-asserted-by":"crossref","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Software Eng. 3(2), 125\u2013143 (1977). https:\/\/doi.org\/10.1109\/TSE.1977.229904","DOI":"10.1109\/TSE.1977.229904"},{"key":"16_CR35","doi-asserted-by":"crossref","unstructured":"Lin, S., Andr\u00e9, \u00c9., Liu, Y., Sun, J., Dong, J.S.: Learning assumptions for compositional verification of timed systems. IEEE Trans. Softw. Eng. 40(2), 137\u2013153 (2014). https:\/\/doi.org\/10.1109\/TSE.2013.57","DOI":"10.1109\/TSE.2013.57"},{"key":"16_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-48153-2_30","volume-title":"Correct Hardware Design and Verification Methods","author":"KL McMillan","year":"1999","unstructured":"McMillan, K.L.: Circular compositional reasoning about liveness. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 342\u2013346. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_30"},{"key":"16_CR37","doi-asserted-by":"crossref","unstructured":"Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Software Eng. 7(4), 417\u2013426 (1981). https:\/\/doi.org\/10.1109\/TSE.1981.230844","DOI":"10.1109\/TSE.1981.230844"},{"key":"16_CR38","doi-asserted-by":"crossref","unstructured":"Nam, W., Madhusudan, P., Alur, R.: Automatic symbolic compositional verification by learning assumptions. Formal Methods Syst. Des. 32(3), 207\u2013234 (2008). https:\/\/doi.org\/10.1007\/s10703-008-0055-8","DOI":"10.1007\/s10703-008-0055-8"},{"key":"16_CR39","doi-asserted-by":"crossref","unstructured":"Namjoshi, K.S., Trefler, R.J.: On the completeness of compositional reasoning methods. ACM Trans. Comput. Log. 11(3), 16:1\u201316:22 (2010). https:\/\/doi.org\/10.1145\/1740582.1740584","DOI":"10.1145\/1740582.1740584"},{"key":"16_CR40","doi-asserted-by":"crossref","unstructured":"Owicki, S.S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Commun. ACM 19(5), 279\u2013285 (1976). https:\/\/doi.org\/10.1145\/360051.360224","DOI":"10.1145\/360051.360224"},{"key":"16_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-642-35632-2_23","volume-title":"Runtime Verification","author":"S Pinisetty","year":"2013","unstructured":"Pinisetty, S., Falcone, Y., J\u00e9ron, T., Marchand, H., Rollet, A., Nguena Timo, O.L.: Runtime enforcement of timed properties. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 229\u2013244. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35632-2_23"},{"key":"16_CR42","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems - Conference proceedings, Colle-sur-Loup (near Nice), France, 8\u201319 October 1984. NATO ASI Series, pp. 123\u2013144. Springer (1984). https:\/\/doi.org\/10.1007\/978-3-642-82453-1_5","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"16_CR43","doi-asserted-by":"crossref","unstructured":"Rivest, R.L., Schapire, R.E.: Inference of finite automata using homing sequences. Inf. Comput. 103(2), 299\u2013347 (1993). https:\/\/doi.org\/10.1006\/inco.1993.1021","DOI":"10.1006\/inco.1993.1021"},{"key":"16_CR44","unstructured":"de\u00a0Roever, W.P., et al.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods, Cambridge Tracts in Theoretical Computer Science, vol.\u00a054. Cambridge University Press (2001)"},{"key":"16_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-030-25540-4_2","volume-title":"Computer Aided Verification","author":"V Roussanaly","year":"2019","unstructured":"Roussanaly, V., Sankur, O., Markey, N.: Abstraction refinement algorithms for timed automata. In: Dillig, I., Tasiran, S. (eds.) CAV 2019, Part I. LNCS, vol. 11561, pp. 22\u201340. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_2"},{"key":"16_CR46","doi-asserted-by":"crossref","unstructured":"Sankur, O.: Timed automata verification and synthesis via finite automata learning. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, 22\u201327 April 2023, Proceedings, Part II. LNCS, pp. 329\u2013349. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_21","DOI":"10.1007\/978-3-031-30820-8_21"},{"key":"16_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-319-30734-3_25","volume-title":"Theory and Practice of Formal Methods","author":"M Sirjani","year":"2016","unstructured":"Sirjani, M., Khamespanah, E.: On time actors. In: \u00c1brah\u00e1m, E., Bonsangue, M., Johnsen, E.B. (eds.) Theory and Practice of Formal Methods. LNCS, vol. 9660, pp. 373\u2013392. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-30734-3_25"},{"key":"16_CR48","doi-asserted-by":"crossref","unstructured":"Sirjani, M., Movaghar, A., Shali, A., de\u00a0Boer, F.S.: Modeling and verification of reactive systems using Rebeca. Fundam. Informaticae 63(4), 385\u2013410 (2004). https:\/\/doi.org\/10.3233\/FUN-2004-63405","DOI":"10.3233\/FUN-2004-63405"},{"key":"16_CR49","doi-asserted-by":"crossref","unstructured":"Staron, M.: Automotive Software Architectures - An Introduction, 2nd edn. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-65939-4","DOI":"10.1007\/978-3-030-65939-4"},{"key":"16_CR50","doi-asserted-by":"crossref","unstructured":"Tripakis, S.: Folk theorems on the determinization and minimization of timed automata. Inf. Process. Lett. 99(6), 222\u2013226 (2006). https:\/\/doi.org\/10.1016\/J.IPL.2006.04.015","DOI":"10.1016\/j.ipl.2006.04.015"},{"key":"16_CR51","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Verification of open systems. In: Ramesh, S., Sivakumar, G. (eds.) Foundations of Software Technology and Theoretical Computer Science, 17th Conference, Kharagpur, India, 18\u201320 December 1997, Proceedings. LNCS, pp. 250\u2013266. Springer (1997). https:\/\/doi.org\/10.1007\/BFB0058035","DOI":"10.1007\/BFb0058035"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32526-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:46:49Z","timestamp":1784796409000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32526-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325259","9783032325266"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32526-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","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":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}