Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Learning Probabilistic Temporal Logic Specifications for Stochastic Systems

Rajarshi Roy, Yash Pote, David Parker, Marta Kwiatkowska

TL;DR

This work tackles the challenge of learning probabilistic temporal specifications for stochastic systems by inferring PLTL^{+} formulas from positive and negative DTMCs. It introduces PriTL, a three-stage pipeline that combines grammar-based enumeration, probabilistic threshold search via model checking, and Boolean set cover to extract concise, interpretable PLTL^{+} specifications. The approach is supported by theoretical guarantees (soundness, completeness, minimality) and validated in two domains: learning from reinforcement-learning–driven strategies and distinguishing variants of probabilistic models. This framework enables automatic, compact temporal specifications that aid verification and policy analysis, and integrates with established tools such as PRISM for scalable probabilistic model checking.

Abstract

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.

Learning Probabilistic Temporal Logic Specifications for Stochastic Systems

TL;DR

This work tackles the challenge of learning probabilistic temporal specifications for stochastic systems by inferring PLTL^{+} formulas from positive and negative DTMCs. It introduces PriTL, a three-stage pipeline that combines grammar-based enumeration, probabilistic threshold search via model checking, and Boolean set cover to extract concise, interpretable PLTL^{+} specifications. The approach is supported by theoretical guarantees (soundness, completeness, minimality) and validated in two domains: learning from reinforcement-learning–driven strategies and distinguishing variants of probabilistic models. This framework enables automatic, compact temporal specifications that aid verification and policy analysis, and integrates with established tools such as PRISM for scalable probabilistic model checking.

Abstract

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.
Paper Structure (29 sections, 5 theorems, 7 equations, 4 figures, 1 table, 5 algorithms)

This paper contains 29 sections, 5 theorems, 7 equations, 4 figures, 1 table, 5 algorithms.

Table of Contents

  1. Introduction
  2. Related Work
  3. Learning Temporal Logics.
  4. Explaining RL policies
  5. Preliminaries
  6. Markov Chains and MDPs
  7. Probabilistic Linear Temporal Logic (PLTL)
  8. Passive Learning of PLTL$^{+}$ Formulas
  9. The Learning Algorithm
  10. Grammar-based Enumeration for LTL
  11. Probabilistic Threshold Search for PLTL
  12. Boolean Set Cover for PLTL$^{+}$
  13. Theoretical guarantees.
  14. Evaluation
  15. Learning from strategies in stochastic environment
  16. ...and 14 more sections

Key Result

Lemma 1

$\bigcup_{n\leq N'}\mathcal{F}_n$ computed by GBE consists of all semantically distinct formulas of size $\leq N'$ and depth $\leq D$.

Figures (4)

  • Figure 1: An illustration of an office-world environment with the following features: office $\circ$, coffee , and decoration $\ast$. The shaded part near is slippery and introduces stochasticity in the agent's movement. The positive example demonstrates a strategy where the agent $\triangle$ collects and delivers to $\circ$ while avoiding $\ast$, whereas the negative examples do not achieve this temporal task.
  • Figure 2: The high-level overview of the learning algorithm. The set $\mathcal{F}_n$ consists of formulas of size $n$, the set $\mathcal{D}_n$ consists of discarded formulas, and the set $\mathcal{B}_n$ consists of formulas for Boolean combinations. The procedures PTS and BSC output a consistent PLTL and PLTL$^{+}$ formula $\Phi^*$, respectively, if they find one.
  • Figure 3: Runtime comparison for strategies generated from varying formulas and varying sample sizes.
  • Figure 4: The MDP environment for the frozen lake task. Blue represents ice, $h$ are holes, $a$ and $b$ are lake camps, and the purple triangle is the start.

Theorems & Definitions (8)

  • Lemma 1
  • Lemma 2
  • proof
  • Lemma 3
  • Lemma 4
  • Theorem 1
  • proof
  • proof