論文の概要: Proving Non-Inclusion of B\"uchi Automata based on Monte Carlo Sampling
- arxiv url: http://arxiv.org/abs/2007.02282v2
- Date: Tue, 7 Jul 2020 01:26:19 GMT
- ステータス: 処理完了
- システム内更新日: 2022-11-13 08:32:08.686898
- Title: Proving Non-Inclusion of B\"uchi Automata based on Monte Carlo Sampling
- Title（参考訳）: モンテカルロサンプリングに基づくB\"uchi Automataの非包摂性証明
- Authors: Yong Li, Andrea Turrini, Xuechao Sun, Lijun Zhang
- Abstract要約: B"uchiautoa non-inclusion $mathcalL(mathcalA) notsubseteq mathcalL(mathcalB)$を証明するための具体的なアルゴリズムを提案する。
$mathsfIMC2$は、B"uchiautoaのインクルージョンに対する反例を見つける高速で信頼性の高い方法である。
- 参考スコア（独自算出の注目度）: 19.09848789158933
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: The search for a proof of correctness and the search for counterexamples
(bugs) are complementary aspects of verification. In order to maximize the
practical use of verification tools it is better to pursue them at the same
time. While this is well-understood in the termination analysis of programs,
this is not the case for the language inclusion analysis of B\"uchi automata,
where research mainly focused on improving algorithms for proving language
inclusion, with the search for counterexamples left to the expensive
complementation operation.
In this paper, we present $\mathsf{IMC}^2$, a specific algorithm for proving
B\"uchi automata non-inclusion $\mathcal{L}(\mathcal{A}) \not\subseteq
\mathcal{L}(\mathcal{B})$, based on Grosu and Smolka's algorithm
$\mathsf{MC}^2$ developed for Monte Carlo model checking against LTL formulas.
The algorithm we propose takes $M = \lceil \ln \delta / \ln (1-\epsilon)
\rceil$ random lasso-shaped samples from $\mathcal{A}$ to decide whether to
reject the hypothesis $\mathcal{L}(\mathcal{A}) \not\subseteq
\mathcal{L}(\mathcal{B})$, for given error probability $\epsilon$ and
confidence level $1 - \delta$. With such a number of samples, $\mathsf{IMC}^2$
ensures that the probability of witnessing $\mathcal{L}(\mathcal{A})
\not\subseteq \mathcal{L}(\mathcal{B})$ via further sampling is less than
$\delta$, under the assumption that the probability of finding a lasso
counterexample is larger than $\epsilon$. Extensive experimental evaluation
shows that $\mathsf{IMC}^2$ is a fast and reliable way to find counterexamples
to B\"uchi automata inclusion.
- Abstract（参考訳）: 正しさの証明の探索と反例の探索(バグ)は検証の相補的な側面である。
検証ツールの実用性を最大化するためには、それらを同時に追求する方がよい。
これはプログラムの終了解析でよく理解されているが、b\"uchi automataの言語包含分析では、主に言語包含性を証明するアルゴリズムの改善に焦点が当てられている。
本稿では,Grosu と Smolka のアルゴリズムである $\mathsf{IMC}^2$ を,モンテカルロモデルで LTL 式に対するチェックを行うために開発された,B\"uchiautoa non-inclusion $\mathcal{L}(\mathcal{A}) \not\subseteq \mathcal{L}(\mathcal{B})$ を証明するための特定のアルゴリズムである $\mathsf{IMC}^2$ を提案する。
我々が提案するアルゴリズムは、$m = \lceil \ln \delta / \ln (1-\epsilon) \rceil$ ランダムラッソ型標本を$\mathcal{a}$ から取り出して、与えられたエラー確率 $\epsilon$ と信頼レベル $1 - \delta$ に対して$\mathcal{l}(\mathcal{a}) \not\subseteq \mathcal{l}(\mathcal{b})$ を拒絶するかどうかを決定する。
そのようなサンプルでは、$\mathsf{IMC}^2$は、ラッソ反例を見つける確率が$\epsilon$より大きいという仮定の下で、$\mathcal{L}(\mathcal{A}) \not\subseteq \mathcal{L}(\mathcal{B})$が$\delta$より小さいことを保証している。
広範な実験により、$\mathsf{imc}^2$ は b\"uchi automata への反例を見つけるための高速で信頼性の高い方法であることが示されている。
関連論文リスト
- Sample and Computationally Efficient Robust Learning of Gaussian Single-Index Models [37.42736399673992]
シングルインデックスモデル (SIM) は $sigma(mathbfwast cdot mathbfx)$ という形式の関数であり、$sigma: mathbbR to mathbbR$ は既知のリンク関数であり、$mathbfwast$ は隠れ単位ベクトルである。
適切な学習者が$L2$-error of $O(mathrmOPT)+epsilon$。
論文 参考訳（メタデータ） (2024-11-08T17:10:38Z) - Simple and Nearly-Optimal Sampling for Rank-1 Tensor Completion via Gauss-Jordan [49.1574468325115]
ランク1テンソルを$otimes_i=1N mathbbRd$で完了する際のサンプルと計算複雑性を再考する。
本稿では,一対のランダム線形系上で,ガウス・ヨルダンに相当するアルゴリズムを許容する問題のキャラクタリゼーションを提案する。
論文 参考訳（メタデータ） (2024-08-10T04:26:19Z) - Statistical Query Lower Bounds for Learning Truncated Gaussians [43.452452030671694]
この問題のSQアルゴリズムの複雑さは、$dmathrmpoly (1/epsilon)$であり、クラス$mathcalC$が単純である場合でも、$mathrmpoly(d/epsilon)が情報理論的に十分であることを示す。
論文 参考訳（メタデータ） (2024-03-04T18:30:33Z) - Provably learning a multi-head attention layer [55.2904547651831]
マルチヘッドアテンション層は、従来のフィードフォワードモデルとは分離したトランスフォーマーアーキテクチャの重要な構成要素の1つである。
本研究では,ランダムな例から多面的注意層を実証的に学習する研究を開始する。
最悪の場合、$m$に対する指数的依存は避けられないことを示す。
論文 参考訳（メタデータ） (2024-02-06T15:39:09Z) - Quantum Oblivious LWE Sampling and Insecurity of Standard Model Lattice-Based SNARKs [4.130591018565202]
Learning Errors With Errors(mathsfLWE$)問題は$(mathbfAmathbfs+mathbfe$)という形式の入力から$mathbfs$を見つけるように要求する
私たちは$mathsfLWE$の解決ではなく、インスタンスをサンプリングするタスクに注力しています。
我々の主な成果は、よく分散された$mathsfLWE$インスタンスをサンプリングする量子時間アルゴリズムである。
論文 参考訳（メタデータ） (2024-01-08T10:55:41Z) - Optimal Estimator for Linear Regression with Shuffled Labels [17.99906229036223]
本稿では,シャッフルラベルを用いた線形回帰の課題について考察する。
mathbb Rntimes m の $mathbf Y、mathbb Rntimes p の mathbf Pi、mathbb Rptimes m$ の mathbf B、mathbb Rntimes m$ の $mathbf Win mathbb Rntimes m$ である。
論文 参考訳（メタデータ） (2023-10-02T16:44:47Z) - Near-Optimal Bounds for Learning Gaussian Halfspaces with Random
Classification Noise [50.64137465792738]
この問題に対する効率的なSQアルゴリズムは、少なくとも$Omega(d1/2/(maxp, epsilon)2)$. のサンプル複雑性を必要とする。
我々の下限は、この1/epsilon$に対する二次的依存は、効率的なアルゴリズムに固有のものであることを示唆している。
論文 参考訳（メタデータ） (2023-07-13T18:59:28Z) - Fast $(1+\varepsilon)$-Approximation Algorithms for Binary Matrix
Factorization [54.29685789885059]
本稿では, 2次行列分解(BMF)問題に対する効率的な$(1+varepsilon)$-approximationアルゴリズムを提案する。
目標は、低ランク因子の積として$mathbfA$を近似することである。
我々の手法はBMF問題の他の一般的な変種に一般化する。
論文 参考訳（メタデータ） (2023-06-02T18:55:27Z) - Learning a Single Neuron with Adversarial Label Noise via Gradient
Descent [50.659479930171585]
モノトン活性化に対する $mathbfxmapstosigma(mathbfwcdotmathbfx)$ の関数について検討する。
学習者の目標は仮説ベクトル $mathbfw$ that $F(mathbbw)=C, epsilon$ を高い確率で出力することである。
論文 参考訳（メタデータ） (2022-06-17T17:55:43Z) - Threshold Phenomena in Learning Halfspaces with Massart Noise [56.01192577666607]
ガウス境界の下でのマスアートノイズ付きmathbbRd$におけるPAC学習ハーフスペースの問題について検討する。
この結果は,Massartモデルにおける学習ハーフスペースの複雑さを定性的に特徴づけるものである。
論文 参考訳（メタデータ） (2021-08-19T16:16:48Z) - Efficient Statistics for Sparse Graphical Models from Truncated Samples [19.205541380535397]
i) スパースガウス図形モデルの推論と (ii) スパース線形モデルの回復支援の2つの基本的問題と古典的問題に焦点をあてる。
疎線型回帰については、$(bf x,y)$ が生成されるが、$y = bf xtopOmega* + MathcalN(0,1)$ と $(bf x, y)$ は、truncation set $S subseteq mathbbRd$ に属する場合にのみ見られる。
論文 参考訳（メタデータ） (2020-06-17T09:21:00Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。