概要

通常の論理を拡張して、みらいに関するある種の主張(assertion)を含むようにしたもの。このページでは主に並行プログラムにおけるTemporal logic (Linear Temporal Logic)についてまとめる。

$□$ : now and forever (常に) $◊$ : now or sometime in the future (最終的に、Eventually)

並行プログラム

$s_{0}, s_{1}, ... \in Σ$ : sequence of program states
- 以下の条件を満たしてstate transitionを起こす
  - Valid starting state: $s_{0}$ is possible program state
  - Transition: $i > 0$ について、 $s_{i}$ は $s_{i - 1}$ から $ready (s_{i - 1})$ に含まれる1つのアトミック処理によって引き起こされる
  - Fairness: $ready (s_{i})$ に含まれるアトミック処理 $a$ は、 $s_{j} (j > i)$ の実行にいつか含まれる
現在のステートのみから次の遷移可能なステート群が決まる

Temporal logicは、 $\land$ , $\lor$ , $\sim$ などの一般的な論理記号と $□$ , $◊$ からなる、Immediate Assertion(即時アサーション)から構築される
プログラムのステートにおける関数
記法
- $s ⊨ P$ : ステート $s$ において、即時アサーション $P$ が真である
  - 例: $s ⊨ x = 1$ はステート $s$ において $x = 1$ が満たされていることを示す
$s ⊨ a t A$ : プログラムの制御がステートメント $A$ の開始地点にある状態を示す ( $A$ は実行可能なプログラムのステートメント)
$s ⊨ in A$ : プログラムの制御が $A$ の開始地点あるいは内部の何処かにある状態を示す
$s ⊨ a f t er A$ : プログラムの制御が $A$ の直後にある状態を示す
- whileループのafterは、ループの条件式テスト地点にいることを示す
- Aがcobeginの中のステートメントの場合、cobegin全体が終了しているか、cobeginは実行中だがAは終わっている、という状態

プログラムの実行シーケンスにおける関数
記法
- $σ ⊨ P$ : プログラムの無限の実行シーケンス $σ$ においてtemporal assertion $P$ が真である
Immediate assertionsとの関連性:
- $σ ⊨ P$ if and only if $s_{0} ⊨ P$
時相演算子を使う場合
- $σ ⊨ □ P$ if and only if $\forall i \geq 0 : σ^{(i)} ⊨ P$
- $σ ⊨ ◊ P$ if and only if $\exists i \geq 0 : σ^{(i)} ⊨ P$

$P \supset □ Q$ (含意): if $P$ is true now, then $Q$ will always be true
$□ (I \supset □ I)$ (不変条件): if $I$ ever becomes true, then it will remain true forever
$□ (P \supset ◊ Q)$ : if $P$ ever becomes true, then $Q$ will be true at the same time or later
- $P ⇝ Q$ : $P$ leads $Q$ ともいう
$□ (P \supset Q) \supset (P ⇝ Q)$
$□ (P \land Q) \equiv (□ P \land □ Q)$
$(□ P \lor □ Q) \supset □ (P \lor Q)$
$◊ (P \lor Q) \equiv (◊ P \lor ◊ Q)$
$(□ P \land □ (P \supset Q)) \supset □ Q$
$◊ P \lor □ \sim P$ : Pは最終的に真になるか、永遠に偽でありつづけるかのどちらかである
$((P ⇝ Q) \land (Q ⇝ R)) \supset (P ⇝ R)$ : 推移律
$((P ⇝ R) \land (Q ⇝ R)) \supset ((P \lor Q) ⇝ R)$
$□ (P \lor Q) \supset (□ P \lor ◊ Q)$
$[(P \land □ Q) ⇝ R] \supset [(P \land □ Q) ⇝ (R \land □ Q)]$

以下が言えれば、推移律から $R ⇝ Q$ が言える

$P ⇝ (R_{1} \lor R_{2})$
$R_{1} ⇝ Q$
$R_{2} ⇝ Q$
Proof latticeの定義: A proof lattice for a program is a fnite directed acyclic graph in which each node is labeled with an assertion, such that
- There is a single entry node having no incoming edges (図の $P$ )
- There is a single exit node having no outgoing edges (図の $Q$ )
- If a node labeled $R$ has outgoing edges to nodes labeled $R_{1}, R_{2}, ..., R_{k}$ , then $R ⇝ (R_{1} \lor R_{2} \lor ... \lor R_{k})$ holds for the program
$A ⇝ B$ ということは、ある時点で $B$ がtrueの場合 $A$ もtrue

定理: If there is a proof lattice for a program with entry node labeled $P$ and exit node labeled $Q$ , then $P ⇝ Q$ is true for that program

以下のfairnessを前提に置く
- Atomic assignment axiom: for any atomic assignment statement $S$ : $at S ⇝ after S$
- while control flow axiom: For the statement $w$ : while < $b$ > do s: S od, $at w ⇝ (at s \lor after w)$
「悪いことが起こらない」というSafetyと「何かが最終的に起こる」というfairnessを組み合わせて、「なにか良いことが最終的に起こる」というlivenessを導く