論文の概要: Bisimulation Learning
- arxiv url: http://arxiv.org/abs/2405.15723v1
- Date: Fri, 24 May 2024 17:11:27 GMT
- ステータス: 処理完了
- システム内更新日: 2024-05-27 13:01:17.408850
- Title: Bisimulation Learning
- Title(参考訳): シミュレーション学習
- Authors: Alessandro Abate, Mirco Giacobbe, Yannik Schnitzer,
- Abstract要約: 我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。
提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
- 参考スコア(独自算出の注目度): 55.859538562698496
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We introduce a data-driven approach to computing finite bisimulations for state transition systems with very large, possibly infinite state space. Our novel technique computes stutter-insensitive bisimulations of deterministic systems, which we characterize as the problem of learning a state classifier together with a ranking function for each class. Our procedure learns a candidate state classifier and candidate ranking functions from a finite dataset of sample states; then, it checks whether these generalise to the entire state space using satisfiability modulo theory solving. Upon the affirmative answer, the procedure concludes that the classifier constitutes a valid stutter-insensitive bisimulation of the system. Upon a negative answer, the solver produces a counterexample state for which the classifier violates the claim, adds it to the dataset, and repeats learning and checking in a counterexample-guided inductive synthesis loop until a valid bisimulation is found. We demonstrate on a range of benchmarks from reactive verification and software model checking that our method yields faster verification results than alternative state-of-the-art tools in practice. Our method produces succinct abstractions that enable an effective verification of linear temporal logic without next operator, and are interpretable for system diagnostics.
- Abstract(参考訳): 我々は、非常に大きく、潜在的に無限な状態空間を持つ状態遷移系に対する有限バイシミュレートを計算するためのデータ駆動型アプローチを導入する。
本手法は,各クラスに対するランキング関数とともに状態分類器を学習する問題として特徴付けられる,決定論的システムのスタッタ非感性ビシミュレーションを計算したものである。
提案手法では,サンプル状態の有限データセットから候補状態分類器と候補ランキング関数を学習し,満足度変調理論を用いて状態空間全体を一般化するかどうかを確認する。
肯定的な答えが得られたとき、その手続きは、分類器がシステムの有効なスタッター非感受性のバイシミュレーションを構成すると結論付ける。
負の応答をすると、クラシファイタがクレームに反する反例状態を生成し、データセットに付加し、正のバイシミュレーションが見つかるまで、反例誘導帰納的合成ループでの学習とチェックを繰り返す。
我々は、リアクティブ検証やソフトウェアモデル検査など、さまざまなベンチマークで、我々の手法が実際に行われている代替最先端ツールよりも高速な検証結果をもたらすことを実証した。
本手法は,次の演算子を使わずに線形時間論理を効果的に検証し,システム診断のために解釈可能な簡潔な抽象化を生成する。
関連論文リスト
- Improving Probabilistic Bisimulation for MDPs Using Machine Learning [0.0]
本稿では,与えられたモデルの状態空間を確率的ビシミュレーションクラスに分割する新しい手法を提案する。
このアプローチは、最先端のツールと比較して、実行時間を著しく削減できる。
論文 参考訳(メタデータ) (2023-07-30T12:58:12Z) - Quick Adaptive Ternary Segmentation: An Efficient Decoding Procedure For
Hidden Markov Models [70.26374282390401]
ノイズの多い観測から元の信号(すなわち隠れ鎖)を復号することは、ほぼすべてのHMMに基づくデータ分析の主要な目標の1つである。
本稿では,多対数計算複雑性において隠れた列を復号化するための分法であるQuick Adaptive Ternary(QATS)を提案する。
論文 参考訳(メタデータ) (2023-05-29T19:37:48Z) - Structured model selection via $\ell_1-\ell_2$ optimization [1.933681537640272]
構造化力学系を同定する学習手法を開発した。
候補関数の集合が有界系を成すとき、その回復は安定で有界であることを示す。
論文 参考訳(メタデータ) (2023-05-27T12:51:26Z) - Unified Functional Hashing in Automatic Machine Learning [58.77232199682271]
高速に統一された関数型ハッシュを用いることで,大きな効率向上が得られることを示す。
私たちのハッシュは"機能的"であり、表現やコードが異なる場合でも同等の候補を識別します。
ニューラルアーキテクチャ検索やアルゴリズム発見など、複数のAutoMLドメインで劇的な改善がなされている。
論文 参考訳(メタデータ) (2023-02-10T18:50:37Z) - Data-driven Numerical Invariant Synthesis with Automatic Generation of
Attributes [0.0]
数値不変合成と検証のためのデータ駆動アルゴリズムを提案する。
このアルゴリズムは、正および負の状態のサンプルから決定木を学習するためのICE-DTスキーマに基づいている。
論文 参考訳(メタデータ) (2022-05-30T09:18:37Z) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。
命題の文字は任意の理論で解釈された一階述語式に置き換えられる。
Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文 参考訳(メタデータ) (2022-04-28T17:57:33Z) - An Automated Approach to Causal Inference in Discrete Settings [8.242194776558895]
本稿では,効率的な二重緩和法と空間分岐結合法を用いて因果効果を自動的に結合するアルゴリズムを提案する。
このアルゴリズムは、許容可能なデータ生成プロセスを探索し、利用可能な情報と最も正確な範囲を出力する。
これは、不完全境界を特徴付ける$epsilon$-sharpnessと呼ばれる追加の保証を提供する。
論文 参考訳(メタデータ) (2021-09-28T03:55:32Z) - Sparse PCA via $l_{2,p}$-Norm Regularization for Unsupervised Feature
Selection [138.97647716793333]
再構成誤差を$l_2,p$ノルム正規化と組み合わせることで,単純かつ効率的な特徴選択手法を提案する。
提案する非教師付きモデルを解くための効率的な最適化アルゴリズムを提案し,アルゴリズムの収束と計算の複雑さを理論的に解析する。
論文 参考訳(メタデータ) (2020-12-29T04:08:38Z) - Learning from Incomplete Features by Simultaneous Training of Neural
Networks and Sparse Coding [24.3769047873156]
本稿では,不完全な特徴を持つデータセット上で分類器を訓練する問題に対処する。
私たちは、各データインスタンスで異なる機能のサブセット(ランダムまたは構造化)が利用できると仮定します。
新しい教師付き学習法が開発され、サンプルあたりの機能のサブセットのみを使用して、一般的な分類器を訓練する。
論文 参考訳(メタデータ) (2020-11-28T02:20:39Z) - Adaptive Sampling for Best Policy Identification in Markov Decision
Processes [79.4957965474334]
本稿では,学習者が生成モデルにアクセスできる場合の,割引マルコフ決定(MDP)における最良の政治的識別の問題について検討する。
最先端アルゴリズムの利点を論じ、解説する。
論文 参考訳(メタデータ) (2020-09-28T15:22:24Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。