사회적으로 중요한 환경(socio-critical settings)에서 작동하는 자율 에이전트(Autonomous agents)는 명시적인 안전 제약 조건(safety constraints)을 준수하면서 불확실성 하에 인간과 협력해야 합니다. 기존의 접근 방식들은 공식적인 보증(formal guarantees) 없이 사회적 역학(social dynamics)을 고려하거나, 인간의 행동을 추상화하면서 공식적인 보증을 제공합니다. 우리는 안전 보증과 함께 사회적 인식을 갖춘 협력 전략을 합성(synthesising)하기 위한 공식적으로 근거를 둔 접근 방식인 FormIDEAble을 소개합니다. 인간과 자율 에이전트 간의 협력은 가격이 책정된 타이밍 마르코프 결정 과정(Priced Timed Markov Decision Process)으로 모델링되며, 의사 결정은 비용 제한 도달 가능성 문제(cost-bounded reachability problem)로 공식화됩니다. 우리는 비상 대피 시나리오를 사용하여 이 접근 방식을 설명합니다. 초기 실험 증거는 이 접근 방식의 효과를 입증하며 최적화(optimisation)와 안전 보증(safety guarantees) 사이의 트레이드오프(trade-offs)를 강조합니다. FormIDEAble은 사회적으로 중요한 시스템에서 공식적으로 보증된, 사회적 인식을 갖춘 의사 결정을 위한 원칙적인 토대를 제공합니다.