除了标准的 LTL 运算之外，带过去信息的 LTL （pLTL）新增了两个基本运算符 $Y$ 和 $S$.

$ φ::= ⊤|⊥|p|¬ φ|φ ∧ φ|φ ∨ φ|X φ|φ U φ|Y φ|φ S φ, $

$Y$ 的“人话语义”是 "Yesterday"，即 上一时刻 $φ$ 成立。

$S$ 的“人话语义”是 "Since"，即 $a S b$ 意思是 $b$ 曾经 在某一时刻成立过，且自此之后 $a$ 一直成立。

同时派生出了一系列运算符：

$ O φ:= ⊤ S φ $

Once，表示 $φ$ 曾经成立过。

$ H φ:= ¬ O ¬ φ $

Historically，表示自古以来 $φ$ 一直成立。

$ φ \widetilde S ψ:= φ S ψ ∨ H φ $

Since 的弱化版本， $a \widetilde S b$ 表示 自从 $b$ 曾经 成立过之后 $a$ 一直成立，或者 $a$ 自古以来一直成立，也可以理解为“假设在史前时代，$b$ 成立过一下”的 $S$

$ φ B ψ:= ψ S (ψ ∧ φ) $

Before，$a B b$ 表示曾经有一时刻 $a$ 和 $b$ 同时成立，自此之后 $b$ 仍然成立（$a$ 可能成立或不成立）。

$ φ \widetilde B ψ:= ψ \widetilde S (ψ ∧ φ) $

Before 的弱化版本，“假设在史前时代，$ψ ∧ φ$ 成立过一下”的 $B$。

$ \widetilde Y := Yφ ∨ ¬Y⊤ $

Yesterday 的弱化版本，即 在 0 时刻总是成立 的 $Y$，或者说，“假设在 -1 时刻，$φ$ 成立”的 $Y$。

对 pLTL 公式的强化与弱化

我们观察到，$Y$，$S$，$B$ 这三个运算符各自有其强化和弱化版本。

利用对这些公式中运算符的强化和弱化，我们可以在判定某个序列是否符合一个公式时，通过对公式的强化和弱化避免回朔。

何时需要强化，何时需要弱化

$Y$，$S$，$B$ 及其弱化版本公式成立的前提条件

这些涉及到历史的公式的前提条件分别是：

  • $Y x$ 和 $\widetilde Y x$ 在之前看到过 $x$ 成立时才有可能成立
  • $a S b$ 在之前看到过 $b$ 成立时才有可能成立
  • $a \widetilde S b$ 在之前看到过 $a ∨ b$ 成立时才有可能成立
  • $a B b$ 在之前看到过 $a ∧ b$ 成立时才有可能成立
  • $a \widetilde B b$ 在之前看到过 $b$ 成立时才有可能成立

我们将把公式映射到对应前提条件的函数记为 $wc$。

在公式 $f$ 对序列 $w$ 进行判定时，我们可以维护一个集合 $C$，记录所有 前提条件成立的 涉及到历史的 $f$ 的子公式。

  • 一开始，这个集合为所有 $f$ 中为 弱化版本 的子公式。（显然，所有弱化版本的子公式的前提条件在 0 时刻都是天然成立的）

  • 对于下一时刻，对于每个 f 中涉及到历史的子公式，

    • 若其已经在集合中（说明前提之前已经被满足），则将其弱化，若如果这一时刻的序列满足这个弱化公式的“前提条件”，将其加入集合。
    • 否则，将其强化，若如果这一时刻的序列满足这个强化公式的“前提条件”，将其加入集合。

    弱化已经前提已经被满足的子公式原因是，我们从上面弱化版本的运算符的定义可以看到，我们可以将这些运算符看作 其对应的强化版本 的前提条件在“之前”被满足过的版本。 强化之前没有满足的子公式的原因是，如果这个子公式是一个弱化版本，且之前它的前提条件没有被满足，那么当前它和它的强化版本是等效的。

形式化地，在公式 $φ$ 对序列 $w$ 进行判定时，我们定义这样一个集合 $C$：

$$ C_0 = \{ψ ∈ \text{psf} (φ) | ψ = weaken(ψ)\} $$

$$ C_{t+1} = \{ψ ∈ \text{psf} (φ⟨C_t⟩) | w_{t} \models wc(ψ)\} $$

其中 $\text{psf}(φ)$ 指的是 $φ$ 中所有以 $Y,\widetilde Y,S,\widetilde S,B,\widetilde B$ 为根的子公式。

$weaken(ψ)$ 是 $ψ$ 的弱化版本。

$φ⟨C_t⟩$ 即上面提到的强化/弱化规则，即：

$$ a⟨C⟩ := a $$

$$ (op\ \psi) \langle C \rangle := \begin{cases} (op\ \psi \langle C \rangle)_W & \quad (op\ \psi \in C) \\ (op\ \psi \langle C \rangle)_S & \quad (\text{otherwise}) \end{cases} $$

$$ (\phi\ op\ \psi) \langle C \rangle := \begin{cases} (\phi\ op\ \psi \langle C \rangle)_W & \quad (\phi\ op\ \psi \in C) \\ (\phi\ op\ \psi \langle C \rangle)_S & \quad (\text{otherwise}) \end{cases} $$