時相論理

Agda の方も、その段階まで来たらしく。

　　data LTTL ( V : Set )　: Set where
　　　　s :　V → LTTL V
　　　　○ :　LTTL V → LTTL V
　　　　□ :　LTTL V → LTTL V
　　　　⋄ :　LTTL V → LTTL V
　　　　_U_　:　LTTL V → LTTL　V → LTTL　V
　　　　t-not :　LTTL V → LTTL　V
　　　　_t\/_ :　LTTL V → LTTL　V → LTTL　V
　　　　_t/\_ :　LTTL V → LTTL　V → LTTL　V

　　{-# TERMINATING #-}
　　M : { V : Set } → (ℕ → V → Bool) → ℕ →　LTTL V　→ Set
　　M σ i (s x) = σ i x ≡ true
　　M σ i (○ x) = M σ (suc i) x
　　M σ i (□ p) = (j : ℕ) → i ≤ j → M　σ j p
　　M σ i (⋄ p) = ¬ ( M σ i (□ (t-not p) ))
　　M σ i (p U q) = ¬ ( ( j : ℕ) → i ≤ j → ¬ (M σ j q ∧ (( k : ℕ) → i ≤ k → k < j → M σ j p )) )
　　M σ i (t-not p) = ¬ ( M σ i p )
　　M σ i (p t\/ p₁) = M σ i p ∧ M σ i p₁
　　M σ i (p t/\ p₁) = M σ i p ∨ M σ i p₁

こんなものかな? 変な記号使わないといけないのがなぁ。いや、わかんない。もっと違う定義を使うかも知れないです。

Polymorphism ないから記号を使いまわせない。

Buchi / Muller automaton とか、自分のD論見直した方が良いかも。