時相作用素
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2019/01/02 21:06 UTC 版)
時相論理では2種類の作用素を使用する。論理作用素と様相作用素（英語版）である。論理作用素は一般的な真理関数作用素である( ¬ , ∨ , ∧ , → {\displaystyle \neg ,\lor ,\land ,\rightarrow } )。線形時相論理や計算木論理で使用される様相作用素を以下に示す。 文字表記記号表記定義説明ダイアグラム二項演算 ϕ {\displaystyle \phi } U ψ {\displaystyle \psi } ϕ U ψ {\displaystyle \phi ~{\mathcal {U}}~\psi } ( B U C ) ( ϕ ) = ( ∃ i : C ( ϕ i ) ∧ ( ∀ j < i : B ( ϕ j ) ) ) {\displaystyle {\begin{matrix}(B\,{\mathcal {U}}\,C)(\phi )=\\(\exists i:C(\phi _{i})\land (\forall j<i:B(\phi _{j})))\end{matrix}}} Until: ψ {\displaystyle \psi } は現在あるいは未来の位置で有効で、 ϕ {\displaystyle \phi } はそれ以前の位置まで有効でなければならない。その位置で ϕ {\displaystyle \phi } は保持する必要はなくなる。 ϕ {\displaystyle \phi } R ψ {\displaystyle \psi } ϕ R ψ {\displaystyle \phi ~{\mathcal {R}}~\psi } ( B R C ) ( ϕ ) = ( ∀ i : C ( ϕ i ) ∨ ( ∃ j < i : B ( ϕ j ) ) ) {\displaystyle {\begin{matrix}(B\,{\mathcal {R}}\,C)(\phi )=\\(\forall i:C(\phi _{i})\lor (\exists j<i:B(\phi _{j})))\end{matrix}}} Release: ϕ {\displaystyle \phi } が真である最初の位置まで ψ {\displaystyle \psi } が真であるならば（またはそのような位置がないなら永久に）、 ϕ {\displaystyle \phi } は ψ {\displaystyle \psi } をリリースする。 単項演算 N ϕ {\displaystyle \phi } ∘ ϕ {\displaystyle \circ \phi } N B ( ϕ i ) = B ( ϕ i + 1 ) {\displaystyle {\mathcal {N}}B(\phi _{i})=B(\phi _{i+1})} Next: ϕ {\displaystyle \phi } は次の状態で有効でなければならない。（X は同義語的に使われる） F ϕ {\displaystyle \phi } ◊ ϕ {\displaystyle \Diamond \phi } F B ( ϕ ) = ( t r u e U B ) ( ϕ ) {\displaystyle {\mathcal {F}}B(\phi )=(true\,{\mathcal {U}}\,B)(\phi )} Finally: ϕ {\displaystyle \phi } は結局、有効となる必要がある。（将来のいずれかの時点で） G ϕ {\displaystyle \phi } ◻ ϕ {\displaystyle \Box \phi } G B ( ϕ ) = ¬ F ¬ B ( ϕ ) {\displaystyle {\mathcal {G}}B(\phi )=\neg {\mathcal {F}}\neg B(\phi )} Globally: ϕ {\displaystyle \phi } はその後ずっと有効である必要がある。 A ϕ {\displaystyle \phi } ∀ ϕ {\displaystyle \forall \phi } ( A B ) ( ψ ) = ( ∀ ϕ : ϕ 0 = ψ → B ( ϕ ) ) {\displaystyle {\begin{matrix}({\mathcal {A}}B)(\psi )=\\(\forall \phi :\phi _{0}=\psi \to B(\phi ))\end{matrix}}} All: ϕ {\displaystyle \phi } は現在状態から生ずる全てのパス上で有効である必要がある。 E ϕ {\displaystyle \phi } ∃ ϕ {\displaystyle \exists \phi } ( E B ) ( ψ ) = ( ∃ ϕ : ϕ 0 = ψ ∧ B ( ϕ ) ) {\displaystyle {\begin{matrix}({\mathcal {E}}B)(\psi )=\\(\exists \phi :\phi _{0}=\psi \land B(\phi ))\end{matrix}}} Exists: 現在状態から生じるパスの少なくとも1つで ϕ {\displaystyle \phi } が有効なものがある。 他の表現: 作用素 R は V で表記されることがある。 作用素 W は weak until を意味する。 f W g {\displaystyle fWg} は f U g ∨ G f {\displaystyle fUg\lor Gf} と等価である。 B( ϕ {\displaystyle \phi } ) が整論理式(wff)であれば、単項作用素は全て整論理式である。B( ϕ {\displaystyle \phi } ) と C( ϕ {\displaystyle \phi } ) が整論理式であれば、二項作用素は全て整論理式である。 論理体系によっては一部の作用素は表現できない。例えば、Temporal Logic of Actions では N 作用素は表現できない。
※この「時相作用素」の解説は、「時相論理」の解説の一部です。
「時相作用素」を含む「時相論理」の記事については、「時相論理」の概要を参照ください。
- 時相作用素のページへのリンク
