自主决策系统的信念刻画

高自主系统（HAS）必须评估其所处情境并推导信念，并基于这些信念决定下一步行动。这些信念不仅基于 HAS 迄今所做的观测，还基于关于 HAS 运行世界的普遍认知。这些认知要么在设计中内建于 HAS，要么在其任务期间由可信来源提供。尽管其信念可能不精确且存在缺陷，HAS 仍须外推可能的未来，以评估其行动后果，进而自主做出决策。本文将以当前信念为最佳而始终选择动作的系统性形式化为自主决策系统。我们证明，给定应用领域、动态变化的知识库与一组 LTL 任务目标，可检验能否构建自主决策系统。此外，我们可综合出自主决策系统的信念形成机制。在形式化刻画中，我们采用面向安全关键 HAS 的信念框架，其中信念形成支持 HAS 的外推。