{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T20:05:48Z","timestamp":1760731548523,"version":"3.40.5"},"reference-count":33,"publisher":"Cambridge University Press (CUP)","issue":"9","license":[{"start":{"date-parts":[[2022,9,6]],"date-time":"2022-09-06T00:00:00Z","timestamp":1662422400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2022,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Given the complexity of cyber-physical systems (CPS), such as swarms of drones, often deviations, from a planned mission or protocol, occur which may in some cases lead to harm and losses. To increase the robustness of such systems, it is necessary to detect when deviations happen and diagnose the cause(s) for a deviation. We build on our previous work on soft agents, a formal framework based on using rewriting logic for specifying and reasoning about distributed CPS, to develop methods for diagnosis of CPS at design time. We accomplish this by (1) extending the soft agents framework with Fault Models; (2) proposing a protocol specification language and the definition of protocol deviations; and (3) development of workflows\/algorithms for detection and diagnosis of protocol deviations. Our approach is partially inspired by existing work using counterfactual reasoning for fault ascription. We demonstrate our machinery with a collection of experiments.<\/jats:p>","DOI":"10.1017\/s0960129522000251","type":"journal-article","created":{"date-parts":[[2022,9,6]],"date-time":"2022-09-06T07:34:34Z","timestamp":1662449674000},"page":"1254-1282","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":3,"title":["Detection and diagnosis of deviations in distributed systems of autonomous agents"],"prefix":"10.1017","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4089-1218","authenticated-orcid":false,"given":"Vivek","family":"Nigam","sequence":"first","affiliation":[]},{"given":"Minyoung","family":"Kim","sequence":"additional","affiliation":[]},{"given":"Ian","family":"Mason","sequence":"additional","affiliation":[]},{"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2022,9,6]]},"reference":[{"key":"S0960129522000251_ref10","doi-asserted-by":"crossref","unstructured":"G\u00f6ssler, G. and Astefanoaei, L. (2014). Blaming in component-based real-time systems. In: Proceedings of the Embedded Software (EMSOFT), 7:1\u20137:10.","DOI":"10.1145\/2656045.2656048"},{"key":"S0960129522000251_ref13","first-page":"843","article-title":"Causes and explanations: A structural-model approach","volume":"56","author":"Halpern","year":"2005","journal-title":"Part I: Causes. British Journal for the Philosophy of Science"},{"key":"S0960129522000251_ref5","doi-asserted-by":"crossref","unstructured":"Choi, J. S. , McCarthy, T. , Kim, M. and Stehr, M.-O. (2013). Adaptive wireless networks as an example of declarative fractionated systems. In: Mobile and Ubiquitous Systems: Computing, Networking, and Services. MobiQuitous 2013, Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering, vol. 131, Springer.","DOI":"10.1007\/978-3-319-11569-6_43"},{"key":"S0960129522000251_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2020.06.010"},{"key":"S0960129522000251_ref21","unstructured":"Maude-Team (2021). The Maude System. Accessed: 2021-06-21."},{"key":"S0960129522000251_ref25","doi-asserted-by":"crossref","unstructured":"Moradi, F. , Asadollah, S. A. , Sedaghatbaf, A. , Causevic, A. , Sirjani, M. and Talcott, C. L. 2020. An actor-based approach for security analysis of cyber-physical systems. In: Formal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Vienna, Austria, September 2\u20133, 2020, Proceedings, 130\u2013147.","DOI":"10.1007\/978-3-030-58298-2_5"},{"key":"S0960129522000251_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"S0960129522000251_ref30","unstructured":"Sha, L. , Al-Nayeem, A. , Sun, M. , Meseguer, J. and \u00d6lveczky, P. C. (2009). PALS: Physically asynchronous logically synchronous systems. In: The IEEE Real-Time Systems Symposium."},{"key":"S0960129522000251_ref29","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.25"},{"volume-title":"Causality: Models, Reasoning, and Inference","year":"2000","author":"Pearl","key":"S0960129522000251_ref27"},{"key":"S0960129522000251_ref15","doi-asserted-by":"publisher","DOI":"10.1017\/S096012951500016X"},{"key":"S0960129522000251_ref20","doi-asserted-by":"crossref","unstructured":"Mason, I. A. , Nigam, V. , Talcott, C. and Brito, A. (2017). A framework for analyzing adaptive autonomous aerial vehicles. In: 1st Workshop on Formal Co-Simulation of Cyber-Physical Systems.","DOI":"10.1007\/978-3-319-74781-1_28"},{"key":"S0960129522000251_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/256303.256306"},{"key":"S0960129522000251_ref7","doi-asserted-by":"publisher","DOI":"10.1109\/VNC51378.2020.9318334"},{"key":"S0960129522000251_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-28766-9_6"},{"key":"S0960129522000251_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57318-6_30"},{"key":"S0960129522000251_ref17","unstructured":"Kim, M. , Mason, I. and Talcott, C. 2019. Softagents diagnosis. Accessed: 2021-06-21."},{"key":"S0960129522000251_ref28","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"S0960129522000251_ref6","volume-title":"LNCS","volume":"4350","author":"Clavel","year":"2007"},{"key":"S0960129522000251_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2019.08.001"},{"key":"S0960129522000251_ref31","volume-title":"Software, Services, and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering","volume":"8950","author":"Talcott","year":"2015"},{"key":"S0960129522000251_ref9","unstructured":"Frehse, G. and Althoff, M. (eds.) (2021). 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21), EPiC Series in Computing, EPIC."},{"key":"S0960129522000251_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.06.003"},{"key":"S0960129522000251_ref8","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008335115538"},{"key":"S0960129522000251_ref18","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2018\/260"},{"key":"S0960129522000251_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.05.006"},{"volume-title":"Verifying Cyber-Physical Systems","year":"2021","author":"Mitra","key":"S0960129522000251_ref24"},{"key":"S0960129522000251_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/3157831.3157835"},{"key":"S0960129522000251_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-34096-8_1"},{"key":"S0960129522000251_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_23"},{"key":"S0960129522000251_ref3","first-page":"129","volume-title":"LNCS","volume":"7215","author":"Basin","year":"2012"},{"key":"S0960129522000251_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-12441-9_11"},{"key":"S0960129522000251_ref33","doi-asserted-by":"crossref","first-page":"299","DOI":"10.3233\/JCS-200012","article-title":"Resource and timing aspects of security protocols","volume":"29","author":"Urquiza","year":"2021","journal-title":"Journal of Computer Security"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129522000251","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,29]],"date-time":"2023-03-29T02:33:39Z","timestamp":1680057219000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129522000251\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,6]]},"references-count":33,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2022,10]]}},"alternative-id":["S0960129522000251"],"URL":"https:\/\/doi.org\/10.1017\/s0960129522000251","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2022,9,6]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}