关系域中从样例学习概率时序安全性质

我们提出一个从标记为安全或不安全状态集合中学习概率计算树逻辑（pCTL）公式片段的框架。我们在关系设定下工作，并将关系马尔可夫决策过程的思想与 pCTL 模型检测相结合。更具体地，我们假设存在一个未知的关系 pCTL 目标公式，其仅被安全状态满足，且具有最大 $k$ 步的视界和阈值概率 $\alpha$。该任务随后由从被领域专家标记为安全或不安全状态中学习此未知公式构成。我们应用关系学习原理来归纳出一个被所有安全状态满足且不被任何不安全状态满足的 pCTL 公式。该公式随后可用作该域的安全规范，使系统能在未来避免陷入危险情形。遵循关系学习原理，我们引入了候选公式生成过程，以及判定哪个候选公式是给定标记状态的满意规范的方法。专家知晓与不知晓系统策略的情形均被处理，然而，多数学习过程对两种情形相同。我们在一个合成关系域上评估了我们的方法。