从随机系统轨迹中自动学习概率时序逻辑规范。
Learning Probabilistic Temporal Logic Specifications for Stochastic Systems
- 基于语法枚举与概率模型检验，推导简洁的概率时序逻辑表达式。
- 在强化学习策略和概率模型变体上验证，能准确捕捉时序差异。
- 适合做智能系统行为分析与形式化验证的研究者使用。
近年来，从样本轨迹中推断形式化行为规范（如线性时序逻辑）已取得显著进展。然而，现有方法难以处理具有随机行为的系统，这类系统在强化学习和形式化验证中十分常见。本文研究从一组被分类为正/负的马尔可夫链中被动学习布尔组合的概率线性时序逻辑（PLTL）公式的问题。提出一种新算法，结合语法枚举、搜索启发式、概率模型检验与布尔集合覆盖，高效生成简洁的PLTL规范。在两个应用场景中验证：从强化学习算法生成的策略中学习，以及从概率模型的不同变体中学习。结果表明，该方法能自动、高效地提取出精准刻画策略或模型变体间时序差异的PLTL规范。
原文摘要 · Abstract (English)
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, classified as either positive or negative. We propose a novel learning algorithm that infers concise PLTL specifications, leveraging grammar-based enumeration, search heuristics, probabilistic model checking and Boolean set-cover procedures. We demonstrate the effectiveness of our algorithm in two use cases: learning from policies induced by RL algorithms and learning from variants of a probabilistic model. In both cases, our method automatically and efficiently extracts PLTL specifications that succinctly characterise the temporal differences between the policies or model variants.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。