{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,2]],"date-time":"2026-06-02T20:04:44Z","timestamp":1780430684999,"version":"3.54.1"},"reference-count":58,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,3,21]],"date-time":"2026-03-21T00:00:00Z","timestamp":1774051200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100009917","name":"US Naval Research Laboratory","doi-asserted-by":"publisher","award":["N0017317-1-G002"],"award-info":[{"award-number":["N0017317-1-G002"]}],"id":[{"id":"10.13039\/100009917","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100023652","name":"Sveu\u010dili\u0161te u Rijeci","doi-asserted-by":"publisher","award":["uniri-iz-25-74"],"award-info":[{"award-number":["uniri-iz-25-74"]}],"id":[{"id":"10.13039\/501100023652","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004488","name":"Croatian Science Foundation","doi-asserted-by":"publisher","award":["HRZZ-IP-2024-05-3882"],"award-info":[{"award-number":["HRZZ-IP-2024-05-3882"]}],"id":[{"id":"10.13039\/501100004488","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-15-1-2202"],"award-info":[{"award-number":["N00014-15-1-2202"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-20-1-2635"],"award-info":[{"award-number":["N00014-20-1-2635"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-20-1-2644"],"award-info":[{"award-number":["N00014-20-1-2644"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Journal of Logical and Algebraic Methods in Programming"],"published-print":{"date-parts":[[2026,6]]},"DOI":"10.1016\/j.jlamp.2026.101124","type":"journal-article","created":{"date-parts":[[2026,3,22]],"date-time":"2026-03-22T23:05:54Z","timestamp":1774220754000},"page":"101124","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Verification of time-bounded multiset rewriting properties"],"prefix":"10.1016","volume":"150","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3230-6891","authenticated-orcid":false,"given":"Tajana","family":"Ban Kirigin","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-9734-3457","authenticated-orcid":false,"given":"Jesse","family":"Comer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7502-1653","authenticated-orcid":false,"given":"Max","family":"Kanovich","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4536-0419","authenticated-orcid":false,"given":"Andre","family":"Scedrov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2845-7144","authenticated-orcid":false,"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/j.jlamp.2026.101124_bib0001","unstructured":"R. Bloomfield, G. Fletcher, H. Khlaaf, P. Ryan, S. Kinoshita, Y. Kinoshita, M. Takeyama, Y. Matsubara, P. Popov, K. Imai, et al., Towards identifying and closing gaps in assurance of autonomous road vehicles\u2013a collection of technical notes part 1, (2020). arXiv preprint arXiv: 2003.00789."},{"issue":"2","key":"10.1016\/j.jlamp.2026.101124_bib0002","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1109\/JSYST.2009.2017397","article-title":"Towards a conceptual framework for resilience engineering","volume":"3","author":"Madni","year":"2009","journal-title":"IEEE Syst. J."},{"issue":"2","key":"10.1016\/j.jlamp.2026.101124_bib0003","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1002\/sys.21234","article-title":"Towards affordably adaptable and effective systems","volume":"16","author":"Neches","year":"2013","journal-title":"Syst. Eng."},{"issue":"1","key":"10.1016\/j.jlamp.2026.101124_bib0004","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1145\/3519262","article-title":"The many faces of resilience","volume":"66","author":"Lewis","year":"2022","journal-title":"Commun. ACM"},{"key":"10.1016\/j.jlamp.2026.101124_bib0005","series-title":"2019IEEE\/ACM 14th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS)","first-page":"70","article-title":"Modelling and analysing resilient cyber-physical systems","author":"Bennaceur","year":"2019"},{"issue":"1","key":"10.1016\/j.jlamp.2026.101124_bib0006","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1109\/JPROC.2017.2731741","article-title":"SURE: A modeling and simulation integration platform for evaluation of secure and resilient cyber-physical systems","volume":"106","author":"Koutsoukos","year":"2018","journal-title":"Proc. IEEE"},{"key":"10.1016\/j.jlamp.2026.101124_bib0007","series-title":"From Chance to Choice: Strategies to Attaining Resilience in Cyber-Physical Systems","author":"Caldas","year":"2024"},{"issue":"1","key":"10.1016\/j.jlamp.2026.101124_bib0008","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1109\/COMST.2020.3036778","article-title":"Resilient machine learning for networked cyber physical systems: a survey for machine learning security to securing machine learning for CPS","volume":"23","author":"Olowononi","year":"2021","journal-title":"IEEe Commun. Surv. Tutorials"},{"key":"10.1016\/j.jlamp.2026.101124_bib0009","series-title":"2021 IEEE International Conference on Cyber Security and Resilience (CSR)","first-page":"536","article-title":"Towards resilient artificial intelligence: survey and research issues","author":"Eigner","year":"2021"},{"key":"10.1016\/j.jlamp.2026.101124_bib0010","series-title":"Towards Robust and Resilient Machine Learning","author":"Prasad","year":"2022"},{"key":"10.1016\/j.jlamp.2026.101124_bib0011","article-title":"Adversarial resilience in sequential prediction via abstention","volume":"36","author":"Goel","year":"2024","journal-title":"Adv. Neural. Inf. Process. Syst."},{"issue":"8","key":"10.1016\/j.jlamp.2026.101124_bib0012","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1145\/2692916.2555248","article-title":"Resilient X10: efficient failure-aware programming","volume":"49","author":"Cunningham","year":"2014","journal-title":"SIGPLAN Not."},{"key":"10.1016\/j.jlamp.2026.101124_bib0013","series-title":"IEEE\/IFIP International Conference on Dependable Systems and Networks Workshops (DSN 2012)","first-page":"1","article-title":"A programming model for resilience in extreme scale computing","author":"Hukerikar","year":"2012"},{"key":"10.1016\/j.jlamp.2026.101124_bib0014","series-title":"Experimental Algorithms","first-page":"1","article-title":"Experimental study of resilient algorithms and data structures","author":"Ferraro-Petrillo","year":"2010"},{"issue":"2","key":"10.1016\/j.jlamp.2026.101124_bib0015","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/s00453-015-0073-z","article-title":"Resilient dynamic programming","volume":"77","author":"Caminiti","year":"2017","journal-title":"Algorithmica"},{"key":"10.1016\/j.jlamp.2026.101124_bib0016","series-title":"Technical Report","article-title":"Cyber-Physical Resilience: A Report to the President","author":"Science","year":"2024"},{"issue":"5","key":"10.1016\/j.jlamp.2026.101124_bib0017","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1145\/3388890","article-title":"Efficiency vs. resilience: what COVID-19 teaches computing","volume":"63","author":"Vardi","year":"2020","journal-title":"Commun. ACM"},{"key":"10.1016\/j.jlamp.2026.101124_bib0018","series-title":"Theoretical Aspects of Computing\u2013ICTAC 2022: 19th International Colloquium, Tbilisi, Georgia, September 27\u201329, 2022, Proceedings","first-page":"96","article-title":"On the formalization and computational complexity of resilience problems for cyber-physical systems","author":"Alturki","year":"2022"},{"issue":"3","key":"10.1016\/j.jlamp.2026.101124_bib0019","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1017\/S096012951500016X","article-title":"A rewriting framework and logic for activities subject to regulations","volume":"27","author":"Kanovich","year":"2017","journal-title":"Math. Struct. Comput. Sci."},{"key":"10.1016\/j.jlamp.2026.101124_bib0020","series-title":"Protocols, Strands, and Logic","first-page":"251","article-title":"On the complexity of verification of time-Sensitive distributed systems","volume":"13066","author":"Kanovich","year":"2021"},{"issue":"2","key":"10.1016\/j.jlamp.2026.101124_bib0021","doi-asserted-by":"crossref","first-page":"247","DOI":"10.3233\/JCS-2004-12203","article-title":"Multiset rewriting and the complexity of bounded security protocols","volume":"12","author":"Durgin","year":"2004","journal-title":"J. Comput. Secur."},{"key":"10.1016\/j.jlamp.2026.101124_bib0022","series-title":"14th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS)","first-page":"228","article-title":"Timed multiset rewriting and the verification of time-sensitive distributed systems","author":"Kanovich","year":"2016"},{"key":"10.1016\/j.jlamp.2026.101124_bib0023","series-title":"Rewriting Logic and Its Applications - 15th International Workshop, WRLA 2024, Luxembourg City, Luxembourg, April 6\u20137, 2024, Revised Selected Papers","first-page":"22","article-title":"Time-bounded resilience","volume":"14953","author":"Ban Kirigin","year":"2024"},{"issue":"28","key":"10.1016\/j.jlamp.2026.101124_bib0024","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1016\/j.ifacol.2022.10.350","article-title":"Resilience in discrete event systems","volume":"55","author":"Fabre","year":"2022","journal-title":"IFAC-PapersOnLine"},{"key":"10.1016\/j.jlamp.2026.101124_bib0025","series-title":"International Conference on Formal Modeling and Analysis of Timed Systems","first-page":"117","article-title":"An STL-based formulation of resilience in cyber-physical systems","author":"Chen","year":"2022"},{"key":"10.1016\/j.jlamp.2026.101124_bib0026","series-title":"FSTTCS 2021-41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science","first-page":"1","article-title":"Resilience of timed systems","author":"Akshay","year":"2021"},{"issue":"1","key":"10.1016\/j.jlamp.2026.101124_bib0027","doi-asserted-by":"crossref","DOI":"10.3390\/su9010103","article-title":"Urban resilience: a civil engineering perspective","volume":"9","author":"Bozza","year":"2017","journal-title":"Sustainability"},{"issue":"4","key":"10.1016\/j.jlamp.2026.101124_bib0028","doi-asserted-by":"crossref","first-page":"434","DOI":"10.1111\/j.0361-3666.2006.00331.x","article-title":"The concept of resilience revisited","volume":"30","author":"Manyena","year":"2006","journal-title":"Disasters"},{"issue":"3","key":"10.1016\/j.jlamp.2026.101124_bib0029","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/j.gloenvcha.2006.04.002","article-title":"Resilience: the emergence of a perspective for social-ecological systems analyses","volume":"16","author":"Folke","year":"2006","journal-title":"Global Environ. Change"},{"key":"10.1016\/j.jlamp.2026.101124_bib0030","series-title":"2013 IEEE 19th Pacific Rim International Symposium on Dependable Computing","first-page":"41","article-title":"Towards formal approaches to system resilience","author":"Sharma","year":"2013"},{"key":"10.1016\/j.jlamp.2026.101124_bib0031","series-title":"2015IEEE\/ACM 1st International Workshop on Software Protection","first-page":"45","article-title":"A framework for measuring software obfuscation resilience against automated attacks","author":"Banescu","year":"2015"},{"key":"10.1016\/j.jlamp.2026.101124_bib0032","doi-asserted-by":"crossref","first-page":"33741","DOI":"10.1109\/ACCESS.2019.2903153","article-title":"Predictive formal analysis of resilience in cyber-physical systems","volume":"7","author":"Mouelhi","year":"2019","journal-title":"IEEE Access"},{"key":"10.1016\/j.jlamp.2026.101124_bib0033","unstructured":"W. Huang, Y. Zhou, Y. Sun, A. Banks, J. Meng, J. Sharp, S. Maskell, X. Huang, Formal Verification of Robustness and Resilience of Learning-Enabled State Estimation Systems for Robotics, 2020. 2010.08311."},{"issue":"1","key":"10.1016\/j.jlamp.2026.101124_bib0034","doi-asserted-by":"crossref","DOI":"10.3390\/systems8010003","article-title":"Constructing models for systems resilience: challenges, concepts, and formal methods","volume":"8","author":"Madni","year":"2020","journal-title":"Systems"},{"issue":"4","key":"10.1016\/j.jlamp.2026.101124_bib0035","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1193\/1.1623497","article-title":"A framework to quantitatively assess and enhance the seismic resilience of communities","volume":"19","author":"Bruneau","year":"2003","journal-title":"Earthquake Spectra"},{"key":"10.1016\/j.jlamp.2026.101124_bib0036","series-title":"17th International Symposium on Theoretical Aspects of Software Engineering","first-page":"1","article-title":"Automating recoverability proofs for cyber-physical systems with runtime assurance architectures","volume":"13931","author":"Nigam","year":"2023"},{"key":"10.1016\/j.jlamp.2026.101124_bib0037","series-title":"Fault-Tolerant Systems","author":"Koren","year":"2020"},{"key":"10.1016\/j.jlamp.2026.101124_bib0038","series-title":"Design for Reliability: Information and Computer-Based Systems","author":"Bauer","year":"2011"},{"key":"10.1016\/j.jlamp.2026.101124_bib0039","series-title":"Proceedings of the 14th IEEE Workshop on Computer Security Foundations","first-page":"5","article-title":"Robust declassification","author":"Zdancewic","year":"2001"},{"issue":"2","key":"10.1016\/j.jlamp.2026.101124_bib0040","doi-asserted-by":"crossref","first-page":"157","DOI":"10.3233\/JCS-2006-14203","article-title":"Enforcing robust declassification and qualified robustness","volume":"14","author":"Myers","year":"2006","journal-title":"J. Comput. Secur."},{"key":"10.1016\/j.jlamp.2026.101124_bib0041","series-title":"Normal Accidents: Living with High Risk Technologies-updated Edition","author":"Perrow","year":"2011"},{"key":"10.1016\/j.jlamp.2026.101124_bib0042","series-title":"Cyber Resilience of Systems and Networks","volume":"1","author":"Kott","year":"2019"},{"issue":"7590","key":"10.1016\/j.jlamp.2026.101124_bib0043","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1038\/nature16948","article-title":"Universal resilience patterns in complex networks","volume":"530","author":"Gao","year":"2016","journal-title":"Nature"},{"issue":"6","key":"10.1016\/j.jlamp.2026.101124_bib0044","doi-asserted-by":"crossref","first-page":"585","DOI":"10.3233\/JCS-0560","article-title":"Time, computational complexity, and probability in the analysis of distance-bounding protocols","volume":"25","author":"Kanovich","year":"2017","journal-title":"J. Comput. Secur."},{"issue":"3\u20134","key":"10.1016\/j.jlamp.2026.101124_bib0045","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/s10817-010-9190-1","article-title":"Collaborative planning with confidentiality","volume":"46","author":"Kanovich","year":"2011","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/j.jlamp.2026.101124_bib0046","series-title":"Real-Time: Theory in Practice","first-page":"74","article-title":"Logics and models of real time: a survey","author":"Alur","year":"1992"},{"issue":"1","key":"10.1016\/j.jlamp.2026.101124_bib0047","first-page":"1","article-title":"Logics for real time: decidability and complexity","volume":"62","author":"Hirshfeld","year":"2004","journal-title":"Fundam. Inform."},{"issue":"1","key":"10.1016\/j.jlamp.2026.101124_bib0048","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(76)90061-X","article-title":"The polynomial-time hierarchy","volume":"3","author":"Stockmeyer","year":"1976","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"10.1016\/j.jlamp.2026.101124_bib0049","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/0022-0000(88)90042-6","article-title":"The complexity of facets resolved","volume":"37","author":"Papadimitriou","year":"1988","journal-title":"J. Comput. Syst. Sci."},{"issue":"2","key":"10.1016\/j.jlamp.2026.101124_bib0050","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","article-title":"Proving the correctness of multiprocess programs","volume":"SE-3","author":"Lamport","year":"1977","journal-title":"IEEE Trans. Software Eng."},{"issue":"1","key":"10.1016\/j.jlamp.2026.101124_bib0051","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/S0747-7171(87)80027-5","article-title":"Complexity of matching problems","volume":"3","author":"Benanav","year":"1987","journal-title":"J. Symb. Comput."},{"key":"10.1016\/j.jlamp.2026.101124_bib0052","series-title":"Research Report","article-title":"Improving the efficiency of AC matching and unification","author":"Eker","year":"1993"},{"key":"10.1016\/j.jlamp.2026.101124_bib0053","series-title":"Mathematical Foundations of Computer Science 1986","first-page":"573","article-title":"Complexity of generalized graph coloring","author":"Rutenburg","year":"1986"},{"key":"10.1016\/j.jlamp.2026.101124_bib0054","series-title":"Computational Complexity","author":"Papadimitriou","year":"2007"},{"key":"10.1016\/j.jlamp.2026.101124_bib0055","article-title":"All About Maude: A High-Performance Logical Framework","volume":"4350","author":"Clavel","year":"2007"},{"issue":"1","key":"10.1016\/j.jlamp.2026.101124_bib0056","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","article-title":"Conditional rewriting logic as a unified model of concurrency","volume":"96","author":"Meseguer","year":"1992","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.jlamp.2026.101124_bib0057","series-title":"Computer Security - ESORICS 2023","first-page":"42","article-title":"Protocol dialects as formal patterns","author":"Gal\u00e1n","year":"2024"},{"key":"10.1016\/j.jlamp.2026.101124_bib0058","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/s10990-007-9001-5","article-title":"Semantics and pragmatics of real-time maude","volume":"20","author":"\u00d6lveczky","year":"2007","journal-title":"Higher-Order Symb. Comput."}],"container-title":["Journal of Logical and Algebraic Methods in Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2352220826000167?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2352220826000167?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,6,2]],"date-time":"2026-06-02T19:24:49Z","timestamp":1780428289000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S2352220826000167"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6]]},"references-count":58,"alternative-id":["S2352220826000167"],"URL":"https:\/\/doi.org\/10.1016\/j.jlamp.2026.101124","relation":{},"ISSN":["2352-2208"],"issn-type":[{"value":"2352-2208","type":"print"}],"subject":[],"published":{"date-parts":[[2026,6]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Verification of time-bounded multiset rewriting properties","name":"articletitle","label":"Article Title"},{"value":"Journal of Logical and Algebraic Methods in Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.jlamp.2026.101124","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 The Author(s). Published by Elsevier Inc.","name":"copyright","label":"Copyright"}],"article-number":"101124"}}