Teaching LTL and {\omega}-automata with Spot

技術要約：Spotを用いたLTLおよび$\omega$-オートマトンの教育

問題提起
線形時相論理（LTL）および$\omega$-オートマトンは、形式手法の教育、特にプログラム検証やモデル検査において基礎となるものである。教科書は理論的基礎を提供しているが、深い理解を得るためには、学生がLTL式をオートマトンへと変換するプロセスを実験的に体験することが不可้อมである。学習者は、式の変化が結果として得られるオートマトンにどのように影響するかを観察することで、決定性、状態複雑性、および構文構造と意味論的クラス（Manna & Pnueliの階層など）との関係に関する直感を構築できる。しかし、効果的な教育には、複雑なインストール障壁なしに、即時の可視化、比較、およびインタラクティブな実験を可能にするアクセシブルなツールが必要である。

手法
本論文では、LTLおよび$\omega$-オートマトン操作のために設計された成熟したオープンソースのC++/PythonライブラリおよびツールセットであるSpotを、教育用プラットフォームとして提示する。手法の焦点は、教育のための「ゼロインストール」のエントリポイントを作成するために、Spotの既存の機能を活用することにある。このアプローチでは、主に3つのインターフェースを利用する：

1. Webアプリケーション： 標準的なブラウザからアクセス可能なシングルページアプリケーション（ローカルへのインストール不要）。これは、式の変換、特性の研究、および論理の比較を行うためのインタラクティブなインターフェースとして機能する。
2. Jupyter Notebooks： Pythonコード、インラインのオートマトン可視化（Graphviz経由でレンダリング）、および解説テキストを組み合わせた、物語主導型のノートブック集。これにより、包含関係のチェック、反例、および状態のラベル付けの再設定をプログラム的に探索することが可能になる。
3. コマンドラインツール： 特定の基準に基づいてランダムな例を生成し、演習セットを作成するためのユーティリティスイート。

主な貢献
本論文では、Spotの既存の機能がいかに再利用され、教育用に構造化されているかを詳述している：

• インタラクティブな可視化と変換： Webツールを使用すると、ユーザーはLTLまたはPSL式を入力し、様々な受理条件（一般化Büchi、Rabin、Streett、Parityなど）を持つ$\omega$-オートマトンを即座に生成できる。また、複数の入力構文やフォーマット（HOA、never claims、LBTTなど）をサポートしている。
• 比較分析と簡略化：
  • 同値性チェック： 「compare」タブでは、2つの式を入力し、それらが同値でない場合に区別となる$\omega$-語（$\omega$-words）を受け取ることができる。これにより、より単純な同値式を見つけることが容易になる。
  • 階層ナビゲーション： 「study」タブは、Manna & Pneliの時相階層および構文的・未来（syntactic-future）階層における式の正確なクラスを特定する。また、構文的な分類と意味論的な特性の間の不一致を強調する（例：構文的には高いクラスに属しているが、より低いクラスの式と同値である場合を特定するなど）。
  • スタッター不変性（Stutter Invariance）： ツールは、モデル検査における部分順序簡約（partial order reduction）において重要な特性であるスタッター不変性を検出する。式がスタッター不変でない場合、ツールは不全を示す特定の反例語（$w$ および $w'$）を提供する。
• プログラムによる探索： Python APIとJupyter Notebooksにより、非決定性Büchiオートマトンを用いた言語包含チェックや、決定的なオートマトンの状態を、それが認識するLTL式でラベル付けし直すといった高度な概念のデモンストレーションが可能になる。
• 自動演習生成： コマンドラインツール（randltl, ltlfilt）を用いることで、特定の制約を満たすランダムな式をブルートフォースで生成できる（例：$X$演算子を使用せずに $a \mathbin{U} b$ と同値な式を作成する、あるいは$X$演算子を含むスタッター不変な式を見つけるなど）。

結果
本論文は、以下の具体的な教育シナリオを通じて、これらのツールの実用的な適用を実証している：

• 学生は、$(a \mathbin{R} (a \mathbin{U} b)) \mathbin{W} b$ が $a \mathbin{U} b$ と同値であることを、オートマトンの比較または比較タブを使用して検証できる。
• ツールは、$a \mathbin{W} \mathbin{F}(b)$ が構文的には $\Pi_2$ に見えるにもかかわらず、Obligation特性（Manna & Pneli $\Delta_1$）であることを正しく特定し、$G(a) \lor \mathbin{F}(b)$ と同値であることを確認する。
• コマンドラインの例は、特定の基準を満たす式のリストを生成することに成功している（例：$a \mathbin{U} b$ と同値であり、かつ特定の演算子を除外した10個の式を見つける、あるいは$X$演算子を含みながらもスタッター不変である式を見つけるなど）。

意義
本論文は、Spotが時相論理式とその意味論的オートマトンのつながりを教えるための包括的かつアクセシブルなプラットフォームを提供すると主張している。Webベース、Notebookベース、およびコマンドラインベースのインターフェースを提供することで、タブレットを使用する教室から研究コードを書く研究者まで、多様な教育環境に対応している。その意義は、静的な理論を超え、学生が「実験：式を変化させ、その結果として生じるオートマトンの変化を見、直感を構築する」ことを可能にする点にある。これらのツールは、Webユーザーにはインストール不要の準備ができているリソースとして、またPythonをローカルにインストールできない者のために事前構成された環境（spot-sandbox経由）を提供することで、形式手法教育への参入障壁を下げている。