確率的な無限状態システムで到達可能性の確率を近似
Quantitative coverability for probabilistic well-structured transition systems
この論文をやさしく読む
ひとことで言うと
状態が無限にある確率的システムで、ある状態群に到達する確率を近似計算できる条件を示した理論研究。
何に役立つ？
確率的な個体群モデルや通信路モデルの形式検証に役立つと考えられる。実機や実データでの性能評価ではなく、計算可能性についての数学的結果である。
この研究の面白いところ
分岐数が有限とは限らない場合を扱い、確率的単調性から決定性を導く。多型Galton–Watson過程では母関数や従来の領域別の場合分けを使わずに結論を得る。
どこまで分かった？
有限時間の結果は効果的な部分クラスが対象で、無限時間には決定性が必要。Galton–Watson過程への適用には繁殖則への仮定がある。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
整列構造を持つ遷移系（WSTS）は無限状態システムの検証に使われる古典的な枠組みである。しかし、その確率的な拡張については、定量的な被覆可能性を統一的に扱う方法がない。経路を列挙するアルゴリズムは分岐数が有限であることを仮定し、別の近似手法では、有限時間内の確率など一部の計算を個別のモデルに任せている。本研究では、可算の状態集合上のマルコフ連鎖で、基礎となる遷移系がWSTSである確率的WSTS（pWSTS）を導入する。分岐数について事前の制約を設けない。このクラスには、確率的ベクトル加算系（pVAS）や確率的損失通信路系（pLCS）など、マルコフ核を備えた任意のWSTSが含まれる。効果的に計算できる部分クラスについて、有限時間の近似的な定量的被覆可能性問題を解き、決定性が成り立つ場合には無限時間についても解く。その際、個々の遷移確率以外の確率情報は必要としない。次に決定性が得られる一般的な理由として、確率的単調性を持つすべてのpWSTSは、任意の上方閉集合に関して決定的であることを示す。最後に、子の数の分布が無限の台を持ち得る古典的な個体群動態モデル、多型Galton–Watson過程にこの枠組みを適用する。繁殖則に穏やかな仮定を置くと、これらの過程は効果的なpWSTSであり、確率的単調性、したがって決定性を持つ。このため、有限・無限両方の時間範囲で近似的な定量的被覆可能性を計算できる。その証明は、従来の母関数も、過程の振る舞いの区分による場合分けも用いない。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-22（UTC）
- 最新改訂
- 2026-09-22 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-22 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
Well-structured transition systems (WSTS) provide a classical framework for the verification of infinite-state systems, but their probabilistic extensions lack a unified treatment of quantitative coverability: path-enumeration algorithms assume a finite branching degree, while alternative approximation schemes defer some computations, such as probabilities over a bounded horizon, to the model at hand. We introduce probabilistic well-structured transition systems (pWSTS), Markov chains over countable state sets whose underlying transition systems are WSTS, with no a priori assumption on the branching degree. This class encompasses any WSTS equipped with a Markov kernel, such as probabilistic vector addition systems (pVAS) and probabilistic lossy channel systems (pLCS). For an effective subclass, we solve the approximate quantitative coverability problem over bounded horizons, and over infinite horizons under decisiveness, requiring no probabilistic information beyond individual transition probabilities. We then identify a general source of decisiveness: every stochastically monotone pWSTS is decisive with respect to every upward-closed set. We finally instantiate the framework on multi-type Galton--Watson processes, a classical model of population dynamics whose offspring distributions may have infinite support. Under mild assumptions on the reproduction laws, these processes are effective pWSTS, and they are stochastically monotone, hence decisive. Approximate quantitative coverability is therefore computable for them over both horizons, with a proof that uses none of the traditional tools: neither generating functions nor any case distinction between regimes.
著者のコメント
25 pages
arXiv ID: 2609.26312 ／ 要約の誤りについて