TLA+が確認できることとできないこと

概要

• TLA+ は複雑な並行システム設計やバグ検出に優れるが、万能ではない
• 形式手法 の過大評価や誤解がネット上で広がっている現状
• TLA+が表現・検証できる特性 と、そもそも表現できない特性の整理
• 回避不能な限界 や、ハック的な回避策の実例
• 他手法との比較 や、TLA+の現実的な有効範囲のまとめ

TLA+で検証できること

• TLA+ は、システムを「状態の列（ビヘイビア）」として記述
  • 各状態で ブール式 による特性表現
• 3種類の時相演算子 を利用
  • []P（常にP） ：全ての未来状態でPが成り立つ
  • P'（Pプライム） ：次の状態でPが成り立つ
  • <>P（いつかP） ：現在または将来のどこかでPが成り立つ
• システムの特性（プロパティ） 定義
  • 例： []P は「全てのビヘイビアの初期状態でPが成り立つ」＝ 不変条件（インバリアント）
• アクションプロパティやバリアント の表現
  • 例： [](x' >= x) （xは単調増加）
  • [](P => P') （Pが成り立ったら以降ずっと成り立つ）
• 安全性（Safety） と 活性（Liveness） の検証
  • 安全性： 「悪いことが決して起きない」
  • 活性： 「良いことがいつか必ず起きる」
  • 例： []<>P （どの状態でも将来Pが成り立つ）
  • 例： <>[]P （いつかPが成り立ち、その後ずっと成り立つ）
  • 例： P ~> Q （Pが成り立ったらいつかQが成り立つ）

TLA+で表現できないこと

• 論理式として特性を定義できなければ検証不可
  • 例： 「鳥らしさ」 のような人間的直観は形式化不能
• 複数ステップにまたがる特性の直接表現が困難
  • 例：「削除→元に戻すで元の状態に戻る」など
  • 浮動小数点演算や実時間 も非対応、論理時間のみ
• 全てのビヘイビアに対する性質しか扱えない
  • 「あるビヘイビアでPが成り立つ（到達可能性）」 は表現不能
  • 例： 「ゲームがクリア可能」 など
• 複数ビヘイビア間の関係（ハイパープロパティ） は表現困難
  • 例： 「省エネモードの方が常に消費電力が少ない」
  • セキュリティや統計的特性（パーセンタイル応答時間など）も該当
• 状態空間全体に関する特性（メタプロパティ） も表現不能
  • 例：「状態XからYへの経路は1つだけ」など

TLA+の「できること」のハック

• 補助変数 で2ステップ特性を模倣可能
  • 例： state_history 配列で過去状態を記録し、インバリアント化
• 自己合成（self-composition） で一部ハイパープロパティを模倣
  • 各ビヘイビアを2つのビヘイビアの組み合わせとして表現
• TLCモデルチェッカー の新機能（REACHABLE, TLCGet）で一部到達可能性を検証
• フェアネスや機械的閉包 を利用した高度なハックも存在
• ただし、これらのハックは
  • モデルが複雑化・肥大化
  • 他のTLA+特性との相性が悪い
  • 本来のシステムとモデルが乖離
  • 組み合わせに弱く、拡張性が低い

他手法との比較・TLA+の現実的な活用範囲

• CTL ：到達可能性の直接検証が可能
• PRISM ：確率的特性の検証が可能
• それぞれTLA+が得意な分野では劣る
• 論理式で表現できない特性はどの手法でも検証不能
• TLA+はインバリアントや活性など「低い枝の果実」を効率的に拾える
• 万能ではなく限界を認識した上での活用が重要

まとめ

• TLA+は強力だが万能ではない
• 形式手法への過度な期待は禁物
• 何を表現・検証できて、何ができないかを理解することが重要
• ハック的手法は限定的な効果のみ
• 目的や特性に応じて適切なツール選択が必要