|
127
|
1 -title: 時相論理とCTL
|
|
|
2
|
|
|
3 --LTTL
|
|
|
4
|
|
|
5 []<> に○p(次の時刻でpが成立)と p until q (q が成立するまでずーっとp)を付け加えた論理をLTTL( Linear Time Temporal Logic )という。
|
|
|
6
|
|
|
7 任意のLTTL式はωオートマトンに変換することができる。
|
|
|
8
|
|
|
9 変数に対する量化記号を許すと QPTL と呼ばれる。
|
|
|
10
|
|
|
11 --CTL
|
|
|
12
|
|
|
13 Computational Tree Logic は、非決定性を含む計算に対して、計算の経路を含む状況を記述する。
|
|
|
14
|
|
|
15 非決定性は入力の非決定性による。
|
|
|
16
|
|
|
17 EF p requires that there exists a path starting from a state, such that property p holds in a future time
|
|
|
18 AF p requires that for all paths starting from a state, property p holds in a future time
|
|
|
19 EG p requires that there exists a path starting from a state, such that property p holds in all future time instants
|
|
|
20 AG p requires that for all paths starting from a state, property p holds in all future time instants
|
|
|
21
|
