Jack of All Trades, Master of None

当ブログ最初の記事ですが, 初っ端から論文紹介です。

(挨拶記事だけ書いてブログに飽きるというジンクスを回避したい…)

以降も,こんな感じで面白いなと思った論文や記事の紹介,解説をしていく感じになると思います(続けば)

ざっくり説明するので,しっかり理解したい人は原文をどうぞ

Comparing LTL Semantics for Runtime Verification

概要

時相論理式のモデルは普通イベントの無限長の語
→対して, 実行時のイベントは有限長(利用可能なプレフィックスは増加するが)
実行時検査の観点から, 有限長のトレースの為のLTL由来の論理を再調査
結果として
→実行時検査用のLTL由来論理が満たすべき4つの公理を確立
→それらを全て満たす4値論理RV-LTLを導入
加えて, RV-LTLについて, ムーア機械を用いるモニタの構成を提案

1節導入

ある性質のモニタリングでは少なくとも3つの異なる状況がある

性質は続くステップとは独立に, 有限回のステップ後満たされる(true)
性質は以降何が続いても満たされない(false)
既に現れたプレフィックスではまだ判断出来ない(inconclusive)

[ABLS05, BLS06]ではこれらの状況に対応する有限トレース上の3値論理LTL3を提案した.

LTL3はsafety(e.g. Gp)とco-safety(e.g. Fp)のようなモニタ可能(monitorable)な性質については良くマッチしたが, モニタ不可能(non-monitorable)な性質(((e.g. G(r -> Fa))についてはその限りでない.そこで, request/acknowledge 性質((e.g. G(r->Fa)))に関する直感に基づき, inconclusiveの代わりに次の2つの値を入れたような論理を考える.

論理式 $\phi = G(r \rightarrow Fa)$ について

aで終わる有限長文字列は $\phi$ がおそらく満たされる事を表す真理値
rで終わる有限長文字列は $\phi$ が充足されなさそうであることを表す真理値

論文の構成

2節 : 議論の準備

3節 : 既存の3つのLTLベースの論理のおさらい

4節 : 実行時検査を目的とした時のこれら論理の有用性を議論

5節 : RV-LTLの導入と諸々の証明

6節 : RV-LTLモニタの構成

2節準備

真理領域

真理値はある種の束として解釈できる.有限束にはユニークな最小元( $\bot$ )と最大限( $\top$ )が存在する.例えば, $(\mathcal{L}, \sqsubseteq)=(\{\top, \bot\}, \{(\bot, \top)\})$ という束を考えれば、これはよく知られたBooleanに対応する(e.g. $\top\sqcup\bot=\top$ , $\top\sqcap\bot=\bot$ ).束 $\mathcal{L}$ が有限ド・モルガン束であるとき, $\mathcal{L}$ を真理領域(Truth domain)と呼ぶ.

無限トレース上のLTL

無限トレース $w=a_0a_1...\in\Sigma^{\omega}$ 上のLTL式の意味は関数 $[\_\models\_]_\omega : \Sigma^\omega\times LTL\rightarrow\mathcal{B}_2$ によって与えられる.

以降,この論文では,この真理領域や,LTLの文法,関数 $[\_\models\_]$ の定義を変更することで与えられる有限トレース上のLTLについての議論と比較をしている.

3節有限トレース上のLTL

3節では既存の有限トレース上のLTLについて紹介を兼ねていくつかの観点から比較をしている. 詳しくは原文を読んでもらうこととして, ここでは後の節の都合上最低限紹介が必要な２つを説明する.

FLTL

有限トレース上のLTLを考えるとき, X(Next)オペレータをどのように扱うかが問題になる.論理式 $X\phi$ は次の時点で $\phi$ が成り立つことを意味する時相演算子だが,たとえばトレース長が1であるとき,すなわち次の時点,というのが存在しない場合に $X\phi$ をどのように扱うのか,という問題である.FLTLでは,強いX(strong neXt),弱い $\overline{X}$ (weak neXt)という２つのXを導入することでこれを解決している. ここで, $X\phi$ は次の時点が存在しない場合,偽として評価され, $\overline{X}\phi$ は次の時点が存在しない場合真として評価される.

LTL3

$LTL_3$ では,文法は無限長のトレース上のLTLのものをそのまま用いますが,意味を与える関数の値域を3値に拡張します.具体的には $\top$ , $\bot$ の他に, $\bot \sqsubset ? \sqsubset \top$ となるような値?を加えます.この論理では, ある有限長のトレースuの上で論理式 $\phi$ が $\top$ ( $\bot$ )に評価されるのは,任意の無限長トレースが続いてもその判断が変わらない時, すなはち $\forall w\in\Sigma^\omega [uw\models \phi ] = \top(\bot)$ のようなとき, となります.続くトレースによって,真偽が変わるような場合には?がその論理式の値になります.したがってこの時,トレースの長さが足りない場合の $X\phi$ は?が割り当てられる事になります.

4節実行時検証用LTLの為の公理

実行時検証に用いるLTL風の論理が満たすべき性質のようなものを著者は次の4つの公理としてまとめている.

Existential Next (Nextの存在についての公理)

$[u\models X\phi]=\top \Rightarrow \begin{matrix} |u| \lt 1 \land [u^1\models\phi] \lor \\ |u|=1 \land \forall w\in\Sigma^\omega[w\models\phi]=\top\end{matrix}$

無限トレース上のLTLでは $[u\models X\phi]=\top$ と $[u^1\models\phi]=\top$ との間には,iffの関係が成り立つが,有限トレース上のLTLでは必ずしもそうでなければならないというのは厳しすぎるので,それを弱めた形で入れている.これはFLTLでもLTL3でも成り立つ.

Complementation by Negation (否定による補完)

任意の性質 $\phi$ 任意の語 $u$ について,

$[u\models\phi]=\overline{[u\models\neg\phi]}\land[u\models\phi]\neq[u\models\neg\phi]$

これは,2値論理では当然成り立っていそうな性質だが,非決定的な値を含むような論理では必ずしも成り立たない.実際,FLTLでは成り立つがLTL3では成り立たない.

Impartiality(公平性)

任意の性質 $\phi$ 任意の有限語 $u\in\Sigma^{*}$ について,

$[u\models\phi]=\top\Rightarrow\forall w\in\Sigma^\Omega [uw\models\phi]=\top$

$[u\models\phi]=\bot\Rightarrow\forall w\in\Sigma^\Omega [uw\models\phi]=\bot$

今度は打って変わって2値論理では満たすことの出来ない性質になっている.任意の有限語に対して $\top , \bot$ のいずれかを割り当てねばならないためである.当然2値論理であるFLTLはこれを満たさず,LTL3は満たしている.

Anticipation(予期)

任意の性質 $\phi$ 任意の有限語 $u\in\Sigma^{*}$ について

$[u\models\phi] =\top\Leftarrow\forall w\in\Sigma^\Omega[uw\models\phi]=\top$

$[u\models\phi] =\bot\Leftarrow\forall w\in\Sigma^\Omega[uw\models\phi]=\bot$

公平性とは逆の性質になっており,有限トレース上で判断できるものは判断されなければならないとしている.FLTLではこれは満たされないが,LTL3では満たされる.

5節 RV-LTL

4節で説明した4つの公理を全て満たすような有限トレース上のLTLとして,RV-LTLというものを導入する.RV-LTLの意味は,4つの値 $\{\top , \bot, \top^p, \bot^p\}=\mathcal{B}_4$ (順序関係は,自明ではないが直感的なのでここでは省略)を持つ束をレンジに持つような関数 $[\_\models\_]_{RV} : RVLTL \rightarrow \mathcal{B}_4$ によって与えられる. $\top,\bot$ の直感的な意味は良いとして, $\top^p, \bot^p$ の直感的な意味は,導入の時に説明したように,有限のトレース上では判断がつかないが,無限に続いたら,おそらく満たす(満たさない)だろうというような意味になる.先に説明した公理の内,LTL3は否定による補完の公理以外を満たし,FLTLは否定による補完の公理を満たしていた.この2つの特徴を併せ持つようにRV-LTLの意味を与える関数 $[\_\models\_]_{RV}$ を次のように与える.

$[u\models\phi]_{RV}=\begin{cases}\top \ \ if[u\models\phi]_3 = \top \\ \bot \ \ if[u\models\phi]_3 = \bot \\ \top^p \ \ if [u\models\phi]_3 = ?\ and\ [u\models\phi]_F = \top \\ \bot^p \ \ if [u\models\phi]_3 = ? \ and\ [u\models\phi]_F = \bot \end{cases}$

ここで $[\_\models\_]_3$ はLTL3での解釈, $[\_\models\_]_F$ はFLTLでの解釈を表す.

本記事では詳細は書かないが,この論理のもとで,導入でもあげた request/acknowledgeの例を考えてみると、このRV-LTLが直感的な意味と一致していることがわかる.(原文では丁寧に書いてある)

6節モニタの構成

RV-LTLの論理式から対応するムーア機械を構成する方法を与えています.

そんなに長くないので詳細は原文を(ry

7節結論

省略.

原文を(ry

Jack of All Trades, Master of None

器用貧乏系情報科学徒のメモ

nested word

Nested word

定義

マッチング関係

参考

正規言語のVariety Theoryと動的命題論理