FormIDEAble: Safe and Socially-aware Autonomous Systems

Unknown

Conceptio › Archive › arXiv CS

arXiv CSopen access

FormIDEAble: Safe and Socially-aware Autonomous Systems

Unknown · 2026 · arxiv_cs

arXiv CS · Papers · License: Open Access · 2026

Open Source ↗Direct PDF ↓

softwarearchitecture softwareengineering testing

software engineering, software architecture, testing

arXiv:2606.31572v1 [cs.SE] 30 Jun 2026

FormIDEAble: Safe and Socially-aware Autonomous Systems Livia Lestingi

Amel Bennaceur

Marcello Bersani

Politecnico di Milano Milan, Italy

The Open University Milton Keynes, UK

Politecnico di Milano Milan, Italy

The Open University Milton Keynes, UK

Anastasia Kordoni

Mark Levine

Bashar Nuseibeh

Matteo Rossi

Lancaster University Lancaster, UK

The Open University Milton Keynes, UK

Politecnico di Milano Milan, Italy

Abstract Autonomous agents operating in socio-critical settings must coordinate with humans under uncertainty while respecting explicit safety constraints. Existing approaches either account for social dynamics without formal guarantees or provide formal assurance while abstracting away human behaviour. We introduce FormIDEAble, a formally grounded approach for synthesising socially-aware cooperation strategies with safety guarantees. The cooperation between humans and the autonomous agent is modelled as a Priced Timed Markov Decision Process, and decision-making is formulated as a cost-bounded reachability problem. We illustrate the approach using an emergency evacuation scenario. Initial experimental evidence demonstrates the effectiveness of the approach and highlights the trade-offs between optimisation and safety guarantees. FormIDEAble provides a principled foundation for formally assured, socially-aware decision-making in socio-critical systems.

Keywords Autonomous Agents, Strategy Synthesis, Social Identity Theory, Safety Guarantees ACM Reference Format: Livia Lestingi, Amel Bennaceur, Marcello Bersani, Carlos Gavidia-Calderon, Anastasia Kordoni, Mark Levine, Bashar Nuseibeh, and Matteo Rossi. 2026. FormIDEAble: Safe and Socially-aware Autonomous Systems. In . ACM, New York, NY, USA, 10 pages. https://doi.org/10.1145/nnnnnnn.nnnnnnn

Carlos Gavidia-Calderon

Introduction

Autonomous agents often require interaction and cooperation with humans to achieve their goals. Such systems are considered safetycritical since they raise the need for guarantees that, even following autonomous agents’ decisions, the system will satisfy safety properties. However, human behaviour is uncertain and complex. As a result, formally reasoning about human behaviour and specifying, designing, and deploying autonomous agents able to cooperate with humans while guaranteeing safety is challenging [1]. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]. Conference’17, Washington, DC, USA © 2026 Copyright held by the owner/author(s). Publication rights licensed to ACM. ACM ISBN 978-x-xxxx-xxxx-x/YYYY/MM https://doi.org/10.1145/nnnnnnn.nnnnnnn

Many existing approaches model human behaviour probabilistically or as a reaction to system stimuli, enabling autonomous agents to reason under uncertainty [6, 8, 14]. However, these approaches typically provide limited guarantees about whether safety constraints will hold when decisions are enacted in the presence of humans. For autonomous agents to be able to interact and cooperate with humans, they need to reason about the social structures that drive human behaviour [1]. Identity-Aware Architecture for Autonomous systems (IDEA) [17] proposes a software architecture that enables humans and autonomous agents to cooperate by leveraging the notion of social identity [39] (i.e., that humans tend to behave according to the values and expectations imposed by their social groups when these become salient). IDEA demonstrates how social identity can be leveraged to support cooperation between humans and autonomous agents. However, in IDEA, the strategies are derived through equilibrium reasoning and do not provide formal guarantees that safety constraints—such as time bounds or prioritisation requirements—will always be satisfied. This paper introduces FormIDEAble (Formally-verified Identityaware Autonomous Agents), an approach for supporting cooperation between humans and autonomous agents while providing explicit safety guarantees. The core idea explored in this paper is to synthesise decision-making strategies for autonomous agents that are both socially-aware and formally verified. We model human– autonomous agent interaction as a Priced Timed Markov Decision Process (PTMDP) [11], where uncertainty captures socially-driven human responses, timing constraints capture urgency, and prices represent performance objectives. Safety requirements are formulated as reachability properties, enabling the automated synthesis of strategies that optimise performance while guaranteeing safety by construction. By formulating socially-aware cooperation as a costbounded reachability problem over PTMDPs, our approach differs from prior game-theoretic and probabilistic models by explicitly constraining strategy synthesis with formal safety requirements. This paper focuses on the foundational modelling and strategy synthesis principles underlying FormIDEAble. We present an emergency evacuation case study and initial experimental evidence that illustrates the effectiveness of the approach and the trade-offs between safety guarantees and performance metrics. A comprehensive evaluation of scalability, deployment constraints, and broader empirical validation is left to ongoing and future work. Our contributions are as follows: • a formalisation of socially-aware human–autonomous agent cooperation through PTMDPs,

Conference’17, July 2017, Washington, DC, USA

• a strategy synthesis approach that integrates social identity uncertainty with explicit safety guarantees as a cost-bounded reachability problem over PTMDPs, and • initial experimental evidence demonstrating its effectiveness.

Lestingi et al. a1 <latexit sha1_base64="TlhgfWHb5lE6BApFRYGSfoj2t6Y=">AAAB9XicbVC7TsNAEDzzDOEVoKQ5ESFRRTZCgTKChjII8pASK1pfNuGU80N3a1Bk5RNooaJDtHwPBf+CbVxAwlSjmV3t7HiRkoZs+9NaWl5ZXVsvbZQ3t7Z3dit7+20TxlpgS4Qq1F0PDCoZYIskKexGGsH3FHa8yVXmdx5QGxkGdzSN0PVhHMiRFECpdAsDZ1Cp2jU7B18kTkGqrEBzUPnqD0MR+xiQUGBMz7EjchPQJIXCWbkfG4xATGCMvZQG4KNxkzzqjB/HBijkEWouFc9F/L2RgG/M1PfSSR/o3sx7mfif14tpdOEmMohiwkBkh0gqzA8ZoWXaAfKh1EgEWXLkMuACNBChlhyESMU4LaWc9uHMf79I2qc1p16r35xVG5dFMyV2yI7YCXPYOWuwa9ZkLSbYmD2xZ/ZiPVqv1pv1/jO6ZBU7B+wPrI9vkcKSGQ==</latexit>

c1 <latexit sha1_base64="ok5ZVwmb6mQ0WGZPAcZWQudAHos=">AAAB9XicbVC7TsNAEFzzDOEVoKQ5ESFRRTZCgTKChjII8pASKzpfNuGU80N3a1Bk5RNooaJDtHwPBf+CbVxAwlSjmV3t7HiRkoZs+9NaWl5ZXVsvbZQ3t7Z3dit7+20TxlpgS4Qq1F2PG1QywBZJUtiNNHLfU9jxJleZ33lAbWQY3NE0Qtfn40COpOCUSrdi4AwqVbtm52CLxClIFQo0B5Wv/jAUsY8BCcWN6Tl2RG7CNUmhcFbuxwYjLiZ8jL2UBtxH4yZ51Bk7jg2nkEWomVQsF/H3RsJ9Y6a+l076nO7NvJeJ/3m9mEYXbiKDKCYMRHaIpML8kBFaph0gG0qNRDxLjkwGTHDNiVBLxoVIxTgtpZz24cx/v0japzWnXqvfnFUbl0UzJTiEIzgBB86hAdfQhBYIGMMTPMOL9Wi9Wm/W+8/oklXsHMAfWB/flOSSGw==</latexit>

<latexit sha1_base64="r3Ey8h2UtqIIbEcPfeSVsc8LaB0=">AAAB/nicbVC7TsNAEDzzDOEVoKQ5iJCoIhuhQBlBQxkk8pDiKDpfNuGU8/l0t0aKrEh8BS1UdIiWX6HgX7CNC0iYajSzq52dQEth0XU/naXlldW19dJGeXNre2e3srfftlFsOLR4JCPTDZgFKRS0UKCErjbAwkBCJ5hcZ37nAYwVkbrDqYZ+yMZKjARnmEq+HzK8R0zG0exoUKm6NTcHXSReQaqkQHNQ+fKHEY9DUMgls7bnuRr7CTMouIRZ2Y8taMYnbAy9lCoWgu0neeYZPYktw4hqMFRImovweyNhobXTMEgns4x23svE/7xejKPLfiKUjhEUzw6hkJAfstyItAygQ2EAkWXJgQpFOTMMEYygjPNUjNN2ymkf3vz3i6R9VvPqtfrtebVxVTRTIofkmJwSj1yQBrkhTdIinGjyRJ7Ji/PovDpvzvvP6JJT7ByQP3A+vgEWT5Zf</latexit>

<latexit sha1_base64="1HZNancsto2HgI0PMBP5pCKeHto=">AAACAHicbVC7TsNAEDyHVwivACXNiQiJAkU2QoEygoYySOQhOSY6XzbhlPPZulsjRVYavoIWKjpEy59Q8C/YxgUkTDWa2dXOjh9JYdC2P63S0vLK6lp5vbKxubW9U93d65gw1hzaPJSh7vnMgBQK2ihQQi/SwAJfQtefXGV+9wG0EaG6xWkEXsDGSowEZ5hKd/2A4b0ZJa594nizQbVm1+0cdJE4BamRAq1B9as/DHkcgEIumTGuY0foJUyj4BJmlX5sIGJ8wsbgplSxAIyX5Kln9Cg2DEMagaZC0lyE3xsJC4yZBn46maec9zLxP8+NcXThJUJFMYLi2SEUEvJDhmuR1gF0KDQgsiw5UKEoZ5ohghaUcZ6KcdpPJe3Dmf9+kXRO606j3rg5qzUvi2bK5IAckmPikHPSJNekRdqEE02eyDN5sR6tV+vNev8ZLVnFzj75A+vjG8oulrI=</latexit>

[0, 1] <latexit sha1_base64="dlYv9Gxkpn6hnLryWH9aKXwqACw=">AAACAHicbVC7TsNAEDyHVwivACXNQYREFdkIBcoIGsogkYeUmGh92YRTzg/drZEiKw1fQQsVHaLlTyj4F2yTAhKmGs3samfHi5Q0ZNufVmFpeWV1rbhe2tjc2t4p7+61TBhrgU0RqlB3PDCoZIBNkqSwE2kE31PY9sZXmd9+QG1kGNzSJELXh1Egh1IApdJdzwe6J0oMwWR62C9X7Kqdgy8SZ0YqbIZGv/zVG4Qi9jEgocCYrmNH5CagSQqF01IvNhiBGMMIuykNwEfjJnnqKT+ODVDII9RcKp6L+HsjAd+Yie+lk1lKM+9l4n9eN6bhhZvIIIoJA5EdIqkwP2SElmkdyAdSIxFkyZHLgAvQQIRachAiFeO0n1LahzP//SJpnVadWrV2c1apX86aKbIDdsROmMPOWZ1dswZrMsE0e2LP7MV6tF6tN+v9Z7RgzXb22R9YH9/Zkpde</latexit>

<latexit sha1_base64="luJ1mNXFRmIhLYrJJ61+ijvaAkI=">AAAB/nicbVC7SgNBFJ31lRhfUUubwSBYSNi1iHYGbSwjmAdklzA7uYlDZh/M3BXCEvArBCut7MTWX7Gw80Oc3aTQxFMdzrmXe+7xYyk02vantbS8srpWKK6XNja3tnfKu3stHSWKQ5NHMlIdn2mQIoQmCpTQiRWwwJfQ9kdXmd++B6VFFN7iOAYvYMNQDARnaCTXDRjeIabDaHLRK1fsqp2DLhJnRip16p58958KjV75y+1HPAkgRC6Z1l3HjtFLmULBJUxKbqIhZnzEhtA1NGQBaC/NM0/oUaIZRjQGRYWkuQi/N1IWaD0OfDOZZdTzXib+53UTHJx7qQjjBCHk2SEUEvJDmithygDaFwoQWZYcqAgpZ4ohghKUcW7ExLRTMn04898vktZp1alVazemmEsyRZEckENyTBxyRurkmjRIk3ASk0fyTF6sB+vVerPep6NL1mxnn/yB9fEDKxaZSQ==</latexit>

go!

stay!

<latexit sha1_base64="+tcLa2m5A9EUpOi3aMegKeau5E4=">AAAB9XicbVC7TsNAEFyHVwivACXNiQiJKrIjFCgjaCiDIA8piaLzZRNOOT90twZFVj6BFio6RMv3UPAv2MYFJEw1mtnVzo4bKmnItj+twsrq2vpGcbO0tb2zu1feP2ibINICWyJQge663KCSPrZIksJuqJF7rsKOO71K/c4DaiMD/45mIQ48PvHlWApOiXQrhrVhuWJX7QxsmTg5qUCO5rD81R8FIvLQJ6G4MT3HDmkQc01SKJyX+pHBkIspn2AvoT730AziLOqcnUSGU8BC1Ewqlon4eyPmnjEzz00mPU73ZtFLxf+8XkTji0Es/TAi9EV6iKTC7JARWiYdIBtJjUQ8TY5M+kxwzYlQS8aFSMQoKaWU9OEsfr9M2rWqU6/Wb84qjcu8mSIcwTGcggPn0IBraEILBEzgCZ7hxXq0Xq036/1ntGDlO4fwB9bHN5Zzkhw=</latexit>

<latexit sha1_base64="9vLM4I/cTvwmiXRZUTcnbC3GClQ=">AAACAHicbVC7TgJBFJ3FB4gv1NJmIjGxMGTXAu0k2lhiIo8EkNwdLjhh9pGZuyZkQ+NXaKmVnbH1Tyzs/BB3gULBU52cc2/uuccNlTRk259WZml5ZTWbW8uvb2xubRd2dusmiLTAmghUoJsuGFTSxxpJUtgMNYLnKmy4w8vUb9yjNjLwb2gUYseDgS/7UgAl0m3bA7ojig3BaHzeLRTtkj0BXyTOjBQrvH383XvKVruFr3YvEJGHPgkFxrQcO6RODJqkUDjOtyODIYghDLCVUB88NJ14knrMDyMDFPAQNZeKT0T8vRGDZ8zIc5PJNKWZ91LxP68VUf+sE0s/jAh9kR4iqXByyAgtkzqQ96RGIkiTI5c+F6CBCLXkIEQiRkk/+aQPZ/77RVI/KTnlUvk6KeaCTZFj++yAHTGHnbIKu2JVVmOCafbIntmL9WC9Wm/W+3Q0Y8129tgfWB8/7lmaSA==</latexit>

go?

<latexit sha1_base64="gp/WDItr82k2qkb04li1H1st+v8=">AAAB9XicbVC7TsNAEFyHVwivACXNiQiJKrIBBcoIGsogyENKouh82YRTzg/drUGRlU+ghYoO0fI9FPwLtnEBCVONZna1s+OGShqy7U+rsLS8srpWXC9tbG5t75R391omiLTApghUoDsuN6ikj02SpLATauSeq7DtTq5Sv/2A2sjAv6NpiH2Pj305koJTIt2KwemgXLGrdga2SJycVCBHY1D+6g0DEXnok1DcmK5jh9SPuSYpFM5KvchgyMWEj7GbUJ97aPpxFnXGjiLDKWAhaiYVy0T8vRFzz5ip5yaTHqd7M++l4n9eN6LRRT+WfhgR+iI9RFJhdsgILZMOkA2lRiKeJkcmfSa45kSoJeNCJGKUlFJK+nDmv18krZOqU6vWbs4q9cu8mSIcwCEcgwPnUIdraEATBIzhCZ7hxXq0Xq036/1ntGDlO/vwB9bHN5gCkh0=</latexit>

stay?

a3 0.8 <latexit sha1_base64="ekygS3o7/1VnF/Sxzo+ZDEi1zrs=">AAAB9XicbVC7TsNAEDyHVwivACXNiQiJKrIBBcoIGsogyENKomh92YRTzg/drUGRlU+ghYoO0fI9FPwLtnEBCVONZna1s+OGShqy7U+rsLS8srpWXC9tbG5t75R391omiLTApghUoDsuGFTSxyZJUtgJNYLnKmy7k6vUbz+gNjLw72gaYt+DsS9HUgAl0i0MTgflil21M/BF4uSkwnI0BuWv3jAQkYc+CQXGdB07pH4MmqRQOCv1IoMhiAmMsZtQHzw0/TiLOuNHkQEKeIiaS8UzEX9vxOAZM/XcZNIDujfzXir+53UjGl30Y+mHEaEv0kMkFWaHjNAy6QD5UGokgjQ5culzARqIUEsOQiRilJRSSvpw5r9fJK2TqlOr1m7OKvXLvJkiO2CH7Jg57JzV2TVrsCYTbMye2DN7sR6tV+vNev8ZLVj5zj77A+vjG5Tgkhs=</latexit>

<latexit sha1_base64="LrkKMIR/aG9qQt/bNrXAI1p3PYs=">AAAB9XicbVC7TsNAEDyHVwivACXNiQiJKrIjFCgjaCiDIA8piaL1ZRNOOT90twZFVj6BFio6RMv3UPAv2MYFJEw1mtnVzo4bKmnItj+twsrq2vpGcbO0tb2zu1feP2ibINICWyJQge66YFBJH1skSWE31Aieq7DjTq9Sv/OA2sjAv6NZiAMPJr4cSwGUSLcwrA3LFbtqZ+DLxMlJheVoDstf/VEgIg99EgqM6Tl2SIMYNEmhcF7qRwZDEFOYYC+hPnhoBnEWdc5PIgMU8BA1l4pnIv7eiMEzZua5yaQHdG8WvVT8z+tFNL4YxNIPI0JfpIdIKswOGaFl0gHykdRIBGly5NLnAjQQoZYchEjEKCmllPThLH6/TNq1qlOv1m/OKo3LvJkiO2LH7JQ57Jw12DVrshYTbMKe2DN7sR6tV+vNev8ZLVj5ziH7A+vjG5NRkho=</latexit>

0.2 <latexit sha1_base64="5WBCMsNQLQeYje8ophWQ6c8Ty54=">AAAB9XicbVC7TsNAEDyHVwivACXNiQiJyrIjFCgjaCiDIA8psaLzZRNOOZ+tuzUosvIJtFDRIVq+h4J/wTYuIGGq0cyudnb8SAqDjvNplVZW19Y3ypuVre2d3b3q/kHHhLHm0OahDHXPZwakUNBGgRJ6kQYW+BK6/vQq87sPoI0I1R3OIvACNlFiLDjDVLp17PqwWnNsJwddJm5BaqRAa1j9GoxCHgegkEtmTN91IvQSplFwCfPKIDYQMT5lE+inVLEAjJfkUef0JDYMQxqBpkLSXITfGwkLjJkFfjoZMLw3i14m/uf1YxxfeIlQUYygeHYIhYT8kOFapB0AHQkNiCxLDlQoyplmiKAFZZynYpyWUkn7cBe/Xyaduu027MbNWa15WTRTJkfkmJwSl5yTJrkmLdImnEzIE3kmL9aj9Wq9We8/oyWr2Dkkf2B9fAP58ZG4</latexit>

<latexit sha1_base64="bMrUa5uc4OD5+M2NTM/eIcwuCPI=">AAACBHicbVC7TsNAEDyHVwgvAyXNQYREFdkIBcoIGsogkYeUWNH5sgmnnM/W3TpSZKXlK2ihokO0/AcF/4JtXEDCVKOZXe3s+JEUBh3n0yqtrK6tb5Q3K1vbO7t79v5B24Sx5tDioQx112cGpFDQQoESupEGFvgSOv7kJvM7U9BGhOoeZxF4ARsrMRKcYSoNbLsfMHxATMRYhRrmxwO76tScHHSZuAWpkgLNgf3VH4Y8DkAhl8yYnutE6CVMo+AS5pV+bCBifMLG0EupYgEYL8mTz+lpbBiGNAJNhaS5CL83EhYYMwv8dDLLaRa9TPzP68U4uvISoaIYQfHsEAoJ+SHDtUgrAToUGhBZlhyoUJQzzRBBC8o4T8U47aiS9uEufr9M2uc1t16r311UG9dFM2VyRE7IGXHJJWmQW9IkLcLJlDyRZ/JiPVqv1pv1/jNasoqdQ/IH1sc32NOYZg==</latexit>

<latexit sha1_base64="M3QUwEUrO2bCY+ssnbA8eaEsca4=">AAAB9XicbVC7TsNAEDyHVwivACXNiQiJyrIRCikjaCiDIA8psaLzZRNOOZ+tuzUosvIJtFDRIVq+h4J/wTYuIGGq0cyudnb8SAqDjvNplVZW19Y3ypuVre2d3b3q/kHHhLHm0OahDHXPZwakUNBGgRJ6kQYW+BK6/vQq87sPoI0I1R3OIvACNlFiLDjDVLp17MawWnNsJwddJm5BaqRAa1j9GoxCHgegkEtmTN91IvQSplFwCfPKIDYQMT5lE+inVLEAjJfkUef0JDYMQxqBpkLSXITfGwkLjJkFfjoZMLw3i14m/uf1Yxw3vESoKEZQPDuEQkJ+yHAt0g6AjoQGRJYlByoU5UwzRNCCMs5TMU5LqaR9uIvfL5POme3W7frNea15WTRTJkfkmJwSl1yQJrkmLdImnEzIE3kmL9aj9Wq9We8/oyWr2Dkkf2B9fAMDWpG+</latexit>

ignore!

<latexit sha1_base64="gSwweaEeRc+kQ+Q+JSLh+1RyxNY=">AAACBHicbVC7TsNAEDyHVwgvAyXNQYREFdkIBcoIGsogkYeUWNH5sgmnnB+6W0eKrLR8BS1UdIiW/6DgXzgbF5Cw1WhmVzM7fiyFRsf5tEorq2vrG+XNytb2zu6evX/Q1lGiOLR4JCPV9ZkGKUJooUAJ3VgBC3wJHX9yk+mdKSgtovAeZzF4ARuHYiQ4Q0MNbLsfMHxATDMvCOfHA7vq1Jx86DJwC1AlxTQH9ld/GPEkgBC5ZFr3XCdGL2UKBZcwr/QTDTHjEzaGnoEhC0B7aZ58Tk8TzTCiMSgqJM1J+H2RskDrWeCbzSynXtQy8j+tl+DoyktFGCfmK54ZoZCQG2muhKkE6FAoQGRZcqAipJwphghKUMa5IRPTUcX04S5+vwza5zW3XqvfXVQb10UzZXJETsgZccklaZBb0iQtwsmUPJFn8mI9Wq/Wm/X+s1qyiptD8mesj2/qMZhx</latexit>

listen!

0.8 <latexit sha1_base64="M3QUwEUrO2bCY+ssnbA8eaEsca4=">AAAB9XicbVC7TsNAEDyHVwivACXNiQiJyrIRCikjaCiDIA8psaLzZRNOOZ+tuzUosvIJtFDRIVq+h4J/wTYuIGGq0cyudnb8SAqDjvNplVZW19Y3ypuVre2d3b3q/kHHhLHm0OahDHXPZwakUNBGgRJ6kQYW+BK6/vQq87sPoI0I1R3OIvACNlFiLDjDVLp17MawWnNsJwddJm5BaqRAa1j9GoxCHgegkEtmTN91IvQSplFwCfPKIDYQMT5lE+inVLEAjJfkUef0JDYMQxqBpkLSXITfGwkLjJkFfjoZMLw3i14m/uf1Yxw3vESoKEZQPDuEQkJ+yHAt0g6AjoQGRJYlByoU5UwzRNCCMs5TMU5LqaR9uIvfL5POme3W7frNea15WTRTJkfkmJwSl1yQJrkmLdImnEzIE3kmL9aj9Wq9We8/oyWr2Dkkf2B9fAMDWpG+</latexit>

The rest of the paper is structured as follows. Section 2 presents the case study. Section 3 outlines preliminary concepts. Section 4 details the FormIDEAble framework. Section 5 reports on the empirical validation. Section 6 reviews related work. Finally, Section 7 concludes the paper and outlines the research agenda.

a4 <latexit sha1_base64="Sn2FC4BxqulX60PaAAC99hB4P/A=">AAAB9XicbVC7TsNAEDyHVwivACXNiQiJKrJRFCgjaCiDIA8piaL1ZRNOOT90twZFVj6BFio6RMv3UPAv2MYFJEw1mtnVzo4bKmnItj+twsrq2vpGcbO0tb2zu1feP2ibINICWyJQge66YFBJH1skSWE31Aieq7DjTq9Sv/OA2sjAv6NZiAMPJr4cSwGUSLcwrA3LFbtqZ+DLxMlJheVoDstf/VEgIg99EgqM6Tl2SIMYNEmhcF7qRwZDEFOYYC+hPnhoBnEWdc5PIgMU8BA1l4pnIv7eiMEzZua5yaQHdG8WvVT8z+tFNL4YxNIPI0JfpIdIKswOGaFl0gHykdRIBGly5NLnAjQQoZYchEjEKCmllPThLH6/TNpnVaderd/UKo3LvJkiO2LH7JQ57Jw12DVrshYTbMKe2DN7sR6tV+vNev8ZLVj5ziH7A+vjG5Zvkhw=</latexit>

t → 10 <latexit sha1_base64="HRpJIBR1pejrCpOW4km4FbdPONA=">AAAB+nicbVC7TsNAEDzzDOEVoKQ5ESFRRTZCgTKChjJI5CElVrS+bMIp5wd3a6TI5CdooaJDtPwMBf+CbVxAwlSjmV3t7HiRkoZs+9NaWl5ZXVsvbZQ3t7Z3dit7+20TxlpgS4Qq1F0PDCoZYIskKexGGsH3FHa8yVXmdx5QGxkGtzSN0PVhHMiRFECp1KW+wnvu2INK1a7ZOfgicQpSZQWag8pXfxiK2MeAhAJjeo4dkZuAJikUzsr92GAEYgJj7KU0AB+Nm+R5Z/w4NkAhj1BzqXgu4u+NBHxjpr6XTvpAd2bey8T/vF5Mows3kUEUEwYiO0RSYX7ICC3TIpAPpUYiyJIjlwEXoIEIteQgRCrGaTPltA9n/vtF0j6tOfVa/eas2rgsmimxQ3bETpjDzlmDXbMmazHBFHtiz+zFerRerTfr/Wd0ySp2DtgfWB/f3+eT7Q==</latexit>

t → 10 <latexit sha1_base64="LNjvvzlPTiE/wrU35P7u+60cznQ=">AAAB+nicbVC7TsNAEFzzDOEVoKQ5ESFRRTZCgTKChjJI5CElVnS+bMIp5wd3a6TI5CdooaJDtPwMBf+CbVxAwlSjmV3t7HiRkoZs+9NaWl5ZXVsvbZQ3t7Z3dit7+20TxlpgS4Qq1F2PG1QywBZJUtiNNHLfU9jxJleZ33lAbWQY3NI0Qtfn40COpOCUSl3qj/GeOfagUrVrdg62SJyCVKFAc1D56g9DEfsYkFDcmJ5jR+QmXJMUCmflfmww4mLCx9hLacB9NG6S552x49hwClmEmknFchF/byTcN2bqe+mkz+nOzHuZ+J/Xi2l04SYyiGLCQGSHSCrMDxmhZVoEsqHUSMSz5MhkwATXnAi1ZFyIVIzTZsppH87894ukfVpz6rX6zVm1cVk0U4JDOIITcOAcGnANTWiBAAVP8Awv1qP1ar1Z7z+jS1axcwB/YH18A9gDk+g=</latexit>

[v, →1]

<latexit sha1_base64="o4DNgWSeOuW2e8Z1i54lABtINFU=">AAACBHicbVC7TsNAEDyHVwgvAyXNiQiJAiIboUAZQUMZJPKQEis6XzbhlPPZultHiqy0fAUtVHSIlv+g4F+wjQsITDWa2dXOjh9JYdBxPqzS0vLK6lp5vbKxubW9Y+/utU0Yaw4tHspQd31mQAoFLRQooRtpYIEvoeNPrjO/MwVtRKjucBaBF7CxEiPBGabSwLZ7/YDhvRkl0/kJPXW9gV11ak4O+pe4BamSAs2B/dkfhjwOQCGXzJie60ToJUyj4BLmlX5sIGJ8wsbQS6liARgvyZPP6VFsGIY0Ak2FpLkIPzcSFhgzC/x0Mo+56GXif14vxtGllwgVxQiKZ4dQSMgPGa5FWgnQodCAyLLkQIWinGmGCFpQxnkqxmlHlbQPd/H7v6R9VnPrtfrtebVxVTRTJgfkkBwTl1yQBrkhTdIinEzJI3kiz9aD9WK9Wm/foyWr2Nknv2C9fwF+W5eK</latexit>

ignore!

Figure 1: PTMDP example. Dashed lines represent uncontrollable edges.

Running Example: Emergency Evacuation

FormIDEAble targets socio-critical systems, in which autonomous agents must coordinate with humans under uncertainty while respecting explicit safety constraints. FormIDEAble’s target applications are characterised by decision points at which multiple cooperative actions are available and the choice among them may affect human safety or the use of scarce resources [3]. Mass emergencies—such as fires, earthquakes, or terrorist attacks— require rapid and coordinated response to minimise harm. Alongside professional emergency services (first responders), ordinary people (zero responders) often play a crucial role in early response, particularly when professional resources are scarce [13]. Social identity dynamics may promote pro-social behaviour among survivors, but also introduce uncertainty, as not all individuals are equally willing or able to cooperate. We consider evacuation scenarios in which an autonomous agent acts as an active participant, supporting coordination between humans and professional responders. The autonomous agent must make localised decisions at runtime, such as assigning a rescue task to a survivor or contacting a first responder, while ensuring that safety requirements are not violated. Consider a search-and-rescue robot operating in a disaster zone. When the robot encounters a fallen person who cannot move independently, it must decide how to coordinate assistance. Possible actions include requesting help from a nearby survivor or contacting a first responder. The decision implies a trade-off between response time, availability of resources, and uncertainty about human compliance. Safety requirements may impose constraints such as maximum response time or prioritisation of vulnerable individuals. This example captures the challenges addressed by FormIDEAble: cooperation between an autonomous agent and humans, uncertainty arising from socially-driven behaviour, the presence of scarce resources, and urgency imposed by safety-critical conditions.

listen!

Preliminaries

This section introduces the minimal formal background required to understand how FormIDEAble models and synthesises sociallyaware, safety-constrained decisions. We omit full formal definitions for brevity and focus on the core modelling and synthesis concepts. Socio-critical decision-making problems require reasoning about four intertwined aspects: (i) control, as the autonomous agent selects among alternative actions; (ii) uncertainty, as human responses cannot be predicted deterministically; (iii) time, as actions incur delays and deadlines must be respected; and (iv) cost, as decisions affect performance metrics such as evacuation time or the use of scarce resources. To capture these aspects jointly, FormIDEAble models decision-making problems using PTMDPs [10].

A PTMDP is a stochastic transition system in which an autonomous agent (the controller) selects controllable actions, the environment responds probabilistically, and both time and cost accumulate along executions. Therefore, a PTMDP combines: (i) controllable actions chosen by the autonomous agent; (ii) probabilistic environment responses, capturing uncertain human behaviour; (iii) time constraints governing action durations; and (iv) accumulated costs representing performance objectives. Figure 1 shows an illustrative example of a PTMDP featuring a controller (the automaton on the left) and the agent reacting to the controller’s decisions (the automaton on the right). The controller must decide whether the agent moves or not. In the first case, the agent covers a distance but it spends energy. In the second case, the agent does not move but recovers energy. Due to uncertainty, there is a 20% probability that the agent will ignore the controller’ decision. A PTMDP consists of a finite set of locations ℓ ∈ 𝐿 representing system states connected by edges 𝑒 ∈ 𝐸. Edges are partitioned into controllable (modeling the autonomous agent selecting an action) and uncontrollable (modeling the environment responding probabilistically). Controllable edges are labeled with actions 𝑎 ∈ 𝐴𝑐 , determining the next location. When an uncontrollable edge fires, the environment selects an action 𝑎 ∈ 𝐴𝑢 according to a probability distribution, modelling uncertain human behaviour. Each location is annotated with time constraints (e.g., 𝑡 < 10) and a cost vector c (e.g., [v, −1], where v denotes the agent’s speed), capturing elapsed time or resource usage. This structure induces executions in which control alternates between the autonomous agent and the environment, while time and cost accumulate along the path. Strategies resolve controllable choices so as to optimise a cost objective subject to safety constraints. A strategy is a stochastic function 𝜎 : 𝐿 × R ≥0 → D (𝐴𝑐 ), where 𝐿 is the set of locations, R ≥0 represents elapsed time, 𝐴𝑐 is the set of controllable actions, and D (𝐴𝑐 ) denotes a probability distribution over 𝐴𝑐 . FormIDEAble synthesises strategies by formulating decision-making as a cost-bounded reachability problem [10]. We denote as E[cost] the expected value of a cost metric, and as P (𝜓 ) the probability that property 𝜓 holds. Given a PTMDP, the goal is to compute a strategy for the autonomous agent that minimises an expected cost while ensuring that a designated safety condition is satisfied. Formally, we consider strategies 𝜎 that resolve controllable choices and optimise: min E|𝜎 [cost]

subject to

P |𝜎 (^𝐺 ∧ cost ≤ 𝐵) ≥ 𝑝,

where 𝐺 is a set of goal states satisfying a safety requirement, 𝐵 is a cost bound (e.g., a maximum response time), and 𝑝 is a required

FormIDEAble: Safe and Socially-aware Autonomous Systems

probability threshold. Operator ^ denotes reachability. This formulation highlights the trade-off between performance optimisation and safety guarantees addressed by FormIDEAble. In the evacuation scenario, 𝐺 may represent the fallen person receiving assistance within a given time bound, while the cost captures the duration of the rescue or the involvement of scarce first-responder resources. FormIDEAble relies on Uppaal Stratego for the synthesis of strategies for PTMDPs [11]. Uppaal Stratego provides automated support for computing strategies that optimise quantitative objectives under probabilistic and timing constraints, as well as Statistical Model Checking (SMC) to estimate the likelihood of satisfying safety properties (i.e., the value of P |𝜎 (^𝐺 ∧ cost ≤ 𝐵)).

FormIDEAble: A Framework for Safe and Socially-aware Autonomous Agents

This section presents FormIDEAble, focusing on how socially-aware and safety-constrained decisions are synthesised at runtime. Figure 2 provides an overview of the FormIDEAble framework, illustrating how socially-aware decision-making, formal modelling, and strategy synthesis are integrated. The figure highlights the main responsibilities of the framework components and their interactions. FormIDEAble’s architecture is structured as a MAPE-K loop with formal strategy synthesis at the core of the analysis and planning phases. This architectural solution enables FormIDEAble to support socially-aware cooperation decisions with explicit safety guarantees without imposing assumptions on perception, actuation, or control mechanisms. At a high level, FormIDEAble operates as a decisionsupport layer for an autonomous agent. It is activated when the Monitoring module detects a decision point, that is, a situation in which multiple cooperative actions are available and the choice among them may affect safety or performance. Data collection is assumed to be handled by existing perception components and are treated as external to FormIDEAble. Once invoked, FormIDEAble combines three classes of inputs stored in the Knowledge subsystem. First, field-collected data describe the current state of the environment, such as distances, availability of resources, or task urgency. Second, estimates of socially-driven human behaviour are obtained from identity predictors, which provide probabilistic information about how humans are likely to respond to cooperation requests. Third, safety requirements specify the constraints that must be satisfied by any admissible decision. These inputs are consumed by the Analysis module, whose components are responsible for constructing a formal PTMDP model representing the current decision context. The model captures the controllable choices available to the autonomous agent, uncertain human responses, and the relevant time and cost constraints. Based on this model, the Formal Game Solver component computes a strategy that optimises a performance objective while guaranteeing compliance with the specified safety requirements. The resulting strategy is then used by the Planning module to select the best action to be enacted by the Execution module. Low-level control and actuation are outside the scope of FormIDEAble and are handled by the autonomous agent itself. If the environment evolves or new decision points arise, the process can be repeated, leading to the construction of updated models and strategies.

Conference’17, July 2017, Washington, DC, USA

Detecting Decision Points (Monitoring). FormIDEAble is invoked when the autonomous agent encounters a decision point, that is, a situation in which multiple cooperative actions are available and the choice may affect safety or performance. At a decision point, FormIDEAble gathers three classes of inputs: (i) contextual information about the current system state (e.g., distances, availability of resources); (ii) information about the humans involved, including uncertainty estimates derived from social identity predictors; and (iii) safety requirements provided by stakeholders. These inputs are treated as parameters for the subsequent formal analysis. In the evacuation scenario, a decision point occurs when the autonomous agent detects a fallen person requiring assistance. The available actions include requesting help from a nearby survivor or contacting a first responder. Contextual inputs include distances and response times, while uncertainty arises from the unknown willingness of a survivor to comply with the request. Safety requirements may constrain the maximum allowable time before assistance is provided. FormIDEAble relies on an identity predictor to estimate the likelihood that a human will comply with a cooperation request. The identity predictor (stored in the Knowledge) takes as input observable identity markers (e.g., demographic or contextual cues such as utterances) and estimates the probability of social identity adoption. Therefore, the Monitoring module also features a predictor training and update mechanism. As new interaction data becomes available, the Predictor Training Monitor periodically evaluates the accuracy of the current identity predictor. If performance degradation is detected, a Identity Predictor Builder retrains the model using the latest data and updates the predictor stored in the shared knowledge base. Generating a Verified Optimal Strategy (Analysis). Given the information collected at a decision point, the Formal Game Builder constructs a PTMDP that represents the local decision-making context faced by the autonomous agent. Model construction follows a template-based approach, in which reusable patterns capture recurring aspects of human-autonomous agent cooperation. Figure 3 depicts the modelling patterns the Formal Game Builder uses to construct the controller and environment components of a PTMDP. Each pattern captures a recurring aspect of socio-critical decision-making and can be instantiated and composed to represent a concrete decision context. Figure 3a shows the controller decision pattern, in which the autonomous agent selects one action from a finite set of controllable alternatives (e.g., assigning a task to a survivor or to a first responder). These choices correspond to outgoing controllable edges and represent the points at which the autonomous agent exerts control. Figure 3b models actions that incur a time overhead, such as travel or task execution. The elapsing of time is constrained by parameters (e.g., minimum and maximum duration), allowing the model to capture deadlines and urgency. Figures 3c and 3d capture uncertainty in human behaviour. Fig. 3c represents unobservable adversarial decisions, where the human selects among alternative actions but the outcome is not directly observable by the autonomous agent (e.g., whether they have developed a social identity). Therefore, the humans’s biases towards unobservable actions (i.e., weights 𝑝ˆ1...𝑚 ) must be estimated through predictors, such as the Identity Predictor. Fig. 3d represents observable adversarial decisions, where the human’s choice is visible to the autonomous agent and influences subsequent choices. Together, these

Conference’17, July 2017, Washington, DC, USA

Lestingi et al.

<<subsystem>> Autonomous Agent

Autonomous Agent Embodiment

<<subsystem>> Execution Module

Execute Decision

Decision Executor

Actuators

<<subsystem>> Planning Module Get State

Best Decision Selector

State Estimator

<<subsystem>> Monitoring Module

Select Decision

Decision-making Monitor

Parameter Estimator

Build Game

Get Parameters

<<subsystem>> Analysis Module

Formal Game Builder

Train Model

Identity Predictor Builder

Predictor Training Monitor

Data Lookup

Predictor Lookup

<<creates>>

Solve Game

Requirement Lookup

Formal Game Solver

Strategy Lookup

<<creates>>

<<creates>> <<subsystem>> Knowledge

<<creates>>

«artifact» Field-collected Data

Sensors

«artifact» Safety Requirements

«artifact» Identity Predictor

«artifact» PTMDP

«artifact» Stochastic Strategy

Social Groups

Figure 2: FormIDEAble’s architecture (connectors in bold highlight the activation circuit of the main modules). C.ld [c] <latexit sha1_base64="whP00rsHvhOnudbGBlJedClmvnU=">AAACAHicbVC7TsNAEDyHVwivACXNiQiJyrIRCpQRaSiDRB5SYqLzZRNOOZ+tuzVSZKXhK2ihokO0/AkF/4JtXEDCVKOZXe3s+JEUBh3n0yqtrK6tb5Q3K1vbO7t71f2DjgljzaHNQxnqns8MSKGgjQIl9CINLPAldP1pM/O7D6CNCNUtziLwAjZRYiw4w1S6a9pyOAgY3ptxMpoPqzXHdnLQZeIWpEYKtIbVr8Eo5HEACrlkxvRdJ0IvYRoFlzCvDGIDEeNTNoF+ShULwHhJnnpOT2LDMKQRaCokzUX4vZGwwJhZ4KeTecJFLxP/8/oxji+9RKgoRlA8O4RCQn7IcC3SOoCOhAZEliUHKhTlTDNE0IIyzlMxTvuppH24i98vk86Z7dbt+s15rXFVNFMmR+SYnBKXXJAGuSYt0iacaPJEnsmL9Wi9Wm/W+89oySp2DskfWB/fVS2XDQ==</latexit>

<latexit sha1_base64="7u7g6ru1hVhxTQjsXLa5ctss4Gk=">AAAB/nicbVC7TsNAEDyHVwivACXNiQiJKrIRCpQRNJRBIg/JtqLzZRNOOdunuzVSZEXiK2ihokO0/AoF/4JtXEDCVKOZXe3sBEoKg7b9aVVWVtfWN6qbta3tnd29+v5Bz8SJ5tDlsYz1IGAGpIigiwIlDJQGFgYS+sH0Ovf7D6CNiKM7nCnwQzaJxFhwhpnkuV7I8N6MUz73h/WG3bQL0GXilKRBSnSG9S9vFPMkhAi5ZMa4jq3QT5lGwSXMa15iQDE+ZRNwMxqxEIyfFpnn9CQxDGOqQFMhaSHC742UhcbMwiCbLCIuern4n+cmOL70UxGpBCHi+SEUEopDhmuRlQF0JDQgsjw5UBFRzjRDBC0o4zwTk6ydWtaHs/j9MumdNZ1Ws3V73mhflc1UyRE5JqfEIRekTW5Ih3QJJ4o8kWfyYj1ar9ab9f4zWrHKnUPyB9bHNzYAlnQ=</latexit>

ap ! → Ac <latexit sha1_base64="AdngyeGbQkqt0Y1VHAWegT13c9E=">AAACEXicbVDLSgNBEJz1GeMr6lGE0SB4CruJxByjXjxGMImQhKV3bHVw9sFMrxCWnPwEv8KrnryJV7/Ag//i7hpQo3UqqrrprvIiJQ3Z9rs1NT0zOzdfWCguLi2vrJbW1jsmjLXAtghVqM89MKhkgG2SpPA80gi+p7Dr3RxnfvcWtZFhcEbDCAc+XAXyUgqgVHJLW30f6JoogZGbU0lJNNruy4AfusItle1Ko9qo1Wvcrtg5vokzJmU2RsstffQvQhH7GJBQYEzPsSMaJKBJCoWjYj82GIG4gSvspTQAH80gyWOM+G5sgEIeoeZS8VzEnxsJ+MYMfS+dzD41k14m/uf1YrpsDBIZRDFhILJDJBXmh4zQMu0H+YXUSATZ58jT9AI0EKGWHIRIxTgtrJj24Uym/0s61YpTr9RP98vNo3EzBbbJdtgec9gBa7IT1mJtJtgde2CP7Mm6t56tF+v1a3TKGu9ssF+w3j4B9HSd4w==</latexit>

a1 ! → Ac <latexit sha1_base64="VKTjNN72Ns2ihFJfzZ1gzdHYcpc=">AAACCHicbVC7TsNAEDyHVwiv8OhoDiIkqsgOKKQM0FCCRAAptqz1sQmnnB+6WyOBlR/gK2ihokO0/AUF/4IdIvGcajSzq52dIFHSkG2/WaWJyanpmfJsZW5+YXGpurxyZuJUC+yIWMX6IgCDSkbYIUkKLxKNEAYKz4PBYeGfX6M2Mo5O6SZBL4R+JHtSAOWSX11zQ6Arogx8Z7jhyojv+8Kv1ux6q9Haae5wu26P8EWcMamxMY796rt7GYs0xIiEAmO6jp2Ql4EmKRQOK25qMAExgD52cxpBiMbLRumHfCs1QDFPUHOp+EjE7xsZhMbchEE+WWQ1v71C/M/rptRreZmMkpQwEsUhkgpHh4zQMq8F+aXUSARFcuT59wI0EKGWHITIxTTvqZL34fz+/i85a9SdZr15sltrH4ybKbN1tsm2mcP2WJsdsWPWYYLdsnv2wB6tO+vJerZePkdL1nhnlf2A9foB4tmZbw==</latexit>

... <latexit sha1_base64="r3T3p2tMBRG+nWwczitJuSX31uA=">AAAB93icbVC7TsNAEDzzDOEVoKQ5ESFRRTZCgTKChjJIOImUWNH5sgmnnM/W3RopsvINtFDRIVo+h4J/4WxcQMJUo5kd7e6EiRQGXffTWVldW9/YrGxVt3d29/ZrB4cdE6eag89jGeteyAxIocBHgRJ6iQYWhRK64fQm97uPoI2I1T3OEggiNlFiLDhDK/mDUYxmWKu7DbcAXSZeSeqkRHtY+7I5nkagkEtmTN9zEwwyplFwCfPqIDWQMD5lE+hbqlgEJsiKY+f0NDUMY5qApkLSQoTfiYxFxsyi0E5GDB/MopeL/3n9FMdXQSZUkiIoni9CIaFYZLgWtgWgI6EBkeWXAxWKcqYZImhBGedWTG0tVduHt/j9MumcN7xmo3l3UW9dl81UyDE5IWfEI5ekRW5Jm/iEE0GeyDN5cWbOq/PmvP+Mrjhl5oj8gfPxDadAk1I=</latexit>

<latexit sha1_base64="c7jZS3gCrErCUkZ1W0nPzXDkrlc=">AAAB93icbVC7TsNAEDyHVwivACXNiQgJUVg2QoEygoYySDiJlFjR+bIJp5zP1t0aKbLyDbRQ0SFaPoeCf8E2LiBhqtHMrnZ2glgKg47zaVVWVtfWN6qbta3tnd29+v5Bx0SJ5uDxSEa6FzADUijwUKCEXqyBhYGEbjC9yf3uI2gjInWPsxj8kE2UGAvOMJO8M1sO3WG94dhOAbpM3JI0SIn2sP41GEU8CUEhl8yYvuvE6KdMo+AS5rVBYiBmfMom0M+oYiEYPy3CzulJYhhGNAZNhaSFCL83UhYaMwuDbDJk+GAWvVz8z+snOL7yU6HiBEHx/BAKCcUhw7XIWgA6EhoQWZ4cqFCUM80QQQvKOM/EJKullvXhLn6/TDrnttu0m3cXjdZ12UyVHJFjckpcckla5Ja0iUc4EeSJPJMXa2a9Wm/W+89oxSp3DskfWB/fd06SkA==</latexit>

<latexit sha1_base64="1tFc3r9e+x9mNJ69yXL5BU5Slls=">AAACBXicbVC7TsNAEDyHVwgvB0qaExESVWQnKKSMoKEMUl5SEkXnyyaccn5wtwZFVmq+ghYqOkTLd1DwL9jGEhCYajSzq50dJ5BCo2W9G7mV1bX1jfxmYWt7Z3fPLO53tB8qDm3uS1/1HKZBCg/aKFBCL1DAXEdC15ldJH73FpQWvtfCeQBDl009MRGcYSyNzCIOJNwMXIbXehK1RvZiZJascr1Sr9aq1CpbKb6JnZESydAcmR+Dsc9DFzzkkmndt60AhxFTKLiERWEQaggYn7Ep9GPqMRf0MEqjL+hxqBn6NABFhaSpCD83IuZqPXedeDLNuOwl4n9eP8RJfRgJLwgRPJ4cQiEhPaS5EnEnQMdCASJLkgMVHuVMMURQgjLOYzGMSyrEfdjL3/8lnUrZrpVrV6elxnnWTJ4ckiNyQmxyRhrkkjRJm3ByRx7II3ky7o1n48V4/RrNGdnOAfkF4+0Tl+SY0A==</latexit>

t=0

C.lp [c] <latexit sha1_base64="WpXirehUuIVIR6VXYD8Usg19GWI=">AAAB+XicbVC7TsNAEDyHVwivACXNiQiJKrIRCpQRaSiDRB5SYkXnyyaccj6f7tZIkZWPoIWKDtHyNRT8C7ZxAQlTjWZ2tbMTaCksuu6nU1pb39jcKm9Xdnb39g+qh0ddG8WGQ4dHMjL9gFmQQkEHBUroawMsDCT0glkr83uPYKyI1D3ONfghmyoxEZxhKvVadTlK9GJUrbl1NwddJV5BaqRAe1T9Go4jHoegkEtm7cBzNfoJMyi4hEVlGFvQjM/YFAYpVSwE6yd53AU9iy3DiGowVEiai/B7I2GhtfMwSCdDhg922cvE/7xBjJNrPxFKxwiKZ4dQSMgPWW5E2gPQsTCAyLLkQIWinBmGCEZQxnkqxmkxlbQPb/n7VdK9qHuNeuPusta8KZopkxNySs6JR65Ik9ySNukQTmbkiTyTFydxXp035/1ntOQUO8fkD5yPb9FOk/Q=</latexit>

C.l1 [c] <latexit sha1_base64="UZHurrNHz5cG9nL+1FZNdN0gSCw=">AAAB+XicbVC7TsNAEDyHVwivACXNiQiJKrIRCpQRaSiDRB5SYkXryyaccn7obo0UWfkIWqjoEC1fQ8G/YBsXkDDVaGZXOztepKQh2/60SmvrG5tb5e3Kzu7e/kH18KhrwlgL7IhQhbrvgUElA+yQJIX9SCP4nsKeN2tlfu8RtZFhcE/zCF0fpoGcSAGUSr1WXY0SZzGq1uy6nYOvEqcgNVagPap+DcehiH0MSCgwZuDYEbkJaJJC4aIyjA1GIGYwxUFKA/DRuEked8HPYgMU8gg1l4rnIv7eSMA3Zu576aQP9GCWvUz8zxvENLl2ExlEMWEgskMkFeaHjNAy7QH5WGokgiw5chlwARqIUEsOQqRinBZTSftwlr9fJd2LutOoN+4ua82bopkyO2Gn7Jw57Io12S1rsw4TbMae2DN7sRLr1Xqz3n9GS1axc8z+wPr4Bm7ek7U=</latexit>

⇤.l1

t → T1

<latexit sha1_base64="Y54rw/XzQfeDbEoQqKT0L2h3wmA=">AAAB9XicbVDLSsNAFJ3UV62vqks3g0VwFRIpbV0IRTcuK9oHtKFMprd16OTBzI1SQj/Bra7ciVu/x4X/YhIDavWsDufcyz33uKEUGi3r3SgsLa+srhXXSxubW9s75d29jg4ixaHNAxmonss0SOFDGwVK6IUKmOdK6LrTi9Tv3oHSIvBvcBaC47GJL8aCM0ykazyzhuWKZdZPqw3LppZpZfgmdk4qJEdrWP4YjAIeeeAjl0zrvm2F6MRMoeAS5qVBpCFkfMom0E+ozzzQTpxFndOjSDMMaAiKCkkzEX5uxMzTeua5yaTH8FYveqn4n9ePcNxwYuGHEYLP00MoJGSHNFci6QDoSChAZGlyoMKnnCmGCEpQxnkiRkkppaQPe/H7v6RzYto1s3ZVrTTP82aK5IAckmNikzppkkvSIm3CyYQ8kEfyZNwbz8aL8fo1WjDynX3yC8bbJ6UtkiY=</latexit>

t → T2 <latexit sha1_base64="IzqCl3zV/z/WICO3xTP9C9nOK5g=">AAACBXicbVC7TsNAEDyHVwgvB0qaExESVWQnKKSMoKEMUl5SEkXnyyaccn5wtwZFVmq+ghYqOkTLd1DwL9jGEhCYajSzq50dJ5BCo2W9G7mV1bX1jfxmYWt7Z3fPLO53tB8qDm3uS1/1HKZBCg/aKFBCL1DAXEdC15ldJH73FpQWvtfCeQBDl009MRGcYSyNzCIOpnAzcBle60nUGlUWI7NkleuVerVWpVbZSvFN7IyUSIbmyPwYjH0euuAhl0zrvm0FOIyYQsElLAqDUEPA+IxNoR9Tj7mgh1EafUGPQ83QpwEoKiRNRfi5ETFX67nrxJNpxmUvEf/z+iFO6sNIeEGI4PHkEAoJ6SHNlYg7AToWChBZkhyo8ChniiGCEpRxHothXFIh7sNe/v4v6VTKdq1cuzotNc6zZvLkkByRE2KTM9Igl6RJ2oSTO/JAHsmTcW88Gy/G69dozsh2DsgvGG+fkWOYzA==</latexit>

[c]

(b) Action implying (a) Controller decisions. the elapsing of time. A.ld [c] <latexit sha1_base64="7VfhfnDYqShxx/apdhmzkmtuOfU=">AAACAHicbVC7TsNAEDyHVwivACXNiQiJyrIRCpQBGsogkYeUmOh82YRTzmfrbo0UWWn4Clqo6BAtf0LBv2AbF5Aw1WhmVzs7fiSFQcf5tEpLyyura+X1ysbm1vZOdXevbcJYc2jxUIa66zMDUihooUAJ3UgDC3wJHX9ylfmdB9BGhOoWpxF4ARsrMRKcYSrdXdhy0A8Y3ptRMpwNqjXHdnLQReIWpEYKNAfVr/4w5HEACrlkxvRcJ0IvYRoFlzCr9GMDEeMTNoZeShULwHhJnnpGj2LDMKQRaCokzUX4vZGwwJhp4KeTecJ5LxP/83oxjs69RKgoRlA8O4RCQn7IcC3SOoAOhQZEliUHKhTlTDNE0IIyzlMxTvuppH24898vkvaJ7dbt+s1prXFZNFMmB+SQHBOXnJEGuSZN0iKcaPJEnsmL9Wi9Wm/W+89oySp29skfWB/fUfWXCw==</latexit>

A.ld [c] <latexit sha1_base64="7VfhfnDYqShxx/apdhmzkmtuOfU=">AAACAHicbVC7TsNAEDyHVwivACXNiQiJyrIRCpQBGsogkYeUmOh82YRTzmfrbo0UWWn4Clqo6BAtf0LBv2AbF5Aw1WhmVzs7fiSFQcf5tEpLyyura+X1ysbm1vZOdXevbcJYc2jxUIa66zMDUihooUAJ3UgDC3wJHX9ylfmdB9BGhOoWpxF4ARsrMRKcYSrdXdhy0A8Y3ptRMpwNqjXHdnLQReIWpEYKNAfVr/4w5HEACrlkxvRcJ0IvYRoFlzCr9GMDEeMTNoZeShULwHhJnnpGj2LDMKQRaCokzUX4vZGwwJhp4KeTecJ5LxP/83oxjs69RKgoRlA8O4RCQn7IcC3SOoAOhQZEliUHKhTlTDNE0IIyzlMxTvuppH24898vkvaJ7dbt+s1prXFZNFMmB+SQHBOXnJEGuSZN0iKcaPJEnsmL9Wi9Wm/W+89oySp29skfWB/fUfWXCw==</latexit>

p1 a 1 ! → Au <latexit sha1_base64="ldOwiSBbVZuSconTO4ckBjocdnc=">AAAB/nicbVDLSsNAFJ3UV62vqks3g0VwVZJWapdFNy4r2Ac0pUymt3XoJBlmboQSCn6FW125E7f+igv/xSQG1OpZHc65l3vu8ZQUBm373SqsrK6tbxQ3S1vbO7t75f2DrgkjzaHDQxnqvscMSBFABwVK6CsNzPck9LzZZer37kAbEQY3OFcw9Nk0EBPBGSaS6/oMb80kVouRMypX7Gqz1qw36tSu2hm+iZOTCsnRHpU/3HHIIx8C5JIZM3BshcOYaRRcwqLkRgYU4zM2hUFCA+aDGcZZ5gU9iQzDkCrQVEiaifBzI2a+MXPfSyazjMteKv7nDSKcNIexCFSEEPD0EAoJ2SHDtUjKADoWGhBZmhyoCChnmiGCFpRxnohR0k4p6cNZ/v4v6daqTqPauD6rtC7yZorkiByTU+KQc9IiV6RNOoQTRR7II3my7q1n68V6/RotWPnOIfkF6+0TOo6Wdw==</latexit>

p̂1 <latexit sha1_base64="eXuh6nd1BPhpe4rcB3uIq9zZOpg=">AAACBnicbVDLTgJBEJz1ifhCPHqZSEw8kV0wyJHoxSMm8kiAkN6hgQmzj8z0GsmGu1/hVU/ejFd/w4P/4rKSqGidKlXd6epyQyUN2fa7tbK6tr6xmdnKbu/s7u3nDvJNE0RaYEMEKtBtFwwq6WODJClshxrBcxW23Mnl3G/dojYy8G9oGmLPg5Evh1IAJVI/l+96QGMzjLtjoDic9Z1ZP1ewi9VStVwpc7top/gmzoIU2AL1fu6jOwhE5KFPQoExHccOqReDJikUzrLdyGAIYgIj7CTUBw9NL06zz/hJZIACHqLmUvFUxJ8bMXjGTD03mUyTLntz8T+vE9Gw2oulH0aEvpgfIqkwPWSElkkpyAdSIxHMkyOXPheggQi15CBEIkZJS9mkD2f5+7+kWSo6lWLl+qxQu1g0k2FH7JidMoedsxq7YnXWYILdsQf2yJ6se+vZerFev0ZXrMXOIfsF6+0TtlaZdQ==</latexit>

p̂m a m ! → Au <latexit sha1_base64="Bt7qqD/7QxvVxEiBVlWt0wWoSx8=">AAACBnicbVDLTgJBEJz1ifhCPHqZSEw8kV0wyJHoxSMm8kiAkN6hgQmzj8z0GsmGu1/hVU/ejFd/w4P/4rKSqGidKlXd6epyQyUN2fa7tbK6tr6xmdnKbu/s7u3nDvJNE0RaYEMEKtBtFwwq6WODJClshxrBcxW23Mnl3G/dojYy8G9oGmLPg5Evh1IAJVI/l+96QGMzjLtjoDic9b1ZP1ewi9VStVwpc7top/gmzoIU2AL1fu6jOwhE5KFPQoExHccOqReDJikUzrLdyGAIYgIj7CTUBw9NL06zz/hJZIACHqLmUvFUxJ8bMXjGTD03mUyTLntz8T+vE9Gw2oulH0aEvpgfIqkwPWSElkkpyAdSIxHMkyOXPheggQi15CBEIkZJS9mkD2f5+7+kWSo6lWLl+qxQu1g0k2FH7JidMoedsxq7YnXWYILdsQf2yJ6se+vZerFev0ZXrMXOIfsF6+0TFCWZsQ==</latexit>

<latexit sha1_base64="q7ELO1w5TfbwmHCUru7xP6nskIk=">AAACEXicbVDLSgNBEJyNrxhfUY8ijAbBU9iNEnOMevEYwcRAEpbeSatDZh/M9Aqy5OQn+BVe9eRNvPoFHvwXd9eAzzoVVd10V3mRkoZs+80qTE3PzM4V50sLi0vLK+XVtY4JYy2wLUIV6q4HBpUMsE2SFHYjjeB7Cs+90XHmn1+jNjIMzugmwoEPl4G8kAIoldzyZt8HuiJKYOzmVFLij7f6MuCHbuyWK3a1UWvs1fe4XbVzfBFnQipsgpZbfu8PQxH7GJBQYEzPsSMaJKBJCoXjUj82GIEYwSX2UhqAj2aQ5DHGfCc2QCGPUHOpeC7i940EfGNufC+dzD41v71M/M/rxXTRGCQyiGLCQGSHSCrMDxmhZdoP8qHUSATZ58jT9AI0EKGWHIRIxTgtrJT24fxO/5d0alWnXq2f7leaR5NmimyDbbNd5rAD1mQnrMXaTLBbds8e2KN1Zz1Zz9bL52jBmuyssx+wXj8AC8md8g==</latexit>

a1 ! → Au <latexit sha1_base64="95BJ6n4d24oi7SRD5U3E3m2V+Wg=">AAACCHicbVC7TsNAEDyHVwiv8OhoDiIkqsgOKKQM0FCCRAAptqz1sQmnnB+6WyOBlR/gK2ihokO0/AUF/4IdIvGcajSzq52dIFHSkG2/WaWJyanpmfJsZW5+YXGpurxyZuJUC+yIWMX6IgCDSkbYIUkKLxKNEAYKz4PBYeGfX6M2Mo5O6SZBL4R+JHtSAOWSX11zQ6Arogx8Z7jhyojv+6lfrdn1VqO109zhdt0e4Ys4Y1JjYxz71Xf3MhZpiBEJBcZ0HTshLwNNUigcVtzUYAJiAH3s5jSCEI2XjdIP+VZqgGKeoOZS8ZGI3zcyCI25CYN8sshqfnuF+J/XTanX8jIZJSlhJIpDJBWODhmhZV4L8kupkQiK5Mjz7wVoIEItOQiRi2neUyXvw/n9/V9y1qg7zXrzZLfWPhg3U2brbJNtM4ftsTY7YseswwS7ZffsgT1ad9aT9Wy9fI6WrPHOKvsB6/UD/ueZgQ==</latexit>

A.l1 [c] <latexit sha1_base64="KhE8sV6ZH1LSJrXHACxoXe0V+Ew=">AAAB+XicbVC7TsNAEDyHVwivACXNiQiJKrIRCpQBGsogkYeUWNH6sgmnnB+6WyNFVj6CFio6RMvXUPAv2MYFJEw1mtnVzo4XKWnItj+t0srq2vpGebOytb2zu1fdP+iYMNYC2yJUoe55YFDJANskSWEv0gi+p7DrTW8yv/uI2sgwuKdZhK4Pk0COpQBKpe5VXQ0TZz6s1uy6nYMvE6cgNVagNax+DUahiH0MSCgwpu/YEbkJaJJC4bwyiA1GIKYwwX5KA/DRuEked85PYgMU8gg1l4rnIv7eSMA3ZuZ76aQP9GAWvUz8z+vHNL50ExlEMWEgskMkFeaHjNAy7QH5SGokgiw5chlwARqIUEsOQqRinBZTSftwFr9fJp2zutOoN+7Oa83ropkyO2LH7JQ57II12S1rsTYTbMqe2DN7sRLr1Xqz3n9GS1axc8j+wPr4Bmu0k7M=</latexit>

A.lm [c] <latexit sha1_base64="kqmKMrI1vWvymk22le3foF7YgGM=">AAAB+XicbVC7TsNAEDyHVwivACXNiQiJKrIRCpQBGsogkYeUWNH5sgmn3J2tuzVSZOUjaKGiQ7R8DQX/gm1cQMJUo5ld7ewEkRQWXffTKa2srq1vlDcrW9s7u3vV/YOODWPDoc1DGZpewCxIoaGNAiX0IgNMBRK6wfQm87uPYKwI9T3OIvAVm2gxFpxhKnWv6nKYqPmwWnPrbg66TLyC1EiB1rD6NRiFPFagkUtmbd9zI/QTZlBwCfPKILYQMT5lE+inVDMF1k/yuHN6EluGIY3AUCFpLsLvjYQpa2cqSCcVwwe76GXif14/xvGlnwgdxQiaZ4dQSMgPWW5E2gPQkTCAyLLkQIWmnBmGCEZQxnkqxmkxlbQPb/H7ZdI5q3uNeuPuvNa8LpopkyNyTE6JRy5Ik9ySFmkTTqbkiTyTFydxXp035/1ntOQUO4fkD5yPb8l0k+8=</latexit>

pn an ! → Au <latexit sha1_base64="rQMS5eUzUaj/EnVIByJleFvqUso=">AAAB/nicbVDLSgNBEJyNrxhfUY9eBoPgKewmEnMMevEYwTwgCWF20olDZmeHmV4hLAG/wquevIlXf8WD/+JmXVCjdSqquunq8rUUFl333cmtrK6tb+Q3C1vbO7t7xf2Dtg0jw6HFQxmars8sSKGghQIldLUBFvgSOv70cuF37sBYEaobnGkYBGyixFhwhonU7wcMb+041vOhGhZLbrleqVdrVeqW3RTfxMtIiWRoDosf/VHIowAUcsms7XmuxkHMDAouYV7oRxY041M2gV5CFQvADuI085yeRJZhSDUYKiRNRfi5EbPA2lngJ5NpxmVvIf7n9SIc1wexUDpCUHxxCIWE9JDlRiRlAB0JA4hskRyoUJQzwxDBCMo4T8QoaaeQ9OEtf/+XtCtlr1auXZ+VGhdZM3lyRI7JKfHIOWmQK9IkLcKJJg/kkTw5986z8+K8fo3mnGznkPyC8/YJmaGWtA==</latexit>

<latexit sha1_base64="xxUgeEKNM3lDoYv1bHIuB3sN6xM=">AAACCHicbVDLSgNBEJz1bXytD7x4GQ2Cp7CbQMwxxovHCMYEkrD0jq0Ozj6Y6RV0yQ/4FV4VBG/iVfwJD/ot7kbBZ52Kqm66uvxYSUOO82KNjI6NT0xOTRdmZufmF+zFpUMTJVpgS0Qq0h0fDCoZYoskKezEGiHwFbb9s93cb5+jNjIKD+gixn4AJ6E8lgIokzx7pRcAnRKlMPDc9Z4M+Y6XeHbRKdXKtUq1wp2SM8QXcT9Jsb66/ybvGs9Nz37tHUUiCTAkocCYruvE1E9BkxQKB4VeYjAGcQYn2M1oCAGafjpMP+CbiQGKeIyaS8WHIn7fSCEw5iLws8k8q/nt5eJ/Xjeh41o/lWGcEIYiP0RS4fCQEVpmtSA/khqJIE+OPPtegAYi1JKDEJmYZD0Vsj7c39//JYflklstVffdYr3BPjDF1tgG22Iu22Z1tsearMUEu2TX7IbdWlfWvfVgPX6MjlifO8vsB6yndwZDnR8=</latexit>

<latexit sha1_base64="rgBgBZ5hhST2TP/LFfY/pRXJWb0=">AAACCHicbVC7TsNAEDzzDOEVHh3NQYREFdkBhZQBGkqQCImURNb6ssCJ89m6WyOBlR/gK2ihokO0/AUF/4IdIgGBqUYzu9rZCWIlLbnuuzMxOTU9M1uYK84vLC4tl1ZWz22UGIFNEanItAOwqKTGJklS2I4NQhgobAXXR7nfukFjZaTP6DbGXgiXWl5IAZRJfmm9GwJdEaUw8PVmV2p+4Cd+qexW6tX6bm2XuxV3iG/ijUiZjXDilz66/UgkIWoSCqzteG5MvRQMSaFwUOwmFmMQ13CJnYxqCNH20mH6Ad9OLFDEYzRcKj4U8edGCqG1t2GQTeZZ7biXi/95nYQu6r1U6jgh1CI/RFLh8JAVRma1IO9Lg0SQJ0eefS/AABEayUGITEyynopZH97493/JebXi1Sq1071y43DUTIFtsC22wzy2zxrsmJ2wJhPsjj2wR/bk3DvPzovz+jU64Yx21tgvOG+fYFuZvg==</latexit>

Figure 3: PTMDP patterns composing the controller and adversary models (topical elements of each pattern are in red). Solid lines are controllable edges, while the uncontrollable ones are dashed.

patterns allow FormIDEAble to model socially-driven uncertainty without assuming deterministic or perfectly rational behaviour. A complete PTMDP model is obtained by composing these patterns for the controller and one or more environment entities. Time constraints and cost rates are instantiated from contextual parameters obtained through perception and domain knowledge (i.e., through the Parameter Estimator component). Such parameters include, for example, distances between agents, expected task durations, and resource usage costs. More generally, the construction process yields a parametric PTMDP, where a set of parameters 𝑘 1, . . . , 𝑘𝑛 determines the size and quantitative characteristics of the model. By varying these parameters, the same modelling workflow can be used to generate different instances of a decision problem. Safety requirements are encoded as reachability goals 𝐺 and cost bounds 𝐵, as introduced in Section 3. Intuitively, 𝐺 characterises the set of admissible outcomes (e.g., successful task completion or prioritisation of vulnerable individuals), while 𝐵 constrains the maximum acceptable cost (e.g., response time or number of scarce

resource usages). The resulting PTMDP thus represents a finite, parameterised abstraction of the decision-making problem at hand. The Formal Game Solver generates a strategy by solving a costbounded reachability problem over the constructed PTMDP. Using Uppaal Stratego, a strategy 𝜎 is computed that minimises the expected cost while ensuring that the probability of satisfying the safety condition meets a threshold. Because safety constraints are embedded directly in the synthesis problem, any decision selected according to 𝜎 is guaranteed to comply with the specified safety requirements under the assumptions encoded in the model. Selecting and Executing the Best Decision (Planning and Execution). Once a strategy has been synthesised, the Planning module uses it to select the action to be enacted by the autonomous agent. The State Estimator identifies the location of the PTMDP that most closely represents the state of the physical system and the elapsed time. Given this pair in 𝐿 × R ≥0 , 𝜎 then prescribes a probability distribution over controllable actions. In practice, the Best Decision Selector picks the action with the highest probability (i.e., minimum expected cost) and the Decision Executor maps it to an executable command. In the evacuation scenario, this corresponds to issuing a request to a survivor or contacting a first responder. If the environment evolves or new information becomes available, the process can be repeated at subsequent decision points, yielding updated strategies.

Evaluation

This section reports on the preliminary empirical evaluation of the FormIDEAble framework applied to the mass emergency running example. The experiments evaluate FormIDEAble’s effectiveness in terms of how the generated strategies improve the performance while guaranteeing safety properties. We use two simulation environments for strategies generated through the FormIDEAble framework and compare them to four baseline conditions, (1) no autonomous agent supporting the emergency response (no-support), (2) always calling the first responders (staff-support), (3) always asking zero responders to help each other (survivor-support), and (4) an autonomous agent enacting decisions based on strategies generated by IDEA. Specifically, we address the following questions:

FormIDEAble: Safe and Socially-aware Autonomous Systems 700

Table 3: FormIDEAble’s accuracy when predicting whether the safety goal will hold compared against in-simulation observations.

600

FR calls

500

T_evac

Conference’17, July 2017, Washington, DC, USA

400 300 200

no-support

staff-support survivor-support

IDEA

FormIDEAble

20 15 10

Nfr

[150, 700]

[1, 30]

800

staff-support

IDEA

FormIDEAble

(a) UB = 10, Np ∈ [150, 700], Nfr = [1, 30]

UB 5 10 5 10

Precision 0.932 0.990 0.967 0.997

Recall 0.940 1.000 0.969 1.000

700 40

600

35 30

FR calls

T_evac

500 400

25 20 15

300

200

no-support

staff-support survivor-support

IDEA

FormIDEAble

staff-support

IDEA

FormIDEAble

(b) UB = 10, Np = 800, Nfr = 9

Figure 4: Evacuation time (Tevac ) and first-responder calls (FR_calls) distributions obtained with FormIDEAble (green), IDEA (blue), and the three baselines (yellow). Table 1: Statistical difference (p-value, effect size) between evacuation times (Tevac ) obtained with FormIDEAble compared to IDEA and the baselines. Np

Nfr

[150, 700] 800

[1, 30] 9

no-support < 0.05 (S) < 0.05 (L)

FormIDEAble vs. staff-support survivor-support 1.7E-01 (N) < 0.05 (N) 9.0E-01 (N) < 0.05 (M)

IDEA < 0.05 (N) < 0.05 S

Table 2: Statistical difference (p-value, effect size) between first-responder calls (FR_calls) obtained with FormIDEAble compared to IDEA and the staff-support baseline. Np

Nfr

[150, 700] 800

[1, 30] 9

FormIDEAble vs. staff-support IDEA < 0.05 (N) < 0.05 (N) < 0.05 (M) < 0.05 (M)

RQ1. How effective are FormIDEAble-generated strategies when deployed in an independently-developed simulation and how does FormIDEAble compare against the baselines? RQ2. How much does FormIDEAble support different safety properties and generate optimised strategies when deployed in Uppaal Stratego? RQ3. What is the time overhead induced by FormIDEAble? RQ4. How generalisable is FormIDEAble to socio-critical systems featuring the required factors?

5.1

RQ1: FormIDEAble in Action

The goal of this research question is to assess whether strategies synthesised by FormIDEAble are effective when deployed in an independently-developed simulator, and to compare their performance against IDEA. To this end, we evaluate FormIDEAble in IMPACT+, an agent-based model of emergency evacuation scenarios [17]. IMPACT+ features a rescue robot that, upon detecting a fallen person, must decide whether to request assistance from

a nearby survivor or to contact a first responder. The simulator is parameterised by the number of evacuees (Np ), the number of available first responders (Nfr ), and the maximum time Tfall a fallen person can wait before resuming evacuation autonomously. To ensure a fair comparison, both FormIDEAble and IDEA rely on the same Identity Predictor to estimate the probability that a survivor has developed a shared identity. The predictor is trained on interaction data collected from 100 IMPACT+ simulations and takes as input identity markers of both the survivor and the victim, yielding an estimate 𝑝ˆ𝑠𝑖 of shared identity adoption. We deploy synthesised strategies using 20 values of Tfall ∈ [30, 600] across two scenarios. The first samples Np ∈ [150, 700] and Nfr ∈ [1, 30] uniformly, while the second fixes Np = 800 and Nfr = 9, following the experimental setup of IDEA. Overall, this results in 4000 simulation runs. For each run, we measure the total evacuation time Tevac and the number of first-responder calls (FR_calls), comparing FormIDEAble against three baselines (nosupport, staff-support, survivor-support) and IDEA under identical simulation conditions. Statistical significance is assessed using the Mann–Whitney U test, with effect sizes reported via Vargha and Delaney’s 𝐴ˆ𝐴𝐵 statistic [30, 41]. We additionally evaluate FormIDEAble’s ability to predict whether a safety requirement will hold. Specifically, we compare the time predicted by the PTMDP model against the actual in-simulation time required to provide assistance, reporting precision and recall for different safety bounds UB. Results. Figure 4 reports the distributions of evacuation time and first-responder calls, while Tables 1 and 2 summarise statistical differences with respect to the baselines. Across configurations, FormIDEAble significantly outperforms the no-support baseline. When first responders are scarce (Np = 800, Nfr = 9), FormIDEAble also shows statistically significant improvements over IDEA and survivor-support in evacuation time, while remaining comparable to staff-support. FormIDEAble consistently reduces first-responder involvement compared to both staff-support and IDEA. Table 3 reports the accuracy of FormIDEAble in predicting whether the safety requirement can be satisfied. Precision and recall are always above 93%, indicating that the formal model provides a reliable estimate of safety satisfaction despite being deployed in an independent simulator.

5.2

RQ2: Trade-off between optimality and safety guarantees

This research question evaluates FormIDEAble’s ability to synthesise strategies under different specifications and decision-making contexts, beyond what can be represented in IMPACT+.

Conference’17, July 2017, Washington, DC, USA

Lestingi et al.

Table 4: FormIDEAble configurations selected to address RQ2. While the approach is agnostic with respect to the application domain, descriptors (i.e., distance and duration) are tailored to the evacuation example. Configuration

𝑁𝑠

𝑁𝑣

one-shot

with-memory

Parameters (𝑘 1..𝑛 )

Parameter Range (⊂ N)

Safety Goal (𝐺)

Reachability Property (𝜓 )

survivor-to-victim distance

[1, 20]

Task completion

Task completion and child prioritization

survivor-to-victim distance

[1, 20]

survivor-to-victim distance

{1, 11, 21}

maximum rescue action duration UB

Exp. Value of Task Duration p-value: <0.05, effect size: large

1.0

Task completion and child prioritization Task completion and action duration within threshold

{50, 40, 30}

Pr. of psi holding p-value: 6.0e-01, effect size: negligible

1.75 1.50 1.25 1.00 0.75 0.50 0.25 0.00

0.8

0.6

0.4

0.2

0.0

FormIDEAble

(a) 𝐺 : 10

Child prioritization Task completion and cap on first-responder calls

0.8

0.6

0.4

0.2

0.0

FormIDEAble

Pr. of psi holding p-value: <0.05, effect size: negligible

0.6 0.4 0.2

FormIDEAble

(a) UB = 50

𝑖=1 𝐴.𝑙𝑒𝑛𝑑,𝑖 . 1.0

1.0 0.8

FormIDEAble

Ô6

Exp. Value of Task Duration p-value: <0.05, effect size: small

Exp. Value of FR Calls p-value: <0.05, effect size: large

1.75 1.50 1.25 1.00 0.75 0.50 0.25 0.00

Pr. of psi holding p-value: <0.05, effect size: large

Exp. Value of FR Calls p-value: <0.05, effect size: large

Pr. of psi holding p-value: <0.05, effect size: small

1.0 0.8 0.6 0.4 0.2

FormIDEAble

(b) UB = 40 BL

FormIDEAble

1.75 1.50 1.25 1.00 0.75 0.50 0.25 0.00

(b) 𝐺 : v.age = child.

Figure 5: One-shot configuration results (Ns = 1, Nv = 2). Experiment Design. Table 4 summarises the configurations used to evaluate FormIDEAble. Each configuration is obtained by instantiating the modelling patterns with different numbers of survivors (𝑁𝑠 ), victims (𝑁 𝑣 ), and contextual parameters. In the one-shot configuration, a single decision is made to assist one of two victims when only one survivor is available. Model parameters vary the distance between the survivor and the victim, which affects both task duration and cost. In the with-memory configuration, multiple rescue tasks must be assigned over time with multiple survivors and victims. In addition to varying distances and time bounds, this configuration introduces a safety requirement that limits the number of first-responder interventions. The reachability property measures the probability that all rescue tasks are completed within a given time bound while respecting this constraint. For each configuration and point in the configuration’s parameter space, FormIDEAble synthesises a strategy 𝜎 that minimises task duration while guaranteeing a given safety goal 𝐺. In the one-shot configuration, we consider goals that require task completion or prioritisation of a child victim. In the with-memory configuration, the goal additionally constrains the number of first-responder calls. In all cases, SMC is used to estimate the probability that a reachability property 𝜓 holds under the synthesised strategy. All strategies are evaluated in Uppaal Stratego and compared against a nonstrategised baseline (BL) in which controllable actions are selected randomly with a uniform distribution. We assess the impact of strategy synthesis by comparing: (1) expected values of cost metrics and

Exp. Value of FR Calls p-value: <0.05, effect size: large

1.0

Pr. of psi holding p-value: 7.6e-01, effect size: negligible

0.8 0.6 0.4 0.2

FormIDEAble

Figure 6: With-memory configuration results (Ns = 5, Nv = 5).

(2) the probability of satisfying the reachability property 𝜓 , using the Mann–Whitney U test and Vargha and Delaney’s 𝐴ˆ𝐴𝐵 effect size. Results. Figures 5 and 6 summarise the results. In the one-shot setting (Ns = 1, Nv = 2), FormIDEAble significantly reduces task duration when only termination is required, but does not consistently improve the probability of rescuing the child. When child prioritisation is explicitly enforced as a safety goal, the synthesised strategy substantially increases the probability of satisfying 𝜓 , at the cost of a modest increase in task duration. In the with-memory configuration, FormIDEAble consistently reduces the number of first-responder calls compared to the baseline across all safety bounds. As the time constraint becomes stricter, the probability of satisfying 𝜓 decreases for both approaches; however, FormIDEAble maintains comparable safety satisfaction while significantly reducing reliance on scarce resources (see Figures 6a–6c).

5.3

RQ3: Time Overhead

This research question aims at assessing the wall-clock time overhead induced by the deployment of FormIDEAble.

Wall-clock time [s]

FormIDEAble: Safe and Socially-aware Autonomous Systems 3.0 2.5 2.0 1.5 1.0 0.5 0.0

1 2

Ns × Nv

Conference’17, July 2017, Washington, DC, USA

Figure 7: Wall-clock time for RQ1 and RQ2 experiments for increasingly complex models (Ns × Nv ). Experiment Design. The analysis is carried out by clocking the time necessary to complete a FormIDEAble run with the configurations selected for RQ1 and RQ2. In this case, the alternative to deploying FormIDEAble is having the autonomous agent employ no strategy or choose an action randomly (serving as the baseline), for which the associated time overhead is approximated to 0. Experiments are performed on a machine running macOS Sonoma 14.5 with an Apple M3 processor and 24GB of memory. Verification is performed through Uppaal v.5.1.0. Results. Figure 7 reports the wall-clock time required to synthesise strategies for the configurations used in RQ1 and RQ2, with increasing FormIDEAble model size. Model size is measured by the number of individuals considered by the autonomous agent, expressed as Ns × Nv . Across all configurations, the synthesis overhead introduced by FormIDEAble is non-negligible compared to a zero-cost baseline. However, the overhead remains modest for small and medium-sized configurations, with average runtimes below 0.5s for up to two individuals and below 0.15s for single-individual decisions. The highest observed overhead (approximately 2.25s on average) corresponds to the most complex configurations explored in RQ2. These results indicate that FormIDEAble is suitable for scenarios where safety-critical decisions allow for limited deliberation time. Further scalability optimisations are left to future work.

5.4

RQ4: Generalisability

This research question examines the generalisability of FormIDEAble by grounding it in established evidence that social identity shapes cooperative behaviour across domains such as security, privacy, and healthcare [7, 34, 38]. To do so, we move from emergency evacuations as a running example and qualitatively analyse three distinct socio-technical domains to explore how FormIDEAble can generalise. The three case studies focus on healthcare cybersecurity (the Irish Health Service Executive (HSE) ransomware attack) [32], community-based care for vulnerable older adults (SERVICE) [4], and robotics/software engineering (RSE) [16]. For each of these cases, we present the socio-critical factors such as decision points under uncertainty, scarce resources, and fragmented group structures that motivate identity-aware autonomous support and frame future work needed to fully validate the approach. The three case studies demonstrate how identity dynamics influence coordination, resilience, and safety-critical decision-making. In the HSE case, a lack of clear ownership and preparedness contrasted with strong prosocial behaviour among local hospital teams, revealing how shared crisis identities can emerge and how identityaware agents could support decentralised yet coordinated responses.

In SERVICE, prior work shows that circles of support rely not only on practical assistance but also on psychologically meaningful identities, suggesting that FormIDEAble agents could reason about identity to guide collaborative and safe interventions. Finally, in RSE, identity-based game-theoretic models explain cooperation and sanctioning behaviours in teams such as open-source communities, enabling agents to design nudges that restore collaboration during incidents or failures. Taken together, these cases support the claim that FormIDEAble can generalise across socio-critical systems by leveraging shared identities to manage scarce resources, coordinate human–agent collaboration, and uphold safety-relevant properties. Implications for Software Engineering. Human-Autonomous System (AS) cooperation is increasingly advocated in software engineering whether through Software Engineering 2.0 [29] or AIware [20]. In this context, human and AS agents work together to carry out software engineering tasks such as code reviews. Achieving this vision requires going beyond automation alone [21] and understanding the behaviour of software practitioners. By coordinating group behaviour, FormIDEAble lays the foundation for collaboration between AS and humans. In particular, emergencies manifest themselves in software engineering through incidents, malicious or otherwise. AS have a potentially critical role in coordinating the incident response by enabling groups of developers (first responders) and users (zero responders) to collaborate to manage critical incidents (e.g., security incidents). We plan to explore the role of FormIDEAble in coordinating incident response of multiple groups of developers and users.

5.5

Threats to Validity

This section discusses current limitations and the threats to validity of the reported preliminary results, highlighting directions for future work. The current version of FormIDEAble requires manual effort in two key steps: (i) instantiating and composing PTMDP patterns to model a specific socio-critical decision-making context, and (ii) formalising safety requirements as reachability properties. While the underlying modelling and synthesis techniques are amenable to automation, the development of higher-level notations or tooling to support these tasks is left for future work. The empirical evaluation relies on simulation-based studies and formal analysis using Uppaal Stratego. While this allows controlled experimentation and reproducibility, it constitutes a threat to external validity. In particular, the behaviour of humans in realworld emergencies may deviate from the assumptions in IMPACT+. To address this limitation, future work will ground the probabilistic models of human behaviour on empirical data collected from real-world scenarios. In particular, datasets capturing crowd dynamics and human movement under constraints can be leveraged to calibrate and validate the parameters used in the PTMDP models. Furthermore, the evaluation focuses on a single application domain, namely emergency evacuation scenarios. Although this domain captures key characteristics of socio-critical systems, the results may not generalise directly to other settings without additional modelling effort. We plan to assess the generalisability of FormIDEAble across multiple socio-critical domains that share the same decision-making structure but differ in contextual features. Finally, scalability results are limited to the range of configurations

Conference’17, July 2017, Washington, DC, USA

explored in RQ3; larger models may require further optimisation or abstraction techniques.

Related Work

This section discusses related work along three research directions: human–ASs cooperation, trustworthiness of ASs, and safety in human–ASs cooperation. Human-Autonomous Systems Cooperation. A longstanding challenge in engineering ASs is coping with uncertainty arising from requirements, environments, other systems, and humans [44]. This work focuses on uncertainty stemming from human behaviour. In socio-critical systems, humans interacting with autonomous agents are not merely sources of input but first-class participants whose actions directly influence system decisions and outcomes [33]. Several approaches model human behaviour using behaviourist or probabilistic assumptions, treating actions as responses to stimuli [8, 22, 28]. Such models are widely adopted in human-in-the-loop systems, where humans intervene at predefined decision points [12]. Other work emphasises social adaptation, allowing ASs to update their behaviour based on user feedback or contextual changes [2], including in emergency-management settings [24]. With increasing autonomy, human-on-the-loop approaches treat humans as strategic supervisors overseeing autonomous planning and execution [15, 27]. While these approaches support coordination, they do not explicitly capture the social structures that shape cooperative human behaviour. To address this gap, research on joint action [37] and human– machine teaming [9, 18] emphasises the mutual understanding between humans and autonomous systems. The MAPE-K HMT framework leverages runtime models to support bidirectional adaptation between humans and machines. IDEA [17] further incorporates social identity theory to reason about cooperation between heterogeneous human groups. However, neither MAPE-K HMT nor IDEA provide formal guarantees that cooperative decisions satisfy safety constraints. FormIDEAble builds on social identity theory and gametheoretic interaction models, while additionally synthesising strategies that are safe by construction. Trustworthiness of Autonomous Systems in Emergencies. Empirical studies show that people tend to follow rescue robots during emergencies, even after observing incorrect robot behaviour [23, 35, 36, 42]. At the same time, the presence and behaviour of other humans significantly influence trust and compliance [31]. This raises concerns about overtrust and highlights the need for autonomous systems to behave in a manner that is not only trusted but trustworthy [1, 26]. In this context, ensuring that autonomous decisions are socially grounded and aligned with safety requirements is critical. FormIDEAble contributes to this goal by synthesising cooperation strategies that explicitly account for socially-driven uncertainty while guaranteeing safety properties. Safety of Human-Autonomous Systems Cooperation. Assurance has been a central concern in the development of autonomous systems [43], with formal methods playing a key role in guaranteeing requirement satisfaction. However, shared control and adaptive behaviour in socio-technical systems challenge traditional verification techniques, particularly in the presence of human variability and uncertainty [25]. Beyond functional safety,

Lestingi et al.

autonomous systems increasingly need to satisfy Social, Legal, Ethical, Empathetic, and Cultural requirements [1, 45]. Existing approaches address these challenges through alignment mechanisms such as cooperative inverse reinforcement learning [19] or by weakening human obligations via abstraction and controller synthesis [40]. FormIDEAble aims to balance formality and feasibility [5] by synthesising strategies that optimise quantitative objectives (e.g., evacuation time) while ensuring compliance with explicit safety properties. In summary, FormIDEAble lies at the intersection of these three research directions. It builds on prior work on human-autonomous agent cooperation by explicitly modelling socially-driven uncertainty, draws on insights from trustworthiness research by grounding autonomous decisions in socially-aware reasoning, and advances the state of the art in safety assurance by synthesising cooperation strategies with formal safety guarantees. Unlike existing approaches, which typically address these dimensions in isolation, FormIDEAble integrates them within a single strategy synthesis framework, enabling autonomous systems to coordinate with humans under uncertainty while complying with safety requirements.

Conclusion

This paper presents FormIDEAble, an approach for synthesising socially-aware cooperation strategies with explicit safety guarantees in socio-critical systems. The core contribution lies in modelling human-AS interaction as a PTMDP and formulating decisionmaking as a cost-bounded reachability problem, enabling the automated synthesis of strategies that balance performance objectives with safety constraints. Through simulation-based studies and formal analysis, we provide initial evidence of the feasibility and potential of this approach. This work establishes the foundational modelling and synthesis principles underlying FormIDEAble. Several extensions are required to develop this work into a mature solution. Future work includes: (1) deeper empirical validation across additional socio– critical domains, (2) systematic scalability analysis of strategy synthesis, and (3) improved support for modelling efforts, including higher-level specification of decision contexts and safety requirements. In addition, future work will investigate how uncertainty in social identity prediction propagates to safety guarantees and how richer classes of requirements beyond safety properties—such as normative requirements—can be integrated. In conclusion, this paper provides a principled approach for assured, socially-aware decision-making in autonomous agents and outlines a research agenda toward a comprehensive contribution.

Data Availability A replication package https://zenodo.org/records/13754285.

provided

at:

Acknowledgements This work was supported by the Engineering and Physical Sciences Research Council under grant numbers EP/V026747/1 and EP/R013144/1, and by Science Foundation Ireland under grant number 13/RC/2094_P2.

FormIDEAble: Safe and Socially-aware Autonomous Systems

References [1] Dhaminda B. Abeywickrama, Amel Bennaceur, Greg Chance, Yiannis Demiris, Anastasia Kordoni, Mark Levine, Luke Moffat, Luc Moreau, Mohammad Reza Mousavi, Bashar Nuseibeh, Subramanian Ramamoorthy, Jan Oliver Ringert, James Wilson, Shane Windsor, and Kerstin Eder. 2024. On Specifying for Trustworthiness. Commun. ACM 67, 1 (2024), 98–109. doi:10.1145/3624699 [2] Malik Almaliki, Funmilade Faniyi, Rami Bahsoon, Keith Phalp, and Raian Ali. 2014. Requirements-Driven Social Adaptation: Expert Survey. In Requirements Engineering: Foundation for Software Quality - 20th International Working Conference, REFSQ 2014, Essen, Germany, April 7-10, 2014. Proceedings (Lecture Notes in Computer Science, Vol. 8396). Springer, 72–87. doi:10.1007/978-3-319-05843-6_6 [3] Luciano Baresi, Matteo Camilli, Tommaso Dolci, and Giovanni Quattrocchi. 2024. A Conceptual Framework for Quality Assurance of LLM-based Socio-critical Systems. In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering. 2314–2318. [4] Amel Bennaceur, Avelie Stuart, Blaine A. Price, Arosha K. Bandara, Mark Levine, Linda Clare, Jessica Cohen, Ciaran McCormick, Vikram Mehta, Mohamed Bennasar, Daniel Gooch, Carlos Gavidia-Calderon, Anastasia Kordoni, and Bashar Nuseibeh. 2023. Socio-Technical Resilience for Community Healthcare. In TAS. ACM, 26:1–26:6. [5] Marcello M. Bersani, Matteo Camilli, Livia Lestingi, Raffaela Mirandola, Matteo G. Rossi, and Patrizia Scandurra. 2023. Towards Better Trust in Human-Machine Teaming through Explainable Dependability. In 20th International Conference on Software Architecture, ICSA 2023 - Companion, L’Aquila, Italy, March 13-17, 2023. IEEE, 86–90. doi:10.1109/ICSA-C57050.2023.00029 [6] Andreea Bobu, Dexter R. R. Scobee, Jaime F. Fisac, S. Shankar Sastry, and Anca D. Dragan. 2020. LESS is More: Rethinking Probabilistic Models of Human Behavior. In Intl. Conf. on Human-Robot Interaction. ACM, 429–437. doi:10.1145/3319502. 3374811 [7] Gül Çalikli, Mark Law, Arosha K. Bandara, Alessandra Russo, Luke Dickens, Blaine A. Price, Avelie Stuart, Mark Levine, and Bashar Nuseibeh. 2016. Privacy dynamics: learning privacy norms for social software. In Proceedings of the 11th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS@ICSE 2016, Austin, Texas, USA, May 14-22, 2016. ACM, 47–56. doi:10.1145/2897053.2897063 [8] Javier Cámara, Gabriel Moreno, and David Garlan. 2015. Reasoning about human participation in self-adaptive systems. In 2015 IEEE/ACM 10th International Symposium on Software Engineering for Adaptive and Self-Managing Systems. IEEE, 146–156. [9] Jane Cleland-Huang, Theodore Chambers, Sebastian Zudaire, Muhammed Tawfiq Chowdhury, Ankit Agrawal, and Michael Vierhauser. 2023. Human-Machine Teaming with Small Unmanned Aerial Systems in a MAPE-K Environment. ACM Trans. Auton. Adapt. Syst. (sep 2023). doi:10.1145/3618001 Just Accepted. [10] Alexandre David, Peter G Jensen, Kim Guldstrand Larsen, Axel Legay, Didier Lime, Mathias Grund Sørensen, and Jakob H Taankvist. 2014. On time with minimal expected cost!. In Automated Technology for Verification and Analysis. Springer, 129–145. [11] Alexandre David, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marius Mikucionis, and Jakob Haahr Taankvist. 2015. Uppaal Stratego. In Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science, Vol. 9035). Springer, 206–211. doi:10.1007/978-3-662-46681-0_16 [12] Rogério de Lemos. 2020. Human in the loop: what is the point of no return?. In SEAMS ’20: IEEE/ACM 15th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, Seoul, Republic of Korea, 29 June - 3 July, 2020. ACM, 165–166. doi:10.1145/3387939.3391597 [13] John Drury, Holly Carter, Chris Cocking, Evangelos Ntontis, Selin Tekin Guven, and Richard Amlôt. 2019. Facilitating collective psychosocial resilience in the public in emergencies: Twelve recommendations based on the social identity approach. Frontiers in public health 7 (2019), 141. [14] Douglas Eskins and William H. Sanders. 2011. The Multiple-Asymmetric-Utility System Model: A Framework for Modeling Cyber-Human Systems. In Intl. Conf. on Quantitative Evaluation of Systems. IEEE Computer Society, 233–242. doi:10. 1109/QEST.2011.38 [15] Joel E. Fischer, Chris Greenhalgh, Wenchao Jiang, Sarvapali D. Ramchurn, Feng Wu, and Tom Rodden. 2021. In-the-loop or on-the-loop? Interactional arrangements to support team coordination with a planning agent. Concurr. Comput. Pract. Exp. 33, 8 (2021). doi:10.1002/cpe.4082 [16] Carlos Gavidia-Calderon, Amel Bennaceur, Tamara Lopez, Anastasia Kordoni, Mark Levine, and Bashar Nuseibeh. 2023. Meet your Maker: A Social Identity Analysis of Robotics Software Engineering. In TAS. ACM, 44:1–44:5. [17] Carlos Gavidia-Calderon, Anastasia Kordoni, Amel Bennaceur, Mark Levine, and Bashar Nuseibeh. 2024. The IDEA of Us: An Identity-Aware Architecture for Autonomous Systems. ACM Trans. on Soft. Engineering and Methodology (2024). [18] Elena Corina Grigore, Kerstin Eder, Anthony G. Pipe, Chris Melhuish, and Ute Leonards. 2013. Joint action understanding improves robot-to-human object handover. In Proc. of the 2013 IEEE/RSJ International Conference on Intelligent Robots and Systems. 4622–4629. doi:10.1109/IROS.2013.6697021

Conference’17, July 2017, Washington, DC, USA

[19] Dylan Hadfield-Menell, Anca D. Dragan, Pieter Abbeel, and Stuart Russell. 2016. Cooperative Inverse Reinforcement Learning. CoRR abs/1606.03137 (2016). arXiv:1606.03137 http://arxiv.org/abs/1606.03137 [20] Ahmed E. Hassan, Dayi Lin, Gopi Krishnan Rajbahadur, Keheliya Gallaba, Filipe Roseiro Côgo, Boyuan Chen, Haoxiang Zhang, Kishanthan Thangarajah, Gustavo Ansaldi Oliva, Jiahuei (Justina) Lin, Wali Mohammad Abdullah, and Zhen Ming (Jack) Jiang. 2024. Rethinking Software Engineering in the Era of Foundation Models: A Curated Catalogue of Challenges in the Development of Trustworthy FMware. In SIGSOFT FSE Companion. ACM, 294–305. [21] Junda He, Christoph Treude, and David Lo. 2024. LLM-Based Multi-Agent Systems for Software Engineering: Vision and the Road Ahead. CoRR abs/2404.04834 (2024). [22] Joe E Heimlich and Nicole M Ardoin. 2008. Understanding behavior to understand behavior change: A literature review. Environmental education research 14, 3 (2008), 215–237. [23] Yuqin Jiang, Zhenlong Li, and Susan L Cutter. 2019. Social network, activity space, sentiment, and evacuation: what can social media tell us? Annals of the American Association of Geographers 109, 6 (2019), 1795–1810. [24] Kenneth Johnson, Javier Cámara, Roopak Sinha, Samaneh Madanian, and Dave Parry. 2021. Towards Self-Adaptive Disaster Management Systems. In 18th International Conference on Information Systems for Crisis Response and Management, ISCRAM 2021, Blacksburg, VA, USA, May 2021. ISCRAM Digital Library, 49–61. https://idl.iscram.org/show.php?record=2312 [25] Hadas Kress-Gazit, Kerstin Eder, Guy Hoffman, Henny Admoni, Brenna Argall, Rüdiger Ehlers, Christoffer Heckman, Nils Jansen, Ross A. Knepper, Jan Kretínský, Shelly Levy-Tzedek, Jamy Li, Todd D. Murphey, Laurel D. Riek, and Dorsa Sadigh. 2021. Formalizing and guaranteeing human-robot interaction. Commun. ACM 64, 9 (2021), 78–84. doi:10.1145/3433637 [26] John D Lee and Katrina A See. 2004. Trust in automation: Designing for appropriate reliance. Human factors 46, 1 (2004), 50–80. [27] Nianyu Li, Sridhar Adepu, Eunsuk Kang, and David Garlan. 2020. Explanations for human-on-the-loop: a probabilistic model checking approach. In SEAMS ’20: IEEE/ACM 15th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, Seoul, Republic of Korea, 29 June - 3 July, 2020. ACM, 181–187. doi:10.1145/3387939.3391592 [28] Nianyu Li, Javier Cámara, David Garlan, Bradley R. Schmerl, and Zhi Jin. 2021. Hey! Preparing Humans to do Tasks in Self-adaptive Systems. In 16th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS@ICSE 2021, Madrid, Spain, May 18-24, 2021. IEEE, 48–58. doi:10.1109/ SEAMS51251.2021.00017 [29] David Lo. 2023. Trustworthy and Synergistic Artificial Intelligence for Software Engineering: Vision and Roadmaps. In ICSE-FoSE. IEEE, 69–85. [30] Henry B Mann and Donald R Whitney. 1947. On a test of whether one of two random variables is stochastically larger than the other. The annals of mathematical statistics (1947), 50–60. [31] Mollik Nayyar and Alan R Wagner. 2019. Effective robot evacuation strategies in emergencies. In 2019 28th IEEE International Conference on Robot and Human Interactive Communication (RO-MAN). IEEE, 1–6. [32] PricewaterhouseCoopers (PwC). 2021. Conti Cyber Attack on the HSE: Independent Post Incident Review. Independent Post Incident Review HSE Publications. Health Service Executive (HSE), Ireland. https://www.hse.ie/eng/services/publications/ conti-cyber-attack-on-the-hse-full-report.pdf Commissioned by the HSE Board in conjunction with the CEO and Executive Management Team. [33] Salil Purandare, Urjoshi Sinha, Md Nafee Al Islam, Jane Cleland-Huang, and Myra B. Cohen. 2023. Self-Adaptive Mechanisms for Misconfigurations in Small Uncrewed Aerial Systems. In 18th IEEE/ACM Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS 2023, Melbourne, Australia, May 15-16, 2023. IEEE, 169–180. doi:10.1109/SEAMS59076.2023.00030 [34] Irum Rauf, Dirk van der Linden, Mark Levine, John N. Towse, Bashar Nuseibeh, and Awais Rashid. 2020. Security but not for security’s sake: The impact of social considerations on app developers’ choices. In ICSE ’20: 42nd International Conference on Software Engineering, Workshops, Seoul, Republic of Korea, 27 June 19 July, 2020. ACM, 141–144. doi:10.1145/3387940.3392230 [35] Paul Robinette, Wenchen Li, Robert Allen, Ayanna M Howard, and Alan R Wagner. 2016. Overtrust of robots in emergency evacuation scenarios. In 2016 11th ACM/IEEE international conference on human-robot interaction (HRI). IEEE, 101– 108. [36] Ibraheem Sakour and Huosheng Hu. 2016. Robot assisted evacuation simulation. In 2016 8th Computer Science and Electronic Engineering (CEEC). IEEE, 112–117. [37] Natalie Sebanz, Harold Bekkering, and Günther Knoblich. 2006. Joint action: bodies and minds moving together. Trends in cognitive sciences 10, 2 (2006), 70–76. [38] Avelie Stuart, Dmitri Katz, Clifford Stevenson, Daniel Gooch, Lydia Harkin, Mohamed Bennasar, Lisa Sanderson, Jacki Liddle, Amel Bennaceur, Mark Levine, et al. 2022. Loneliness in older people and COVID-19: applying the social identity approach to digital intervention design. Computers in Human Behavior Reports (2022), 100179.

Conference’17, July 2017, Washington, DC, USA

[39] Henri Tajfel. 2010. Social identity and intergroup relations. Vol. 7. Cambridge University Press. [40] Thein Than Tun, Amel Bennaceur, and Bashar Nuseibeh. 2020. OASIS: Weakening User Obligations for Security-critical Systems. In 28th IEEE International Requirements Engineering Conference, RE 2020, Zurich, Switzerland, August 31 September 4, 2020. IEEE, 113–124. doi:10.1109/RE48521.2020.00023 [41] András Vargha and Harold D Delaney. 2000. A critique and improvement of the CL common language effect size statistics of McGraw and Wong. Journal of Educational and Behavioral Statistics 25, 2 (2000), 101–132. [42] Alan R Wagner and Paul Robinette. 2015. Towards robots that trust: Human subject validation of the situational conditions for trust. Interaction studies 16, 1 (2015), 89–117. [43] Danny Weyns, Nelly Bencomo, Radu Calinescu, Javier Cámara, Carlo Ghezzi, Vincenzo Grassi, Lars Grunske, Paola Inverardi, Jean-Marc Jézéquel, Sam Malek, Raffaela Mirandola, Marco Mori, and Giordano Tamburrelli. 2019. Perpetual Assurances for Self-Adaptive Systems. CoRR abs/1903.04771 (2019). arXiv:1903.04771 http://arxiv.org/abs/1903.04771 [44] Danny Weyns, Radu Calinescu, Raffaela Mirandola, Kenji Tei, Maribel Acosta, Amel Bennaceur, Nicolas Boltz, Tomas Bures, Javier Camara, Ada Diaconescu, Gregor Engels, Simos Gerasimou, Ilias Gerostathopoulos, Sinem Getir Yaman, Vincenzo Grassi, Sebastian Hahner, Emmanuel Letier, Marin Litoiu, Lina Marsso, Angelika Musil, Juergen Musil, Genaina Nunes Rodrigues, Diego Perez-Palacin, Federico Quin, Patrizia Scandurra, Antonio Vallecillo, and Andrea Zisman. 2023. Towards a Research Agenda for Understanding and ManagingUncertainty in Self-Adaptive Systems. SIGSOFT Softw. Eng. Notes 48, 4 (oct 2023), 20–36. doi:10. 1145/3617946.3617951 [45] Sinem Getir Yaman, Ana Cavalcanti, Radu Calinescu, Colin Paterson, Pedro Ribeiro, and Beverley Townsend. 2023. Specification, Validation and Verification of Social, Legal, Ethical, Empathetic and Cultural Requirements for Autonomous Agents. CoRR abs/2307.03697 (2023). arXiv:2307.03697 doi:10.48550/ARXIV.2307. 03697

Lestingi et al.

Record · ID 324960 · SHA-256 cc94a4b52138bffb
Retrieved via Conceptio — every document is proof-bundled with source, license, and retrieval metadata.