{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,8]],"date-time":"2025-11-08T18:07:46Z","timestamp":1762625266087,"version":"3.40.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031659409"},{"type":"electronic","value":"9783031659416"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-65941-6_7","type":"book-chapter","created":{"date-parts":[[2024,8,1]],"date-time":"2024-08-01T07:10:56Z","timestamp":1722496256000},"page":"124-144","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Timed Strategies for\u00a0Real-Time Rewrite Theories"],"prefix":"10.1007","author":[{"given":"Carlos","family":"Olarte","sequence":"first","affiliation":[]},{"given":"Peter Csaba","family":"\u00d6lveczky","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,8,2]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"AlTurki, M., Dhurjati, D., Yu, D., Chander, A., Inamura, H.: Formal specification and analysis of timing properties in software systems. In: Fundamental Approaches to Software Engineering (FASE 2009). LNCS, vol.\u00a05503, pp. 262\u2013277. Springer, Berlin (2009). https:\/\/doi.org\/10.1007\/978-3-642-00593-0_18","DOI":"10.1007\/978-3-642-00593-0_18"},{"key":"7_CR2","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/3563822.3569923","DOI":"10.1145\/3563822.3569923"},{"key":"7_CR3","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. In: Application and Theory of Petri Nets and Concurrency (PETRI NETS 2023). LNCS, vol. 13929, pp. 369\u2013392. Springer, Berlin (2023). https:\/\/doi.org\/10.1007\/978-3-031-33620-1_20","DOI":"10.1007\/978-3-031-33620-1_20"},{"key":"7_CR4","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 networks of parametric timed automata with global variables using Maude and SMT solving. Sci. Comput. Program. 233 (2024).https:\/\/doi.org\/10.1016\/j.scico.2023.103074","DOI":"10.1016\/j.scico.2023.103074"},{"key":"7_CR5","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1016\/j.scico.2010.10.002","DOI":"10.1016\/j.scico.2010.10.002"},{"key":"7_CR6","doi-asserted-by":"publisher","unstructured":"Beffara, E., Bournez, O., Kacem, H., Kirchner, C.: Verification of timed automata using rewrite rules and strategies (2009). https:\/\/doi.org\/10.48550\/arXiv.0907.3123","DOI":"10.48550\/arXiv.0907.3123"},{"key":"7_CR7","doi-asserted-by":"publisher","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Formal Methods for the Design of Real-Time Systems (SFM-RT 2004). LNCS, vol.\u00a03185, pp. 200\u2013236. Springer, Berlin (2004). https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"7_CR8","doi-asserted-by":"publisher","unstructured":"Bobba, R., Grov, J., Gupta, I., Liu, S., Meseguer, J., \u00d6lveczky, P.C., Skeirik, S.: Survivability: Design, formal modeling, and validation of cloud storage systems using Maude. In: Assured Cloud Computing, Chap.\u00a02, pp. 10\u201348. Wiley, New York (2018). https:\/\/doi.org\/10.1002\/9781119428497.ch2","DOI":"10.1002\/9781119428497.ch2"},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Borovansk\u00fd, P., Kirchner, C., Kirchner, H., Ringeissen, C.: Rewriting with strategies in ELAN: A functional semantics. Int. J. Found. Comput. Sci. 12(1), 69\u201395 (2001). https:\/\/doi.org\/10.1142\/S0129054101000412","DOI":"10.1142\/S0129054101000412"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Bravenboer, M., Kalleberg, K.T., Vermaas, R., Visser, E.: Stratego\/XT 0.17. A language and toolset for program transformation. Sci. Comput. Program. 72(1\u20132), 52\u201370 (2008). https:\/\/doi.org\/10.1016\/J.SCICO.2007.11.003","DOI":"10.1016\/J.SCICO.2007.11.003"},{"key":"7_CR11","doi-asserted-by":"publisher","unstructured":"Caccamo, M., Buttazzo, G.C., Sha, L.: Capacity sharing for overrun control. In: Proceedings of the 21st IEEE Real-Time Systems Symposium (RTSS 2000), pp. 295\u2013304. IEEE Computer Society (2000). https:\/\/doi.org\/10.1109\/REAL.2000.896018","DOI":"10.1109\/REAL.2000.896018"},{"key":"7_CR12","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Escobar, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Rubio, R., Talcott, C.: Maude Manual (Version 3.3.1). SRI International (2023). available at http:\/\/maude.cs.illinois.edu"},{"key":"7_CR13","doi-asserted-by":"publisher","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.L.: All About Maude\u2014A High-Performance Logical Framework, LNCS, vol.\u00a04350. Springer, Berlin (2007) https:\/\/doi.org\/10.1007\/978-3-540-71999-1","DOI":"10.1007\/978-3-540-71999-1"},{"key":"7_CR14","doi-asserted-by":"publisher","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Mikucionis, M., Taankvist, J.H.: Uppaal Stratego. In: TACAS 2015. LNCS, vol.\u00a09035. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_16","DOI":"10.1007\/978-3-662-46681-0_16"},{"key":"7_CR15","doi-asserted-by":"publisher","unstructured":"Eker, S., Mart\u00ed-Oliet, N., Meseguer, J., Rubio, R., Verdejo, A.: The Maude strategy language. J. Log. Algebraic Methods Program. 134, 100887 (2023). https:\/\/doi.org\/10.1016\/J.JLAMP.2023.100887","DOI":"10.1016\/J.JLAMP.2023.100887"},{"key":"7_CR16","doi-asserted-by":"publisher","unstructured":"Grov, J., \u00d6lveczky, P.C.: Formal modeling and analysis of Google\u2019s Megastore in real-time Maude. In: Specification, Algebra, and Software\u2014Essays Dedicated to Kokichi Futatsugi. LNCS, vol.\u00a08373, pp. 494\u2013519. Springer, Berlin (2014). https:\/\/doi.org\/10.1007\/978-3-642-54624-2_25","DOI":"10.1007\/978-3-642-54624-2_25"},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Hidalgo-Herrero, M., Verdejo, A., Ortega-Mall\u00e9n, Y.: Using Maude and its strategies for defining a framework for analyzing Eden semantics. In: Antoy, S. (ed.) WRS@FLoC 2006. ENTCS, vol.\u00a0174, pp. 119\u2013137. Elsevier (2006). https:\/\/doi.org\/10.1016\/J.ENTCS.2007.02.051","DOI":"10.1016\/J.ENTCS.2007.02.051"},{"key":"7_CR18","doi-asserted-by":"publisher","unstructured":"Lepri, D., \u00c1brah\u00e1m, E., \u00d6lveczky, P.C.: Sound and complete timed CTL model checking of timed Kripke structures and real-time rewrite theories. Sci. Comput. Program. 99, 128\u2013192 (2015). https:\/\/doi.org\/10.1016\/j.scico.2014.06.006","DOI":"10.1016\/j.scico.2014.06.006"},{"key":"7_CR19","doi-asserted-by":"publisher","unstructured":"Liu, S., Meseguer, J., \u00d6lveczky, P.C., Zhang, M., Basin, D.A.: Bridging the semantic gap between qualitative and quantitative models of distributed systems. Proc. ACM Program. Lang. 6(OOPSLA2), 315\u2013344 (2022). https:\/\/doi.org\/10.1145\/3563299","DOI":"10.1145\/3563299"},{"key":"7_CR20","doi-asserted-by":"publisher","unstructured":"Liu, S., \u00d6lveczky, P.C., Meseguer, J.: Modeling and analyzing mobile ad hoc networks in Real-Time Maude. J. Log. Algebraic Methods Program. 85(1), 34\u201366 (2016). https:\/\/doi.org\/10.1016\/j.jlamp.2015.05.002","DOI":"10.1016\/j.jlamp.2015.05.002"},{"key":"7_CR21","doi-asserted-by":"publisher","unstructured":"Marin, M., Kutsia, T.: Foundations of the rule-based system rLog. J. Appl. Non Class. Logics 16(1\u20132), 151\u2013168 (2006). https:\/\/doi.org\/10.3166\/JANCL.16.151-168","DOI":"10.3166\/JANCL.16.151-168"},{"key":"7_CR22","doi-asserted-by":"publisher","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73\u2013155 (1992). https:\/\/doi.org\/10.1016\/0304-3975(92)90182-F","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"7_CR23","doi-asserted-by":"publisher","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Recent Trends in Algebraic Development Techniques (WADT\u201997). LNCS, vol.\u00a01376, pp. 18\u201361. Springer, Berlin (1997).https:\/\/doi.org\/10.1007\/3-540-64299-4_26","DOI":"10.1007\/3-540-64299-4_26"},{"key":"7_CR24","unstructured":"Olarte, C., \u00d6lveczky, P.C.: RT-Strategies (2024). https:\/\/depot.lipn.univ-paris13.fr\/real-time-maude\/rt-strategies.git"},{"key":"7_CR25","unstructured":"Olarte, C., \u00d6lveczky, P.C.: Timed strategies for real-time rewrite theories (2024). https:\/\/arxiv.org\/abs\/2403.08920"},{"key":"7_CR26","doi-asserted-by":"publisher","unstructured":"\u00d6lveczky, P.C.: Real-Time Maude and its applications. In: Rewriting Logic and Its Applications (WRLA 2014). LNCS, vol.\u00a08663, pp. 42\u201379. Springer, Berlin (2014). https:\/\/doi.org\/10.1007\/978-3-319-12904-4_3","DOI":"10.1007\/978-3-319-12904-4_3"},{"key":"7_CR27","doi-asserted-by":"publisher","unstructured":"\u00d6lveczky, P.C., Boronat, A., Meseguer, J.: Formal semantics and analysis of behavioral AADL models in Real-Time Maude. In: Formal Techniques for Distributed Systems, Joint 12th IFIP WG 6.1 International Conference, FMOODS 2010 and 30th IFIP WG 6.1 FORTE 2010. LNCS, vol.\u00a06117, pp. 47\u201362. Springer, Berlin (2010). https:\/\/doi.org\/10.1007\/978-3-642-13464-7_5","DOI":"10.1007\/978-3-642-13464-7_5"},{"key":"7_CR28","doi-asserted-by":"publisher","unstructured":"\u00d6lveczky, P.C., Caccamo, M.: Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude. In: Fundamental Approaches to Software Engineering (FASE 2006). LNCS, vol.\u00a03922, pp. 357\u2013372. Springer, Berlin (2006). https:\/\/doi.org\/10.1007\/11693017_26","DOI":"10.1007\/11693017_26"},{"key":"7_CR29","doi-asserted-by":"publisher","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Specification of real-time and hybrid systems in rewriting logic. Theor. Comput. Sci. 285(2), 359\u2013405 (2002). https:\/\/doi.org\/10.1016\/S0304-3975(01)00363-2","DOI":"10.1016\/S0304-3975(01)00363-2"},{"key":"7_CR30","doi-asserted-by":"publisher","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. High. Order Symb. Comput. 20(1\u20132), 161\u2013196 (2007). https:\/\/doi.org\/10.1007\/s10990-007-9001-5","DOI":"10.1007\/s10990-007-9001-5"},{"key":"7_CR31","doi-asserted-by":"publisher","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: The Real-Time Maude tool. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008). LNCS, vol.\u00a04963, pp. 332\u2013336. Springer, Berlin (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_23","DOI":"10.1007\/978-3-540-78800-3_23"},{"key":"7_CR32","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/s10703-006-0015-0","DOI":"10.1007\/s10703-006-0015-0"},{"key":"7_CR33","doi-asserted-by":"publisher","unstructured":"\u00d6lveczky, P.C., Thorvaldsen, S.: Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude. Theor. Comput. Sci. 410(2\u20133), 254\u2013280 (2009). https:\/\/doi.org\/10.1016\/j.tcs.2008.09.022","DOI":"10.1016\/j.tcs.2008.09.022"},{"key":"7_CR34","doi-asserted-by":"publisher","unstructured":"Rosa-Velardo, F., Segura, C., Verdejo, A.: Typed mobile ambients in Maude. In: Cirstea, H., Mart\u00ed-Oliet, N. (eds.) RULE@RDP 2005. ENTCS, vol.\u00a0147, pp. 135\u2013161. Elsevier (2005). https:\/\/doi.org\/10.1016\/J.ENTCS.2005.06.041","DOI":"10.1016\/J.ENTCS.2005.06.041"},{"key":"7_CR35","doi-asserted-by":"publisher","unstructured":"Rubio, R., Mart\u00ed-Oliet, N., Pita, I., Verdejo, A.: Strategies, model checking and branching-time properties in Maude. J. Log. Algebraic Methods Program. 123, 100700 (2021). https:\/\/doi.org\/10.1016\/J.JLAMP.2021.100700","DOI":"10.1016\/J.JLAMP.2021.100700"},{"key":"7_CR36","doi-asserted-by":"publisher","unstructured":"Rubio, R., Mart\u00ed-Oliet, N., Pita, I., Verdejo, A.: Model checking strategy-controlled systems in rewriting logic. Autom. Softw. Eng. 29(1), 7 (2022). https:\/\/doi.org\/10.1007\/S10515-021-00307-9","DOI":"10.1007\/S10515-021-00307-9"},{"key":"7_CR37","doi-asserted-by":"publisher","unstructured":"Rubio, R., Mart\u00ed-Oliet, N., Pita, I., Verdejo, A.: Simulating and model checking membrane systems using strategies in Maude. J. Log. Algebraic Methods Program. 124, 100727 (2022). https:\/\/doi.org\/10.1016\/J.JLAMP.2021.100727","DOI":"10.1016\/J.JLAMP.2021.100727"},{"key":"7_CR38","doi-asserted-by":"publisher","unstructured":"Sabahi-Kaviani, Z., Khosravi, R., \u00d6lveczky, P.C., Khamespanah, E., Sirjani, M.: Formal semantics and efficient analysis of Timed Rebeca in Real-Time Maude. Sci. Comput. Program. 113, 85\u2013118 (2015). https:\/\/doi.org\/10.1016\/J.SCICO.2015.07.003","DOI":"10.1016\/J.SCICO.2015.07.003"},{"key":"7_CR39","doi-asserted-by":"publisher","unstructured":"Santos-Garc\u00eda, G., Palomino, M., Verdejo, A.: Rewriting logic using strategies for neural networks: An implementation in Maude. In: Corchado, J.M., Rodr\u00edguez, S., Llinas, J., Molina, J.M. (eds.) DCAI 2008. Advances in Soft Computing, vol.\u00a050, pp. 424\u2013433. Springer, Berlin (2008). https:\/\/doi.org\/10.1007\/978-3-540-85863-8_50","DOI":"10.1007\/978-3-540-85863-8_50"}],"container-title":["Lecture Notes in Computer Science","Rewriting Logic and Its Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65941-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,1]],"date-time":"2024-08-01T07:12:29Z","timestamp":1722496349000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65941-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031659409","9783031659416"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65941-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"2 August 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"WRLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Rewriting Logic and its Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"wrla2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/wrla2024.gitlab.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}