区間時相論理

区間時相論理（区間論理とも呼ばれる）は、時間間隔に関する命題論理と一階述語論理の両方を表現するための時相論理であり、逐次的および並列的な構成の両方を扱うことができる。区間時相論理は、状態の無限シーケンスを扱う代わりに、有限シーケンスを扱う。

区間時相論理は、コンピュータサイエンス、人工知能、言語学などの分野で応用されています。第一階区間時相論理は、1980年代にハードウェアプロトコルの仕様策定と検証のために開発されました。区間時相論理（ITL ）は、時相論理の一種で、ベン・モシュコフスキーがスタンフォード大学の学位論文のために開発したものです。^[1]コンピュータベースのシステムのハードウェアとソフトウェアの形式的な記述に有用です。このプロセスを支援するツールも利用可能です。Tempuraは実行可能なITLフレームワークを提供しています。ITLの設計において、 構成性は重要な課題であり、考慮すべき事項です。

区間時相論理の注目すべき派生としては、グラフィカル区間論理、符号区間論理、未来区間論理などがあります。

参照

• 持続計算
• 形式手法
• 行動の時間的論理

参考文献

1. 「区間時相論理」。