時相論理とは？
じそうろんり
時相論理とは、「過去・現在・未来」にわたる命題の真偽の変化を扱うために、時間の概念を組み込んだ様相論理の一種です。
時相論理（じそうろんり、temporal logic）は、時間の流れに沿って命題の真偽がどのように変化するかを記述・推論するための論理体系です。通常の命題論理や述語論理は静的な真偽しか扱いませんが、時相論理では「いつかは（eventually）」「常に（always）」「次の時点で（next）」「〜が成立するまで（until）」といった時間的な様相を演算子として導入します。
代表的な時相演算子には次のものがあります。
- G（Globally / □）：「今後すべての時点で成り立つ」
- F（Finally / ◇）：「将来いつかは成り立つ」
- X（neXt）：「次の時点で成り立つ」
- U（Until）：「〜が成り立つまでの間ずっと別の条件が成り立つ」
時相論理は線形時間と分岐時間の二つの系統があります。線形時間時相論理（LTL）は時間の流れを一本の線として捉え、分岐時間論理（CTLなど）は未来が複数の可能性に分岐するモデルを採用します。
時相論理はコンピュータ科学において特に重要で、プログラムの振る舞いを形式仕様として記述し、モデル検査（model checking）によってシステムが安全性・活性条件を満たすかを自動検証するために広く活用されています。組込みシステム・通信プロトコル・ハードウェア設計などの分野で実用化されています。
使い方・例文
組込みシステムの安全検証において「ブレーキペダルが踏まれたら必ずいつかブレーキが動作する」という要求を時相論理のF演算子で記述し、自動検査する場面で使われます。
この用語をシェア
最終更新: