時相論理とCTL

LTTL

[]<> に○p(次の時刻でpが成立)と p until q (q が成立するまでずーっとp)を付け加えた論理をLTTL( Linear Time Temporal Logic )という。

任意のLTTL式はωオートマトンに変換することができる。

変数に対する量化記号を許すと QPTL と呼ばれる。

CTL

Computational Tree Logic は、非決定性を含む計算に対して、計算の経路を含む状況を記述する。

非決定性は入力の非決定性による。

    EF p requires that there exists a path starting from a state, such that property p holds in a future time 
    AF p requires that for all paths starting from a state, property p holds in a future time 
    EG p requires that there exists a path starting from a state, such that property p holds in all future time instants 
    AG p requires that for all paths starting from a state, property p holds in all future time instants