Learning Probabilistic Temporal Logic Specifications for Stochastic Systems
Rajarshi Roy, Yash Pote, David Parker, and Marta Kwiatkowska
在从样本轨迹中推断正式行为规范方面取得了实质性进展,例如使用线性时间逻辑(LTL)。 然而,这些技术无法处理正确描述具有随机行为的系统特征的规范,这些规范通常发生在强化学习和正式验证中。 我们考虑从一组马尔可夫链中推断概率LTL(PLTL)公式的布尔组合的被动学习问题,被归类为正或负。 我们提出了一种新的学习算法,该算法可以推断出简洁的PLTL规范,利用基于语法的枚举,搜索启发式,概率模型检查和布尔设置覆盖程序。 我们在两个用例中展示了我们算法的有效性:从RL算法诱导的策略中学习,并从概率模型的变体中学习。 在这两种情况下,我们的方法自动有效地提取PLTL规范,简明扼要地表征策略或模型变体之间的时间差异。
There has been substantial progress in the inference of formal behavioural specifications from sample trajectories, for example, using Linear Temporal Logic (LTL). However, these techniques cannot handle specifications that correctly characterise systems with stochastic behaviour, which occur commonly in reinforcement learning and formal verification. We consider the passive learning problem of inferring a Boolean combination of probabilistic LTL (PLTL) formulas from a set of Markov chains, clas...