第二回 時制論理とリアルタイムリソース わんくま同盟 大阪勉強会 #44 自己紹介 • 名前 – 長月葵 • 職業 – プログラマ • 趣味嗜好 – 漫画/アニメ/ラノベ/論理学 わんくま同盟 大阪勉強会 #44 はじめに • 前回は様相論理の基本的な公理系まで説明 しました – 公理系のあたりはだいぶ駆け足だったのでポ カーン(゚д゚)だった人も多いかもしれませんが。。。 • 今回のトピックは時相論理と時間オートマトン とリアルタイムリソースです – リアルタイムリソースは時間の都合で割愛するか もです – 割愛しました わんくま同盟 大阪勉強会 #44 あらすじ • 前回のおさらい – 可能世界 – 様相論理 • 必然演算子 • 可能性演算子 • フレーム わんくま同盟 大阪勉強会 #44 あらすじ • 時相論理 (temporal logic) – 時点としての可能世界 • ある時点のモーダルオペレータ • ある時点からすべてのモーダルオペレータ – 時点の (全順序) 集合としての時間 – sinceとuntil わんくま同盟 大阪勉強会 #44 あらすじ – 分岐する時間CTL – 分岐する時間の特性 – パス式と状態式 – アクセス可能性 わんくま同盟 大阪勉強会 #44 あらすじ • オートマトン – オートマトンの概要 – 有限オートマトン – Buchiオートマトン – 時間オートマトン (timed automata) • 時間のモデル • 時間オートマトンのモデル • 時間オートマトンの状態遷移図例 • 次回予告 わんくま同盟 大阪勉強会 #44 前回のおさらい わんくま同盟 大阪勉強会 #44 可能世界 • 可能世界はある命題が成り立つ状況の集合 の元 – ようするに何かの起こる可能性それぞれを可能 世界と呼んでいる • 可能世界はアクセス可能性によって関係を持 つ – 可能世界すべてを認識できないとする。さらに観 測者はいずれかの可能世界に属するとしたとき 観測可能な世界をアクセス可能な世界と呼ぶ わんくま同盟 大阪勉強会 #44 様相論理 • 様相論理は命題論理の公理に加えて以下の規則を 持つ論理体系 – 命題φは全ての世界で成り立つことを表す演算子□ (必然 演算子) – 命題φが成り立つ世界が存在することを表す演算子◇ (可能性演算子) • 様相論理の公理系は都合に応じて選択していく – 採用する公理系を決定することは対象としたい論理体系 のシンタックスを決めることでもある – 具体的な公理系についての説明は割愛する。代表的なも のに関しては前回の資料を参照 わんくま同盟 大阪勉強会 #44 必然演算子 • 必然演算子は命題φが (アクセス可能な) す べての世界で成り立つことを表す – すべての可能世界にアクセス可能な神の視点で 考えるなら命題φは必ず成り立っている – 通常神の視点では考えないので命題φは様相に 応じて成り立たないこともある わんくま同盟 大阪勉強会 #44 可能性演算子 • 可能性演算子は命題φが成り立つ (アクセス 可能な) 世界が存在することを表す わんくま同盟 大阪勉強会 #44 フレーム • フレームは可能世界と関係のペア – 可能世界の集合をW={w_1,w_2,w_3,...}と置く – Wの元の間のアクセス可能関係を R={w_1Rw_2,w_1Rw_3,...}と置く – このとき〈W,R〉をフレームと呼ぶ わんくま同盟 大阪勉強会 #44 時相論理 (temporal logic) わんくま同盟 大阪勉強会 #44 前準備 • 時制論理は様相論理のわかりやすい応用の 一つ – 可能世界を時点と捉える – 時間の流れを一方通行のアクセス可能関係と捉 える • 時制論理での時間の扱いを述べる前に二項 関係と順序について整理しておく わんくま同盟 大阪勉強会 #44 二項関係 • 反射的 (reflexive) 任意のtでtRtが成り立つ • 非反射的 (inreflexive) 任意のtで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のいずれかである わんくま同盟 大阪勉強会 #44 順序 • 擬順序 (preorder) 関係が反射的かつ推移的 である • 反順序 (partial order) 関係が反射的かつ推 移的かつ反対称的である • 前順序 (total order) 関係が非反射的かつ推 移的かつ連結的である わんくま同盟 大阪勉強会 #44 時点としての可能世界 • 時制論理 (tense logic) では各々の時点を可 能世界で表す • アクセス可能関係は時間の方向を示すことに なる わんくま同盟 大阪勉強会 #44 ある時点のモーダルオペレータ • 時間の論理のフレームは〈T,≪〉であり、Tは時間の 点の集合、≪はその間の順序関係を表している • このフレーム上に過去と未来を表す以下の様な時制 のオペレータ定義する – Pφが真である⇔過去のある時点においてφが真である – Fφが真である⇔未来のある時点においてφが真である • フレームを用いて定義する – 【Pφ】=T iff ∃t'(t≫t'){【φ】^t'=T} – 【Fφ】=T iff ∃t'(t≪t'){【φ】^t'=T} わんくま同盟 大阪勉強会 #44 ある時点からすべてのモーダルオペレータ • 前ページで導入したPとFは「あるアクセス可能世界」 について述べている • 対して「すべてのアクセス可能世界」に相当する概念 も同様に導入することを考える – Hφが真である⇔過去のすべての時点においてφが真で ある – Gφが真である⇔未来のすべての時点においてφが真で ある • つまり – Hφ=¬P¬φ – Gφ=¬F¬φ わんくま同盟 大阪勉強会 #44 時点の (全順序) 集合としての時間 • 時制論理 (tense logic) で扱う時間は連続し た時点の集合として扱う • このとき時点を表す可能世界間のアクセス可 能性は時間の流れに相当する • このような構成で時間を扱う論理を時点によ る時制の論理 (instant tense logic) と呼ぶ わんくま同盟 大阪勉強会 #44 時点の (全順序) 集合としての時間 • ここまでの定義では時間の構造は順序集合と ならない • 次の公理を付け足すことで全順序を満たす – t≪t',t'≪t''ならばt≪t'' • つまり時点の関係は推移的であるということ – Fφ→G(φ∨Pφ∨Fφ) – Pφ→H(φ∨Pφ∨Fφ) • これは時間が分岐しないことを示している わんくま同盟 大阪勉強会 #44 sinceとuntil • ここまでの定義はPriorによるが、Prior tense logicではsinceとuntilが表現できない • 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}] • 未来のどこかでφとなるまでずっとψである わんくま同盟 大阪勉強会 #44 分岐する時間CTL • ここまでの時制論理では分岐する時間を扱わ ない • しかし我々が記述したい世界はある時点の状 態に応じて先の時間の様相が変わりうる世界 である • なので時間の分岐を織り込む • 分岐する時間の論理としてよく知られるCTL について述べる わんくま同盟 大阪勉強会 #44 分岐する時間の特性 • CTLで扱う時間は以下の特性を持つ物とする – 時間は離散的である – 時間の一コマを新たにstateと呼ぶ • stateの一つがnowに相当する – – – – – 過去は一直線の状態の連鎖である 過去には有限性がある (どこかに始まりがある) 未来は将来の可能性によって分岐しているものとする 未来は永遠に続く物とする ある任意の状態から始めて未来の分岐をw選択していっ た一本の道筋をパスと呼ぶ わんくま同盟 大阪勉強会 #44 パス式と状態式 • 状態式とは一つの時間に注目した時に全て の分岐を含んで正否を問われる式である – 式φが状態式として真であるとき世界wと状態tを 指定して〈w,t〉|= φと書く • パス式とは一つのパスに注目した時に正否を 問われる式である – 注目したパスは線型時間として扱えばよい – 式φがパスp=(t_1,t_2,...)でパス式として真である とき〈w,(t_1,t_2,...)〉|= φと書く わんくま同盟 大阪勉強会 #44 状態式の生成規則 • 状態式の生成式を述べる – (S1)全ての原始命題式は状態式である – (S2)φ,ψが状態式ならば¬φとφ∧ψも状態式であ る – (S3)φが状態式ならばAφ,Eφは状態式である – (S4)φが状態式ならばB_iφ,D_iφ,I_iφも状態式で ある • ここでAφとEφは次のように分岐を定義する – Aφ 全てのパスでφが真 – Eφ どこかのパスでφが真 わんくま同盟 大阪勉強会 #44 パス式の生成規則 • パス式の定義は以下となる – (P0)φ,ψが状態式ならばXφ,φUψはパス式である • ここでX,Uの意味は次のように与えられる – Xφ 今のすぐ次の状態でφが成立する – φUψ 未来のどこかでψが成り立つまでφが成り 立つ わんくま同盟 大阪勉強会 #44 CTLの時相オペレータ • CTLでは(P0)と(S3)が交互に用いられることで状態 式が生成される事から時相オペレータは次の8種類 に限定される – – – – – – – – EXφ ある分岐で次の時点でφが成り立つ EFφ ある分岐でどこか未来でφが成り立つ EGφ ある分岐で未来でずっとφが成り立つ E(φUψ) ある分岐でψになるまでφである AXφ すべての分岐で次の時点でφが成り立つ AFφ すべての分岐でどこか未来でφが成り立つ AGφ すべての分岐で未来でずっとφが成り立つ A(φUψ) すべての分岐でψになるまでφである わんくま同盟 大阪勉強会 #44 オートマトン わんくま同盟 大阪勉強会 #44 オートマトンの概要 • オートマトンはコンピュータの動作を形式的に 表現するのに向いた数学的なモデルである – 本章では有限オートマトン、Buchiオートマトン、時 間オートマトンについて述べる わんくま同盟 大阪勉強会 #44 有限オートマトン • 有限オートマトンはイベント処理などを表すモ デルの一つである • 有限オートマトンの定義を以下に述べる – 有限オートマトンは以下の五つ組である • • • • • S 状態の空でない有限集合 (S≠?) S_0 初期状態の空でない集合 (S_0⊆S,S_0≠?) Σ ラベル (イベント) の有限集合 δ 遷移の集合 (δ⊆S×Σ×S) F 受理状態の集合 (F⊆S) わんくま同盟 大阪勉強会 #44 有限オートマトンの受理言語 • 有限オートマトンの動作は語 (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)で表す わんくま同盟 大阪勉強会 #44 Buchiオートマトン • 有限オートマトンは非決定的ではあるが珠里 状態へ遷移する。詰まり基本的には停止する • Buchiオートマトンは停止しない (対話的シス テムなど) を説明するモデルの一つである – Buchiオートマトンは有限オートマトンと同じ五つ 組からなる – しかしBuchiオートマトンと有限オートマトンでは受 理の考え方が異なる わんくま同盟 大阪勉強会 #44 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)で表す わんくま同盟 大阪勉強会 #44 時間オートマトン (timed automata) • Buchiオートマトンは時間を扱わない – 時間をカウントする変数を使うなどして表現可能 ではあるが、扱う時間が有限であるとは限らない ためその域を有限に抑えることが難しい – 最終の目的とするモデル検査を行うためには変 域や状態数は有限に留めなければならない • 以下では連続時間を表現できる時間オートマ トンについて述べる わんくま同盟 大阪勉強会 #44 時間のモデル • 時間は0以上の実数で表す • 時間変数の集合をXとする – このとき時間制約式θの集合TC(X)は次の式を含 む最小の集合である • x≪c 時間制約 (x∈X,c∈N,≪∈{≦,<}) • ¬θ ¬ • θ∨η 論理和 • 時間の単位は任意である わんくま同盟 大阪勉強会 #44 時間オートマトンのモデル • 時間オートマトンは次の条件を満たす六つ組 である – S 状態の空でない有限集合 (S≠?) – s_init 初期状態 (s_init∈S) – Σ イベントの有限集合 – X 時間変数の有限集合 – δ 遷移の集合 (δ⊆S×TC(X)×Σ×2^X×S) – I 不変述語 (I:S→TC(X)) わんくま同盟 大阪勉強会 #44 時間オートマトンの状態遷移図例 わんくま同盟 大阪勉強会 #44 次回予告 • まだ決めてませんが以下のどれかをやります – 一階述語論理とゲーデルの不完全性定理 – 二重否定の論理 – 時相論理 わんくま同盟 大阪勉強会 #44 次回予告 • 次回より後の回でやりたいと思っているもの – 内包論理 – 信念の論理 – 形式手法 わんくま同盟 大阪勉強会 #44
© Copyright 2024 ExpyDoc