第二回 時制論理とリアルタイムリソース

自己紹介 名前 長月葵 職業 プログラマ 趣味嗜好 漫画/アニメ/ラノベ/論理学

前回は様相論理の基本的な公理系まで説明しました はじめに 前回は様相論理の基本的な公理系まで説明しました 公理系のあたりはだいぶ駆け足だったのでポカーン(ﾟдﾟ)だった人も多いかもしれませんが。。。 今回のトピックは時相論理と時間オートマトンとリアルタイムリソースです リアルタイムリソースは時間の都合で割愛するかもです 割愛しました

あらすじ 前回のおさらい 可能世界 様相論理 必然演算子 可能性演算子 フレーム

時相論理 (temporal logic) 時点としての可能世界 時点の (全順序) 集合としての時間 sinceとuntil あらすじ ある時点のモーダルオペレータ ある時点からすべてのモーダルオペレータ 時点の (全順序) 集合としての時間 sinceとuntil

あらすじ 分岐する時間CTL 分岐する時間の特性 パス式と状態式 アクセス可能性

オートマトン 次回予告 オートマトンの概要 有限オートマトン Buchiオートマトン 時間オートマトン (timed automata) あらすじ オートマトン オートマトンの概要 有限オートマトン Buchiオートマトン 時間オートマトン (timed automata) 時間のモデル 時間オートマトンのモデル 時間オートマトンの状態遷移図例 次回予告

前回のおさらい

可能世界はある命題が成り立つ状況の集合の元 ようするに何かの起こる可能性それぞれを可能世界と呼んでいる 可能世界はアクセス可能性によって関係を持つ 可能世界すべてを認識できないとする。さらに観測者はいずれかの可能世界に属するとしたとき観測可能な世界をアクセス可能な世界と呼ぶ

様相論理は命題論理の公理に加えて以下の規則を持つ論理体系 命題φは全ての世界で成り立つことを表す演算子□ (必然演算子) 命題φが成り立つ世界が存在することを表す演算子◇ (可能性演算子) 様相論理の公理系は都合に応じて選択していく 採用する公理系を決定することは対象としたい論理体系のシンタックスを決めることでもある 具体的な公理系についての説明は割愛する。代表的なものに関しては前回の資料を参照

必然演算子は命題φが (アクセス可能な) すべての世界で成り立つことを表す すべての可能世界にアクセス可能な神の視点で考えるなら命題φは必ず成り立っている 通常神の視点では考えないので命題φは様相に応じて成り立たないこともある

可能性演算子は命題φが成り立つ (アクセス可能な) 世界が存在することを表す

フレームは可能世界と関係のペア 可能世界の集合をＷ={w_1,w_2,w_3,...}と置く Wの元の間のアクセス可能関係をR={w_1Rw_2,w_1Rw_3,...}と置く このとき〈W,R〉をフレームと呼ぶ

時相論理 (temporal logic)

時制論理は様相論理のわかりやすい応用の一つ 前準備 時制論理は様相論理のわかりやすい応用の一つ 可能世界を時点と捉える 時間の流れを一方通行のアクセス可能関係と捉える 時制論理での時間の扱いを述べる前に二項関係と順序について整理しておく

二項関係 反射的 (reflexive) 任意のtでtRtが成り立つ 非反射的 (inreflexive) 任意のｔでtRtが成り立たない 推移的 (transitive) t_1Rt_2かつt_2Rt_3ならばt_1Rt_3が成り立つ 対称的 (symmetric) t_1Rt_2ならばt_2Rt_1が成り立つ 非対称的 (asymmetric) t_1Rt_2ならばt_2Rt_1でない 反対称的 (anti-symmetric) t_1Rt_2かつt_2Rt_1ならばt_1=t_2 連結的 (connected) t_1Rt_2あるいはt_2Rt_1あるいはt_1=t_2のいずれかである

擬順序 (preorder) 関係が反射的かつ推移的である 反順序 (partial order) 関係が反射的かつ推移的かつ反対称的である 前順序 (total order) 関係が非反射的かつ推移的かつ連結的である

時制論理 (tense logic) では各々の時点を可能世界で表す アクセス可能関係は時間の方向を示すことになる 時点としての可能世界 時制論理 (tense logic) では各々の時点を可能世界で表す アクセス可能関係は時間の方向を示すことになる

時間の論理のフレームは〈T,≪〉であり、Tは時間の点の集合、≪はその間の順序関係を表している ある時点のモーダルオペレータ 時間の論理のフレームは〈T,≪〉であり、Tは時間の点の集合、≪はその間の順序関係を表している このフレーム上に過去と未来を表す以下の様な時制のオペレータ定義する Pφが真である⇔過去のある時点においてφが真である Fφが真である⇔未来のある時点においてφが真である フレームを用いて定義する 【Pφ】=T iff ∃t'(t≫t'){【φ】^t'=T} 【Fφ】=T iff ∃t'(t≪t'){【φ】^t'=T}

前ページで導入したPとFは「あるアクセス可能世界」について述べている ある時点からすべてのモーダルオペレータ 前ページで導入したPとFは「あるアクセス可能世界」について述べている 対して「すべてのアクセス可能世界」に相当する概念も同様に導入することを考える Hφが真である⇔過去のすべての時点においてφが真である Gφが真である⇔未来のすべての時点においてφが真である つまり Hφ=￢P￢φ Gφ=￢F￢φ

時制論理 (tense logic) で扱う時間は連続した時点の集合として扱う 時点の (全順序) 集合としての時間 時制論理 (tense logic) で扱う時間は連続した時点の集合として扱う このとき時点を表す可能世界間のアクセス可能性は時間の流れに相当する このような構成で時間を扱う論理を時点による時制の論理 (instant tense logic) と呼ぶ

ここまでの定義では時間の構造は順序集合とならない 次の公理を付け足すことで全順序を満たす 時点の (全順序) 集合としての時間 ここまでの定義では時間の構造は順序集合とならない 次の公理を付け足すことで全順序を満たす t≪t',t'≪t''ならばt≪t'' つまり時点の関係は推移的であるということ Fφ→G(φ∨Pφ∨Fφ) Pφ→H(φ∨Pφ∨Fφ) これは時間が分岐しないことを示している

ここまでの定義はPriorによるが、Prior tense logicではsinceとuntilが表現できない 【S(φ,ψ)】^t=T iff ∃t'≪t[【φ】^t=Tかつ∀t''{t'≪t''≪t →【ψ】^t''=T}] 過去φであってらそれ以降ずっとψである 【U(φ,ψ)】^t=T iff ∃t'≫t[【φ】^t=Tかつ∀t' {t ≪t''≪t'→【ψ】^t''=T}] 未来のどこかでφとなるまでずっとψである

ここまでの時制論理では分岐する時間を扱わない しかし我々が記述したい世界はある時点の状態に応じて先の時間の様相が変わりうる世界である 分岐する時間CTL ここまでの時制論理では分岐する時間を扱わない しかし我々が記述したい世界はある時点の状態に応じて先の時間の様相が変わりうる世界である なので時間の分岐を織り込む 分岐する時間の論理としてよく知られるCTLについて述べる

CTLで扱う時間は以下の特性を持つ物とする 分岐する時間の特性 CTLで扱う時間は以下の特性を持つ物とする 時間は離散的である 時間の一コマを新たにstateと呼ぶ stateの一つがnowに相当する 過去は一直線の状態の連鎖である 過去には有限性がある (どこかに始まりがある) 未来は将来の可能性によって分岐しているものとする 未来は永遠に続く物とする ある任意の状態から始めて未来の分岐をw選択していった一本の道筋をパスと呼ぶ

状態式とは一つの時間に注目した時に全ての分岐を含んで正否を問われる式である パス式と状態式 状態式とは一つの時間に注目した時に全ての分岐を含んで正否を問われる式である 式φが状態式として真であるとき世界wと状態tを指定して〈w,t〉|= φと書く パス式とは一つのパスに注目した時に正否を問われる式である 注目したパスは線型時間として扱えばよい 式φがパスp=(t_1,t_2,...)でパス式として真であるとき〈w,(t_1,t_2,...)〉|= φと書く

ここでAφとEφは次のように分岐を定義する 状態式の生成規則 状態式の生成式を述べる (S1)全ての原始命題式は状態式である (S2)φ,ψが状態式ならば￢φとφ∧ψも状態式である (S3)φが状態式ならばAφ,Eφは状態式である (S4)φが状態式ならばB_iφ,D_iφ,I_iφも状態式である ここでAφとEφは次のように分岐を定義する Aφ　全てのパスでφが真 Eφ　どこかのパスでφが真

パス式の定義は以下となる ここでX,Uの意味は次のように与えられる (P0)φ,ψが状態式ならばXφ,φUψはパス式である パス式の生成規則 パス式の定義は以下となる (P0)φ,ψが状態式ならばXφ,φUψはパス式である ここでX,Uの意味は次のように与えられる Xφ　今のすぐ次の状態でφが成立する φUψ　未来のどこかでψが成り立つまでφが成り立つ

CTLでは(P0)と(S3)が交互に用いられることで状態式が生成される事から時相オペレータは次の8種類に限定される EXφ　ある分岐で次の時点でφが成り立つ EFφ　ある分岐でどこか未来でφが成り立つ EGφ　ある分岐で未来でずっとφが成り立つ E(φUψ)　ある分岐でψになるまでφである AXφ　すべての分岐で次の時点でφが成り立つ AFφ　すべての分岐でどこか未来でφが成り立つ AGφ　すべての分岐で未来でずっとφが成り立つ A(φUψ)　すべての分岐でψになるまでφである

オートマトン

オートマトンはコンピュータの動作を形式的に表現するのに向いた数学的なモデルである オートマトンの概要 オートマトンはコンピュータの動作を形式的に表現するのに向いた数学的なモデルである 本章では有限オートマトン、Buchiオートマトン、時間オートマトンについて述べる

有限オートマトンはイベント処理などを表すモデルの一つである 有限オートマトンの定義を以下に述べる 有限オートマトンは以下の五つ組である S　状態の空でない有限集合 (S≠?) S_0　初期状態の空でない集合 (S_0⊆S,S_0≠?) Σ　ラベル (イベント) の有限集合 δ　遷移の集合 (δ⊆S×Σ×S) F　受理状態の集合 (F⊆S)

有限オートマトンの動作は語 (word) と呼ばれるラベルの列によって与えられる 有限オートマトンの受理言語 有限オートマトンの動作は語 (word) と呼ばれるラベルの列によって与えられる ラベルの列a_0,a_1,...a_(n-1)が有限オートマトンA=(S,S_0,Σ,δ,F)の語であるとは次の条件を満たす状態s_0,s_1,...,s_nが存在することである (s_0,a_0,s_1),(s_1,a_1,s2),...,(s_(n-1),a_(n-1),s_n)∈δ ここでs_0は初期状態である 最後の状態が受理状態 (S_n∈F) であるときその語a_0,a_1,...,a_(n-1)と状態s_0,s_1,...,s_nはオートマトンAによって受理されると言う また有限オートマトンAによって受理される全ての語の集合を受理言語と言いlang(A)で表す

有限オートマトンは非決定的ではあるが珠里状態へ遷移する。詰まり基本的には停止する Buchiオートマトン 有限オートマトンは非決定的ではあるが珠里状態へ遷移する。詰まり基本的には停止する Buchiオートマトンは停止しない (対話的システムなど) を説明するモデルの一つである Buchiオートマトンは有限オートマトンと同じ五つ組からなる しかしBuchiオートマトンと有限オートマトンでは受理の考え方が異なる

BuchiオートマトンB=(S,S_0,Σ,δ,F)の語であるとは次の条件を満たす状態s_0,s_1,...,s_nが存在することである (s_0,a_0,s_1),(s_1,a_1,s2),...,(s_i,a_i,s_(i+1)),...∈δ ここでs_0∈S_0は初期状態である また上の状態の列s_0,s_i,...,s_i,s_(i+1),...をBuchiオートマトンBの実行という 上記の遷移列の中にある受理状態s∈Fが無限回含まれているなら、その無限長の語と実行はBuchiオートマトンに受理されると言う またBuchiオートマトンBによって受理される全ての無限長の語の集合をlang_ω(B)で表す

時間オートマトン (timed automata) Buchiオートマトンは時間を扱わない 時間をカウントする変数を使うなどして表現可能ではあるが、扱う時間が有限であるとは限らないためその域を有限に抑えることが難しい 最終の目的とするモデル検査を行うためには変域や状態数は有限に留めなければならない 以下では連続時間を表現できる時間オートマトンについて述べる

時間は0以上の実数で表す 時間変数の集合をXとする 時間の単位は任意である 時間のモデル 時間は0以上の実数で表す 時間変数の集合をXとする このとき時間制約式θの集合TC(X)は次の式を含む最小の集合である x≪c　時間制約 (x∈X,c∈N,≪∈{≦,＜}) ￢θ　￢ θ∨η　論理和 時間の単位は任意である

時間オートマトンは次の条件を満たす六つ組である 時間オートマトンのモデル 時間オートマトンは次の条件を満たす六つ組である S　状態の空でない有限集合 (S≠?) s_init　初期状態 (s_init∈S) Σ　イベントの有限集合 X　時間変数の有限集合 δ　遷移の集合 (δ⊆S×TC(X)×Σ×2^X×S) I　不変述語 (I:S→TC(X))

時間オートマトンの状態遷移図例

まだ決めてませんが以下のどれかをやります 次回予告 まだ決めてませんが以下のどれかをやります 一階述語論理とゲーデルの不完全性定理 二重否定の論理 時相論理

次回より後の回でやりたいと思っているもの 次回予告 次回より後の回でやりたいと思っているもの 内包論理 信念の論理 形式手法