FormIDEAble: Safe and Socially-aware Autonomous Systems
This work addresses the need for formally assured, socially-aware decision-making in socio-critical autonomous systems, bridging the gap between social dynamics and formal guarantees.
FormIDEAble synthesizes socially-aware cooperation strategies with formal safety guarantees for autonomous agents operating under uncertainty, demonstrated in an emergency evacuation scenario with initial experimental evidence of effectiveness.
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.