makenowjust-labs/blog

有限状態オートマトンの一種にSymbolic Finite Automata (SFA)と呼ばれるものがあります。 これは遷移が文字ではなく条件式でラベル付けされるオートマトンで、現実世界でSFAを使うことで効率的に表現できる例があることから、研究が進められています。

SFAに対するオートマトン学習アルゴリズムとして、$\Lambda*$と$\mathrm{MAT}*$が知られています。 どちらも既存のオートマトン学習のアルゴリズムをベースとしてSFAに拡張したものですが、学習に用いるデータ構造の特徴を上手く利用した興味深いものになっています。

この記事ではまずSFAの定義を確認し、そのあとに$\Lambda*$と$\mathrm{MAT}*$について解説します。

想定読者: オートマトン学習について知識・関心がある方。

$L^\#$ というオートマトン学習のアルゴリズムがあります。

2022年にVaandragerらによって提案された、最新のオートマトン学習のアルゴリズムです。 apartness relationという概念を用いて、よく知られているAngluinの $L^\ast$ とは少し違ったアイディアでオートマトンの学習を実現します。 学習に用いるデータ構造として、従来のobservation tableやdiscrimination treeではなく、observation treeというmembership query (output query) のキャッシュのようなものを利用するのも特徴です。

この記事では $L^\#$ の詳細や実装について、論文 [Vaandrager et al., 2022] を参考に解説します。

想定読者: オートマトン理論やオートマトン学習について理解・関心がある。

Angluinの $L^\ast$ はオートマトン学習 (automata learning) のアルゴリズムとして最も有名なものです。 以前、このブログでもAngluinの $L^\ast$ について説明しました。

$L^\ast$ は歴史のあるアルゴリズムのため、派生アルゴリズムがいくつか存在します。 この記事ではAngluinの $L^\ast$ について簡単に説明した上で、派生アルゴリズムとしてRivest-SchapireとKearns-Vaziraniを紹介します。

• Rivest-Schapireは $L^\ast$ の反例 (counterexample) の解析手法の提案で、二分探索を用いて反例の中のobservation tableに追加すべき接頭辞を探すことで、計算量を改善します。
• Kearns-Vaziraniはobservation tableを置き換えるデータ構造としてdiscrimination treeというデータ構造を提案するものです。

これらの手法により $L^\ast$ の様々な効率が改善できます。

想定読者: オートマトン理論やオートマトン学習について理解・関心がある。

Immerman-Szelepcsényiの定理は $s(n) \ge \log n$ の場合に $\mathbf{NSPACE}(s(n))$ (テープ長に上限のある非決定性チューリングマシンが受理できる言語のクラス) が、否定について閉じていることを示す定理です。 Neil ImmermanとRóbert Szelepcsényiが1987年にそれぞれ独立して示し、この成果により両者は1995年にGödel賞を受賞しました。 このように、Immerman-Szelepcsényiの定理は、計算量複雑性の理論上とても重要な定理となっています。

Immerman-Szelepcsényiの定理の証明は、テープ長に上限のある非決定性有限チューリングマシン (NTM) の様相 (configuration) の総数が入力の長さとそのNTMの大きさで抑えられることを活かして、次のようなNTMを構成することで実現されます。

• ある様相から到達可能な様相の総数を数え上げた上で、
• その総数のステップ中に、受理状態に到達可能かを判定する。

この記事ではImmerman-Szelepcsényiの定理を[Uezato, 2024]を参考に証明したいと思います。 方針は論文に書いてある通りで特に目新しい部分はありません。自分の備忘録として残しておきます。

想定読者: 情報科学の基本的な部分を理解しており、計算量複雑性の理論などに関心があることを想定しています。

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

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

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

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