技術的概要：ネスト型定量オートマトンによる QuAK の拡張

問題定義

定量オートマトン（QA）は、有限状態の$\omega$-オートマトンに重み付き遷移を追加し、平均負荷やピークメモリ使用量などの定量的なシステム特性を指定可能にする。しかし、標準的な QA は有限の重み集合に制限されており、平均応答時間のような無制限の値を必要とする特性を表現できない。このようなシナリオでは、リクエストとグラントの間の遅延は任意に大きくなり得るが、有限の遷移重みではこの制約を捉えられない。

**ネスト型定量オートマトン（NQA）**は、親オートマトンが子オートマトンを生成させ、有限の中間部分列（infix）上で無制限の値を計算させることでこの問題を理論的に解決するために導入されたが、歴史的には実用的なツールサポートが欠如していた。NQA に対する既存の決定手続きは理論的なままにとどまり、決定可能性の結果と自動検証との間にギャップが存在していた。

手法

著者らは、QA 分析用のソフトウェアツールであるQuAK（Quantitative Automata Kit）を NQA をサポートするように拡張することで、このギャップを埋める。中核的な手法は、NQA インスタンスを標準的な QA インスタンスに還元する平坦化手続きに依存している。この還元は、入力 NQA と出力 QA の間の意味的同等性を必ずしも保持しないものの、閾値決定問題（空性および普遍性）に対する回答は保持する。

C++ で実装された平坦化パイプラインは、親集約関数（$f$）と子集約関数（$g$）の組み合わせに基づき、以下のアルゴリズム戦略を処理する。

1. 正規の子（$g \in \{Min, Max, SumB\}$）: 可能な戻り値の集合が有限であるため、ツールは子の戻り値を推測し、義務ベースのアプローチで検証する。これには、可能な子の構成を並行して追跡し、推測された値で最終状態に到達できないものを剪定するプロセスが含まれる。
2. 閾値に基づく境界設定（$f \in \{Sup, LimSup, Inf, LimInf\}, g \in \{Sum+, Sum-\}$）: これらの場合、特定の閾値$\lambda$を超える子の戻り値は切り捨てられる。これにより問題は有界な$SumB$ケースに還元され、正規の子の構築が可能になる。
3. 極値親と単調子: 極値親（$Sup, LimSup, Inf, LimInf$）と単調子を用いた空性チェックにおいて、ツールは正確な戻り値の計算を回避する。代わりに、各子の呼び出しを二値の閾値結果（子が値$\ge \lambda$を返せるか？）に還元する。これにより、必要な閾値ステータスのみを追跡する専用の「推測と検証」手続きが可能となり、一般的な還元と比較して状態空間を大幅に削減できる。
4. 無制限の子を持つリミット平均:
   • $(LimSupAvg, Sum+)$の場合、ツールはまず子の戻り値が無制限に成長し得るかどうかをチェックする。もしそうであれば、空性は自明に成立する。そうでない場合は、有界な$SumB$ケースに還元される。
   • $(LimInfAvg, Sum-)$および$(LimSupAvg, Sum-)$の場合、ツールは同期構築を採用し、すべてのアクティブな子が同時に進行するよう制御する。これにより、アクティブな子の状態の有界な多重集合を追跡する。
5. サイレント重みの除去: 平坦化プロセスは、子を呼び出さない遷移（サイレント重み）を持つ QA を生成する。これらは、中立重み（例：$Sup$の場合は$-\infty$）への置換、またはリミット平均目的のためのパス圧縮構築によって除去される。
6. 反鎖に基づく普遍性: 普遍性を決定するために、ツールは反例となる単語のオンザフライ探索を行い、探索空間を剪定するために反鎖（antichains）を使用する。文脈には、到達可能性 alongside 定量的境界を処理するための値サマリーが追加される。

主要な貢献

1. ツールの実装: NQA 分析アルゴリズムの最初の実際的な実装であり、QuAK フレームワークを拡張したものである。
2. 包括的な平坦化スイート: 空性と普遍性が決定可能であることが知られている、親と子の集約関数のすべての組み合わせに対する平坦化手続きの実装。これには、親関数$\{Sup, Inf, LimSup, LimInf, LimSupAvg, LimInfAvg\}$および子関数$\{Min, Max, SumB, Sum+, Sum-\}$が含まれる。
3. モジュール型アーキテクチャ: NQA をサイレント重み付き QA に変換するパイプラインであり、その後、QuAK の既存の決定手続き（空性、包含、安全性 - 活性分析）によって処理される。
4. 実験的評価: ツールは 2 つのベンチマークファミリーで評価された。
   • 応答時間: 制限された待機リクエスト数（$n$）と応答時間（$k$）を持つリクエスト - グラントプロトコルをモデル化するパラメトリック NQA（$A_{n,k}$）。
   • リソース消費: 動的に開始・終了するプロセスとリソースアクセスパターンをモデル化するパラメトリック NQA（$B_{n,k}$）。

結果

実験的評価は、異なる NQA タイプ全体にわたる QuAK の有効性とスケーラビリティを実証している。

• 応答時間ベンチマーク:
  • $(Sup, Sum+)$の空性チェックにおいて、ツールは良好にスケーリングし、実行時間は応答時間境界$k$に対してほぼ二次的な依存関係を示し、待機リクエスト数$n$に対しては軽微な依存関係を示す。
  • $(LimSupAvg, Sum+)$の空性チェックおよび$(Sup, SumB)$の普遍性チェックでは、両方のパラメータに対して実行時間がより急速に増加する。普遍性は、平坦化されたオートマトンにおける非決定性を処理するために PSpace 手続きが必要となるため、一貫して高コストである。
• リソース消費ベンチマーク:
  • $(Sup, Max)$の空性チェックは、アクティブな子によって追跡されるリソース部分集合の組み合わせ爆発により、両方のパラメータ（$n$と$k$）において急速な増大を示す。
  • $(LimSupAvg, Max)$のケースは著しく困難であり、すべてのアクティブな子に対して正確な戻り値を保持する必要があるため、上限（supremum）ケースと比較してより小さなパラメータ値でメモリ枯渇を引き起こす。

これらの結果は、明示的な平坦化が多くの子インスタンスが同時にアクティブな場合や子の構成が密な場合に大規模な状態空間を招く可能性がある一方で、ツールは複雑な定量的特性の決定可能なインスタンスを成功裡に処理することを確認している。

意義

本論文は、NQA の理論的決定可能性と実用的な検証の間のギャップを埋めると主張している。QuAK を拡張することで、著者らは標準的な QA では表現できないが NQA では表現可能な、平均応答時間などの定量的特性の自動検証を可能にした。この研究は、動的に生成されるタスクと無制限のコストを持つシステムの分析基盤を確立し、プロトコル遅延分析、サービスレベルの応答時間監視、およびリソース消費分析のための実用的な枠組みを提供する。著者らは、現在の実装が明示的な状態構築に依存しているが、将来の研究では状態空間の爆発を緩和するために記号的表現を探求する可能性があることに言及している。