線形時相論理式（LTL）を分かりやく説明

線形時相論理式（Linear Temporal Logic：LTL）をできるだけ分かりやすく説明していこうと思います。

もともとはシステムが正しく動くかどうかを検証するために研究されていたものなのですが、最近ではロボットの移動経路に用いられたり、機械学習の一つである強化学習の報酬設計などにも応用されています。

ただ、この漢字が多いのと「論理式」というだけで、難しそうと感じられてしまうこともしばしば…

ということで、できるだけ分かりやすく、LTLが市民権を得られるように説明していきます。

論理式とは何か？と考えると一番最初に思い浮かべるのは、

AかつBならばC

ではないでしょうか。このフレーズを聞いたことがある方はきっと多いと思います。

そうです。これが論理式です。

ポイントは

です。

1つ目は論理式のメリットになります。書き方が決まっているので、誰でも書き方のルールを覚えれば論理式が書け、同じことを違う論理式で表現したときは、変形することで同じ論理式になります。

ドモルガンの法則がそのよい例です。

2つ目は普通の論理式のデメリットになります。このことを交差点の2つの信号の具体例で考えていきます。

これらの信号に守ってほしいこととして

「いつも一つの信号が青ならば、もう一つの信号は青でない」

があるとします。

しかし、普通の論理式では未来の話やシステムが動作している様子については表現できません。今、「両方の信号が青でない」ことは表現できるのですが、「信号が稼働している間はずっと」となるとダメなんです…

そういったことを解決するために考えられたのが時相論理で、その中でも最も基本で重要なものとして、線形時相論理（LTL）があります。

漢字が多いので、分割します。

つまり、一直線で順番につながっているものに対して、「いつも～」「いつか～」「次に～」を含めて真か偽かを判定できる論理式です

なんやそれ？という感じなのでLTL式で表現できる具体例を考えていきます。

1つ目について、

は真（正しい信号の動作）と判定できるですが、

は偽（危険な信号の動作）と判定されます。

2つ目について、

というようにずーっと赤の信号はダメなので、偽と判定されます。

3つ目について、

こんなのは言わずもがなダメですよね…

このようにシステムのふるまい・動作について、真か偽かを判定することができる論理式がLTL式です

「こんなのLTL式なんか使わなくても表せるのでは？」と思った方はきっといらっしゃると思います。

ここで論理式の説明で挙げたポイント1つ目が活きてきます。書き方さえ守っていれば、長いLTL式＝複雑な命令も表現できます。そして、LTL式は長くても短くても処理の方法そのものは同じで、形式的に決まりきった形で行われます。

ここからは真面目なLTLを紹介します。興味のない方は読み飛ばしてください。

LTLで与えた命令が真か偽かを判定する対象を定義します。

さきほどの信号の動作（色の変化）を実行列と呼び、 $\pi$ で表記します。この実行列 $\pi$ は無限の長さで考えるのですが、最初から数えて $k$ 番目の途中からの実行列を $\pi(k...)$ とします。

具定例としては、このようなイメージです。

LTLはSyntaxとSemanticsで定義されます。

Syntaxはポイントの一つ目で述べた書き方です。SemanticsはSyntaxで出てきた記号がどのような意味なのか、を表します。

Semantics：実行列 $\pi$ の $k$ 番目でLTL式 $\phi$ を満たすことを $\pi(k...) \models\phi$ で表す。

$\pi(k...) \models True$ ,
$\pi(k...) \models ap$ if and only if $ap \in L(\pi(k))$ ,
$\pi(k...) \models \lnot \phi$ if and only if $\pi(k...) \not\models \phi$ ,
$\pi(k...) \models \phi _ 1\land \phi _ 2$ if and only if $\pi(k...) \models \phi _ 1 \land \pi(k...)\models \phi _ 2$ ,
$\pi(k...) \models \bigcirc \phi$ if and only if $\pi(k+1...) \models \phi$ ,
$\pi(k...) \models \phi _ 1 U \phi _ 2$ if and only if there exists $j$ such that $\pi(j...) \models \phi _ 2$ and $\pi(i...) \models \phi _ 1, \forall i \in [k,j-1$ ].