時相論理
時間経過におtもなう真偽変化を扱う
計算機システムへの応用
遷移関係$ Rに従う状態列$ w_0,w_1,\cdotsは計算機の実行経路を表す
$ w_0が初期状態で、$ w_iRw_{i+1}が成り立つ
状態遷移の扱い方の違いから大きく2種類に分けられる
関連
参考
@lotz84_: Functional Reactive Programming と時相論理には対応があって、時相論理をプログラムに翻訳してFRPを実装するとどうなるか解説してる記事 この実装はスペースリークを起こす可能性があって Copy Applicative を用いて改善する方法を解説した記事
@lotz84_: 線形時相論理と Functional Reactive Programming のカリー＝ハワード同型対応から、それぞれのサブセットで対応する圏論的なセマンティクス（Fan Category）を考案しその性質を議論した論文