時相論理 (Temporal Logic) は時間に関する作用素を追加した論理の体系です。 例えば、時相論理では「ボタンを押したら、3秒以内に明かりが点く」のような時間による状況の変化を含めた文を表現することができます。

時間に関する論理的な文は、プログラムやシステムの満たすべき性質を考える際に頻繁に現れます。 そのため、時相論理は形式検証 (Formal Verification) の分野で重要な道具の一つとなっています。

モニタリングとは、入力として与えられた時系列に沿ったイベント列が、時相論理などの形で与えられた仕様を満たすかどうか判定する問題です。 線形時相論理 (LTL) やMetric Temporal Logic (MTL)、Signal Temporal Logic (STL) といった時相論理では、このモニタリングを効率的に行う方法が知られています。 モニタリングは、システムが仕様通りのふるまいをしているかを実行時に確認する、実行時検証の実現方法の1つでもあります。

この記事では、時相論理のモニタリング実装や、その背景にあるアイディアについて整理します。

時相論理 (Temporal Logic)

時相論理 (Temporal Logic) は時間に関する作用素を追加した論理の体系の1つです。 通常の $\varphi \land \psi$ や $\varphi \lor \psi$ などの論理作用素に加えて、$N \varphi$ (次の時点で$\varphi$が真) や$\varphi U \psi$ ($\psi$が真になるまで$\varphi$は真) のような時間に関する作用素を利用できる論理体系が、時相論理になります。

形式検証 (Formal Verification) の分野で、時相論理は重要です。 というのもプログラムやシステムの満たすべき性質には、時間に関する制約が様々な形で現れるためです。 そのような性質として有名なものに、「悪いこと $\varphi$ が今後決して起こらない」という安全性 (Safety) と呼ばれるものがあります。

時相論理には様々な種類があります。 その中でも、形式検証でよく用いられるLTL, MTL, STLの3種類について簡単に説明します。

LTL (Linear Temporal Logic)

線形時相論理 (LTL, Linear Temporal Logic) は時相論理の基本的なバリエーションの1つです。 列として与えられた時系列に沿ったイベント (事実の集合) の上で意味論をもつ時相論理です。¹

線形時相論理には、次のような時間に関する作用素があります。

• $N \varphi$ (Next): 次の時点で $\varphi$ は真
• $G \varphi$ (Globally): どの時点でも $\varphi$ が真
• $\varphi U \psi$ (Until): $\psi$ が真になるまで $\varphi$ は真

他にも $F \varphi$ (Finally、いずれかの時点で $\varphi$ は真) がありますが、これは $F \varphi = \mathbf{true} U \varphi$です。 また、$G \varphi = \lnot F \lnot \varphi$ です。 様相論理との関係から、$G \varphi$ を $\Box \varphi$ と記述したり、$F \varphi$ を $\diamond \varphi$ と記述することもあります。²

LTLで安全性「悪いこと $\varphi$ が今後決して起こらない」は $G \lnot \varphi$ として表されます。

Future-timeとPast-time

先ほど紹介した時間に関する作用素はすべて、未来の事実についての文をつくるものです。 このように未来に対する作用素のみを持つLTLをとくにFuture-time LTLと呼ぶ場合があります。

さらに、次のような過去に対する作用素も考えられます。

• $P \varphi$ (Previous): 前の時点で $\varphi$ は真 ³
• $H \varphi$ (Historically): 以前のどの時点でも $\varphi$ は真
• $\varphi S \psi$ (Since): $\psi$が真になってから$\varphi$は真

Future-timeの場合と同様に、$O \varphi$ (Once, 以前のいずれかの時点で $\varphi$ は真) も考えられます。 これらの作用素をもつLTLはPast-time LTLと呼ばれます。

Past-timeであれば時系列の途中までの時点で、論理式が成り立っているかの判定が可能なため、モニタリングにおいてはPast-time LTLが利用されることの方が多いです。 この事実がモニタリングの原理になっているとも考えられます。

MTL (Metric Temporal Logic)

MTL (Metric Temporal Logic) は、時間に関する作用素に有効となる期間 (Interval) の概念を追加したものです。 期間は2つの時間$a, b$に対する閉区間$[a, b]$や非有界な区間$[a,+∞)$として表されます。 具体的には、次の時間に関する作用素が導入されます。

• $\varphi U_I \psi$: 期間 $I$ 以内で $\psi$ が真になるまで $\varphi$ は真
• $\varphi S_I \psi$: 期間 $I$ 以内で $\psi$ が真になってから $\varphi$ は真

これらの作用素を使うことで「何秒以内に○○が起こる」といったよくある条件を簡潔に記述できるようになります。

モニタリングという観点で考えても、記録しておく必要のある期間が論理式から明確になるため、効率的なモニタリングが実現できるようになります。 そのため、モニタリングの分野ではMTLやそれに近い時相論理が用いられることが多いように思います。

離散的な時間と連続的な時間

MTLでは時間の表現として離散的 (Discrete) なものと、連続的 (Continuous) なものの2種類が考えられます。

離散的な時間とは、個々のイベントが時系列上に列として与えられるような状況で、イベントは自然数のタイムスタンプで添字付けられています。 一方、連続的な時間では、個々のイベントは実数の時間に対して与えられています。つまり$A$を事実 (Atom) の集合として、イベント列が$\mathbb{R}_{\ge 0} \to 2^A$のようにして与えられる状況になります。

連続的な時間の方がより現実的な仮定のため、実世界のシステムの検証の際はそちらの方が有用だと考えられます。 しかし、実行時モニタリングの場合は、一定の周期で事実を観測したり、あるいは何かイベントが離散的に送られてくるようにして実装されるはずなので、離散的な時間で考えてもそれほど問題にはならないのではないかと考えています。

STL (Signal Temporal Logic)

STL (Signal Temporal Logic) はイベントとして事実の集合ではなく、実数値のマッピングを取るような時相論理の拡張です。 この場合、論理式のAtomは$x \ge c$のようなシグナル変数と定数の比較の形を取ります。

STLの特徴は、時間として連続的な時間を考えて、その場合にシグナルの実数値が連続に変化することを考えることです。 とくに、シグナル値が線形に変化する場合は、線形計画法の知識が応用できるようになります。

時系列に沿って変化する値というのは実世界のシステムでよく現れます (例、車の加速度)。 そこで、STLによってより厳密にシステムの仕様を記述できます。

ロバスト値

$x \ge c$は$x - c \ge 0$なので、$x - c$が大きければ大きいほどシグナルの値が多少変わっても論理式は真であり続けます。 このアイディアをベースにしたのがロバスト値と呼ばれるものです。

具体的には、ブール束を実数の束に置き換えて計算することで、通常の意味論と同様にして考えることができます。 モニタリングにおいても、真偽を判定するのではなく、このロバスト値を求められるものも存在しています。

モニタリング

ある時相論理の式 $\varphi$ と時系列に並んだイベント (シグナル) の列が与えられて、ある時点で $\varphi$ を満たすかどうかを判定する問題をモニタリングと呼びます。 さらに、このモニタリングを実際のシステムのログに対して適用し、システムが満たすべき性質を守っているかを検証する手法を、実行時検証 (Runtime Verification) と呼びます。

モニタリングにはさらに、次のような軸での分類があります。

• オフラインか、オンラインか。
  オフラインモニタリングでは、入力のイベント列が予めすべて与えられていて、それに対して各時点についてモニタリングを行います。一方、オンラインモニタリングでは、入力は逐次的に与えられて、与えられた各時点でのモニタリングを行います。
• 質的 (qualititative) か、量的 (quantitative) か。
  質的なモニタリングとは、式を満たすかどうかを真偽値で返すモニタリングです。そして、量的なモニタリングでは、式に対して各時点でのロバスト値を返します。

実装

ここでは調査したモニタリングの実装を紹介します。

まず始めに、各実装の特徴をまとめた表を示します。

ここで言うFirst-orderとはデータに対して変数を$\forall$や$\exists$で量化できることを意味します。

MonPoly

リポジトリ: https://bitbucket.org/monpoly/monpoly/

MonPolyはチューリッヒ工科大学で研究・開発されたモニタリング実装です。 実装言語はOCamlです。

MFOTL (Metric First-Order Temporal Logic) という、MTLをFirst-orderに拡張した時相論理によって、モニタリングの式を記述できます。 さらに、SQLのSUMやCOUNTのような、集計 (Aggregation) のための演算子が追加されているのも大きな特徴です。

下の例は[Basin, et al., 2017]から引用したもので、30単位時間以内に各ユーザーについての引き落としの合計金額が10000を越えた場合を、詐欺の疑いがあるとして、検出する論理式になっています。

(s <- SUM a;u ONCE[0,30] withdraw(u,a) AND tp(i))
AND
NOT s <= 10000

一方で、このような集計を実現するために、論理式の中の自由変数に束縛される値が必ず求められなければいけないという制約があります。 この制約はMonitorableとして形式的に定義されています (c.f. [Basin, et al, 2013]) が、実用の際には意外とこの制約を突破できずもどかしい気分になります。

アルゴリズムは何となくオンラインでも動作しそうなものですが、試した限りではオフラインでしか動作しないです。 まあFuture-timeの作用素をサポートしているので仕方ないのかもしれません。

参考文献:

• [Basin, et al., 2013]:

  Basin, David, et al. "Monitoring of temporal first-order properties with aggregations." Runtime Verification: 4th International Conference, RV 2013, Rennes, France, September 24-27, 2013. Proceedings 4. Springer Berlin Heidelberg, 2013.

• [Basin, et al., 2017]:

  Basin, David A., Felix Klaedtke, and Eugen Zalinescu. "The MonPoly Monitoring Tool." RV-CuBES 3 (2017): 19-28.

DejaVu

リポジトリ: https://github.com/havelund/dejavu

DejaVuはNASA/カリフォルニア工科大学のKlaus Havelundらが研究・開発したモニタリング実装です。 実装言語はScalaで、モニターを実装したScalaのソースコードを生成します。

DejaVuの特徴はBDDを用いてFirst-orderな量化を実現しているところです (c.f. [Havelund, et al., 2020])。 MonPolyでは変数の取り得るが値が有限になることを保証することでモニタリングを解けるようにしていましたが、こちらはBDDを使って変数の取る値を上手く記録することで、記述できる論理式は原則モニタリングが行えるようにしています。

また、ツールとしての特徴として、1つの仕様に複数の満たすべき性質 (論理式) を書いて、一度にモニタリングする実装を出力できます。 他にも再帰的な性質が定義できるようになっていたり、少し面白いです⁴。

発表後はあまりメンテナンスされていないと思っていたのですが、昨日 (2024/3/8) 突然更新されました。

参考文献:

• [Havelund, et al., 2020]:

  Havelund, Klaus, Doron Peled, and Dogan Ulus. "First-order temporal logic monitoring with BDDs." Formal Methods in System Design 56.1 (2020): 1-21.

Reelay

リポジトリ: https://github.com/doganulus/reelay

Reelayはボアズィチ大学のDoğan Ulusが研究・開発したモニタリング実装です。 実装言語はC++で、ヘッダーオンリーのライブラリやPythonのライブラリとして使えるようになっています。 ちなみに、Ulus氏は前のDejaVuの論文の共著者の一人でもあります。

入力のイベント列は、行単位のJSON (JSON Lines) です。 そのため、AtomがJSONのプロパティに対するものになります。 次の例は、lights_onがtrue、speedが20.0より大きくて、modeが"Sport XL"のときに真になるAtomです。

{lights_on: true, speed > 20.0, mode: "Sport XL"}

また、今回紹介する実装の中では唯一量的なモニタリングが可能です。 しかし、forallやexistsといった量化子とは併用できません。 これは、量化子の実装はDejaVuのBDDを用いたものと同様の実装になっているためのようです。

他にも、STLをサポートしています。 つまり、実数値の入力に対して線形補間を行うことが可能なようです。

実装が比較的シンプルで読みやすかったです。 また、入力がJSON Linesだったり、Pythonのライブラリとして提供されていたり、コンパクトに実用的なツールを作ろうとしているところに好感が持てます。

参考文献:

• [Dogan, 2019]:

  Ulus, Dogan. "Online monitoring of metric temporal logic using sequential networks." arXiv preprint arXiv:1901.00175 (2019).

他の実行時検証の方法

時相論理を使ったモニタリングの他にも、実行時検証を実現方法として、ストリーム処理に基づく方法があります。 これは論理式などで性質を書くのではなく、ストリームに対する処理としてやや手続き的に (とはいってもかなり宣言的ですが) 記述する方法になります。

この方法として代表的なものに次のものがあります。

• Lola (RTLola)
• Copilot

Lolaはストリーム記述言語の1つで、RTLolaはそのリアルタイムな拡張です。 比較的歴史があり、ストリーム処理に基づく実行時検証のベースとなっているような印象です。

CopilotはNASAで研究・開発されているストリーム記述言語で、Haskellの内部DSLとして実装されています。 Haskellの型システムに基づいているため、厳格な型チェックができます。 また、メモリ消費が定数なC言語のコードが生成されたり、Haskellのライブラリとして論理的な記述もサポートされています。 モデルの記述も可能なため、モデル検証へとつなげる拡張もあるようです。

Copilotがかなり先進的で面白い気がしています。

まとめ

この記事では時相論理を用いたモニタリングについて調査をまとめました。

実装としてはMonPolyやDejaVu、Reelayなどがありますが、個人的にはReelayを使うのが良さそうだと思っています。 また、時相論理を直接扱うわけではありませんが、Copilotも興味深い実装です。

MTLの実装も試してみているので、いずれそれについても説明できればと思います。

最後まで目を通していただきありがとうございました。