{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T00:33:46Z","timestamp":1760747626741,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783032052902"},{"type":"electronic","value":"9783032052919"}],"license":[{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-05291-9_17","type":"book-chapter","created":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T14:08:10Z","timestamp":1758722890000},"page":"393-417","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Open CPS: A\u00a0Symbolic Model"],"prefix":"10.1007","author":[{"given":"Farhad","family":"Arbab","sequence":"first","affiliation":[]},{"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,9,25]]},"reference":[{"key":"17_CR1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/1086.001.0001","volume-title":"Actors: A Model of Concurrent Computation in Distributed Systems","author":"G Agha","year":"1986","unstructured":"Agha, G.: Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge, MA (1986)"},{"key":"17_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S095679689700261X","volume":"7","author":"G Agha","year":"1997","unstructured":"Agha, G., Mason, I.A., Smith, S.F., Talcott, C.L.: A foundation for actor computation. J. Funct. Program. 7, 1\u201372 (1997)","journal-title":"J. Funct. Program."},{"key":"17_CR3","doi-asserted-by":"publisher","unstructured":"Arbab, F., Talcott, C.: Concurrent rules machines. In: Rebeca for actor analysis in action: essays in the honour of Marjan Sirjani LNCS Festschrift, vol. 15560. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-85134-6_12","DOI":"10.1007\/978-3-031-85134-6_12"},{"key":"17_CR4","doi-asserted-by":"crossref","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. arXiv:2303.08929 (2023)","DOI":"10.1007\/978-3-031-33620-1_20"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Arias, J., Bae, K., Olarte, C., \u00d6lveczky, P.C., Petrucci, L., R\u00f8mming, F.: Symbolic analysis and parameter synthesis for networks of parametric timed automata with global variables using Maude and SMT solving. Sci. Comput. Programm. 233, 103074 (2024)","DOI":"10.1016\/j.scico.2023.103074"},{"key":"17_CR6","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: 8th USENIX Symposium on Operating Systems Design and Implementation, pp. 209\u2013224. USENIX Association (2008)"},{"key":"17_CR7","doi-asserted-by":"publisher","unstructured":"Dur\u00e1n, F., et al.: Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description). In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, 8-10 August 2022, Proceedings. LNCS, vol. 13385, pp. 529\u2013540. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_31","DOI":"10.1007\/978-3-031-10769-6_31"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Escobar, S., L\u00f3pez-Rueda, R., Sapi\u00f1a, J.: Symbolic analysis by using folding narrowing with irreducibility and SMT constraints. In: 9th ACM SIGPLAN International Workshop on Formal Techniques for Safety- Critical Systems (FTSCS 2023), pp. 14\u201325. ACM (2023)","DOI":"10.1145\/3623503.3623537"},{"issue":"7","key":"17_CR9","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Lee, E.A.: Cyber physical systems: Design challenges. In: 11th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing. IEEE (2008)","DOI":"10.1109\/ISORC.2008.25"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Lee, E.A.: Fundamental limits of cyber-physical systems modeling. In: ACM Transactions on Cyber-Physical Systems (2016)","DOI":"10.1145\/2912149"},{"issue":"6","key":"17_CR12","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., Kim, S., Kang, M., \u00d6lveczky, P.C.: Modeling and formal analysis of virtually synchronous cyber-physical systems in AADL. Int. J. Softw. Tools Technol. Transfer 24(6), 911\u2013948 (2022)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"17_CR13","doi-asserted-by":"publisher","unstructured":"Lee, J., Kim, S. and Bae, K.: An extension of HybridSynchAADL and its application to collaborating autonomous UAVs. In: Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning (ISoLA 2022), LNCS, pp. 47\u201364. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-19759-8_4","DOI":"10.1007\/978-3-031-19759-8_4"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Lee, J., Kim, S., Bae, K.: Bounded model checking of plc ST programs using rewriting modulo SMT. In: 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":"17_CR15","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.: Hybrid SynchAADL: 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":"17_CR16","doi-asserted-by":"crossref","unstructured":"Liu, S., Meseguer, J., \u00d6lveczky, P.C., Zhang, M., Basin, D.: Bridging the semantic gap between qualitative and quantitative models of distributed systems. Proc. ACM Program. Lang. 6(OOPSLA2), 315\u2013344 (2022)","DOI":"10.1145\/3563299"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Lunel, S., Boyer, B., Talpin, J.P.: Compositional proofs in differential dynamic logic DL. In: 2017 17th International Conference on Application of Concurrency to System Design (ACSD), pp. 19\u201328 (2017)","DOI":"10.1109\/ACSD.2017.16"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-030-30942-8_22","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"S Lunel","year":"2019","unstructured":"Lunel, S., Mitsch, S., Boyer, B., Talpin, J.-P.: Parallel composition and modular verification of computer controlled systems in differential dynamic logic. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 354\u2013370. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_22"},{"issue":"1","key":"17_CR19","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. Theoret. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theoret. Comput. Sci."},{"issue":"7\u20138","key":"17_CR20","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":"17_CR21","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2013.07.004","volume":"83","author":"J Meseguer","year":"2014","unstructured":"Meseguer, J.: Taming distributed system complexity through formal patterns. Sci. Comput. Program. 83, 3\u201334 (2014)","journal-title":"Sci. Comput. Program."},{"key":"17_CR22","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2019.100483","volume":"110","author":"J Meseguer","year":"2020","unstructured":"Meseguer, J.: Generalized rewrite theories, coherence completion, and symbolic methods. J. Log. Algebraic Methods Program 110, 100483 (2020)","journal-title":"J. Log. Algebraic Methods Program"},{"key":"17_CR23","doi-asserted-by":"publisher","unstructured":"Nigam, V., Talcott, C.: Automating safety proofs about cyber-physical systems using rewriting modulo SMT. In: Bae, K. (eds.) Rewriting Logic and its Applications, LNCS, 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":"17_CR24","doi-asserted-by":"publisher","unstructured":"Nigam, V., Talcott, C.: Automating recoverability proofs for cyber-physical systems with runtime assurance architectures. In: David, C., Sun, M. (eds.) (eds.) Theoretical Aspects of Software Engineering - 17th International Symposium, Proceedings. LNCS, vol. 13931, pp. 1\u201319. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-35257-7_1","DOI":"10.1007\/978-3-031-35257-7_1"},{"key":"17_CR25","doi-asserted-by":"publisher","unstructured":"P\u0103s\u0103reanu, C.S., Visser, W., Bushnell, D., Geldenhuys, J., Mehlitz, P., Rungta, N.: Symbolic pathfinder: integrating symbolic execution with model checking for java bytecode analysis. Automated Softw. Eng. 20, 391\u2013425 (2013). https:\/\/doi.org\/10.1007\/s10515-013-0122-2","DOI":"10.1007\/s10515-013-0122-2"},{"key":"17_CR26","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/s10009-015-0367-0","volume":"18","author":"J-D Quesel","year":"2016","unstructured":"Quesel, J.-D., Mitsch, S., Loos, S., Ar\u00e9chiga, N., Platzer, A.: How to model and prove hybrid systems with KeYmaera: a tutorial on safety. Int. J. Softw. Tools Technol. Transfer 18, 67\u201391 (2016)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"1","key":"17_CR27","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":"17_CR28","doi-asserted-by":"crossref","unstructured":"Zhang, Y., Li, P., Ding, Y., Wang, L., Williams, D., Meng, N.: Broadly enabling KLEE to effortlessly find unrecoverable errors in rust. In: ACM\/IEEE International Conference on Software Engineering: Software Engineering in Practice. ACM\/IEEE (2024)","DOI":"10.1145\/3639477.3639714"}],"container-title":["Lecture Notes in Computer Science","Concurrent Programming, Open Systems and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-05291-9_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T18:32:28Z","timestamp":1760725948000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-05291-9_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,25]]},"ISBN":["9783032052902","9783032052919"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-05291-9_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,9,25]]},"assertion":[{"value":"25 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}