Autonomous systems are often applied in uncertain environments, which require prospective action planning and retrospective data evaluation for future planning to ensure safe operation. Formal approaches may support these systems with safety guarantees, but are usually expensive and do not scale well with growing system complexity. In this paper, we introduce online strategy synthesis based on classical strategy synthesis to derive formal safety guarantees while reacting and adapting to environment changes. To guarantee safety online, we split the environment into region types which determine the acceptance of action plans and trigger local correcting actions. Using model checking on a frequently updated model, we can then derive locally safe action plans (prospectively), and match the current model against new observations via reachability checks (retrospectively). As use case, we successfully apply online strategy synthesis to medical needle steering, i.e., navigating a (flexible and beveled) needle through tissue towards a target without damaging its surroundings.
翻译:自主系统往往在不确定的环境中应用,这需要为未来的规划制定行动规划并进行追溯性数据评估,以确保安全运作; 正式方法可能以安全保障支持这些系统,但通常费用昂贵,且与系统复杂性的日益复杂程度不相称; 在本文件中,我们根据传统战略综合进行在线战略综合,以便在对环境变化作出反应和适应的同时获得正式的安全保障; 为了保证在线安全,我们将环境分为区域类型,确定对行动计划的接受程度并触发地方纠正行动; 利用经常更新的模式进行示范检查,我们随后可以(不同地)制定地方安全行动计划,并通过可达性检查(反光检查)将现有模式与新观测模式相匹配。 使用这一案例,我们成功地将在线战略综合应用于医疗针头的定向,即通过(灵活和可动的)针头通过组织向目标行驶,而不会破坏周围环境。