時相論理

時相論理(じそうろんり、Temporal Logic)

時間とともに真偽が変化するような文のこと

時間とともに変化する問題を扱う規則と体系

「私はいつも腹ペコだ」

「私はそのうち腹ペコになる」

「私は何かを食べるまで腹ペコだろう」

といった文を表現できる

時相論理では、時と共に真理値の変化する文を扱う。「私はいつも腹ペコだ」は時と共に真偽が変化する。そういう文を式として扱うことができる。

非時相論理では、時間経過によって真理値が変化しない文しか扱えない。

アルゴリズムのありとあらゆる「ライフタイム」(最初から最後まで)がシーケンスのさまざまな状態を互いに結びつける何かに従うことを検査する。

データベースで言うと、「常に整合性のとれた状態である」ことの検査と、「最終的に整合性がとれた状態になる」ことの検査の違いのようなもの

「口座の最終的な残高は開始時点の残高と同じである」要件が関連

確認用

Q. 時相論理

参考

関連