論文の概要: Bounded Synthesis of Synchronized Distributed Models from Lightweight Specifications

• arxiv url: http://arxiv.org/abs/2502.13955v1
• Date: Wed, 19 Feb 2025 18:54:32 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-20 14:00:55.009859
• Title: Bounded Synthesis of Synchronized Distributed Models from Lightweight Specifications
• Title（参考訳）: 軽量仕様からの同期分散モデルのバウンド合成
• Authors: Pablo F. Castro, Luciano Putruele, Renzo Degiovanni, Nazareno Aguirre,
• Abstract要約: 本稿では,軽量な形式仕様から同期モデルを自動的に合成する手法を提案する。 我々のアプローチは、グローバルな線形時間制約とともに、分散システムの仕様を入力として受け取ります。 同時実行がグローバルな制約を満たすコンポーネント仕様の実行可能なモデルを生成する。
• 参考スコア（独自算出の注目度）: 4.08734863805696
• License:
• Abstract: We present an approach to automatically synthesize synchronized models from lightweight formal specifications. Our approach takes as input a specification of a distributed system along with a global linear time constraint, which must be fulfilled by the interaction of the system's components. It produces executable models for the component specifications (in the style of Promela language) whose concurrent execution satisfies the global constraint. The component specifications consist of a collection of actions described by means of pre and post conditions together with first-order relational formulas prescribing their behavior. We use the Alloy Analyzer to encode the component specifications and enumerate their potential implementations up to some bound, whose concurrent composition is model checked against the global property. Even though this approach is sound and complete up to the selected bound, it is impractical as the number of candidate implementations grows exponentially. To address this, we propose an algorithm that uses batches of counterexamples to prune the solution space, it has two main phases: exploration, the algorithm collects a batch of counterexamples, and exploitation, where this knowledge is used to speed up the search. The approach is sound, while its completeness depends on the batches used. We present a prototype tool, describe some experiments, and compare it with related approaches.
• Abstract（参考訳）: 本稿では,軽量な形式仕様から同期モデルを自動的に合成する手法を提案する。 我々のアプローチは、システムのコンポーネント間の相互作用によって満たされなければならない、グローバルな線形時間制約とともに、分散システムの仕様を入力するものである。 並列実行はグローバルな制約を満たすコンポーネント仕様(Promela言語スタイル)の実行可能なモデルを生成する。 コンポーネント仕様は、事前条件と後条件によって記述されたアクションの集合と、それらの振る舞いを規定する一階関係式から構成される。 Alloy Analyzerを使ってコンポーネントの仕様をエンコードし、その潜在的な実装をいくつかのバウンダリまで列挙し、そのコンポジションはグローバルプロパティに対してモデルチェックされる。 このアプローチは健全で、選択された境界まで完了しているが、候補実装の数が指数関数的に増加するため、現実的ではない。 そこで本研究では,解空間の探索に反例のバッチを用いるアルゴリズムを提案し,探索,反例のバッチ収集,活用という2つの主要なフェーズを持つ。 アプローチは健全だが、完全性は使用するバッチに依存する。 プロトタイプツールを紹介し、いくつかの実験を記述し、関連するアプローチと比較する。

関連論文リスト

• Fast sampling and model selection for Bayesian mixture models [0.6345523830122168]
  ベイズ混合モデルの積分後続分布からサンプリングする2つのモンテカルロアルゴリズムについて述べる。 最初のアルゴリズムは従来の崩壊したギブスのサンプルであり、異常な動きがある。 2つ目は最初の部分の上に構築され、以前のオーバーコンポーネントの割り当てからリジェクションなしのサンプリングを追加する。
  論文  参考訳（メタデータ） (2025-01-13T19:58:37Z)
• A Bayesian Mixture Model of Temporal Point Processes with Determinantal Point Process Prior [21.23523473330637]
  非同期イベントシーケンスクラスタリングは、教師なしの方法で類似のイベントシーケンスをグループ化することを目的としている。 私たちの研究は、イベントシーケンスクラスタリングのためのフレキシブルな学習フレームワークを提供し、潜在的なクラスタ数の自動識別を可能にします。 これは、ニューラルネットワークベースのモデルを含む幅広いパラメトリック時間点プロセスに適用できる。
  論文  参考訳（メタデータ） (2024-11-07T03:21:30Z)
• Probabilistic Modeling for Sequences of Sets in Continuous-Time [14.423456635520084]
  設定値データを連続的にモデリングするための一般的なフレームワークを開発する。 また,そのようなモデルを用いて確率的クエリに答える推論手法も開発している。
  論文  参考訳（メタデータ） (2023-12-22T20:16:10Z)
• Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
  本稿では, パール構造因果モデルにおいて, 因果関係などの部分的特定可能なクエリのバウンダリングの問題について議論する。 最近提案された反復EMスキームは初期化パラメータをサンプリングしてそれらの境界を内部近似する。 シンボルパラメータを実際の値に置き換えた回路構造を,単一のシンボル知識コンパイルによって得られることを示す。
  論文  参考訳（メタデータ） (2023-10-05T07:10:40Z)
• Single-Stage Visual Relationship Learning using Conditional Queries [60.90880759475021]
  TraCQは、マルチタスク学習問題とエンティティペアの分布を回避する、シーングラフ生成の新しい定式化である。 我々は,DETRをベースとしたエンコーダ-デコーダ条件付きクエリを用いて,エンティティラベル空間を大幅に削減する。 実験結果から、TraCQは既存のシングルステージシーングラフ生成法よりも優れており、Visual Genomeデータセットの最先端の2段階メソッドを多く上回っていることがわかった。
  論文  参考訳（メタデータ） (2023-06-09T06:02:01Z)
• Mutual Exclusivity Training and Primitive Augmentation to Induce Compositionality [84.94877848357896]
  最近のデータセットは、標準的なシーケンス・ツー・シーケンスモデルにおける体系的な一般化能力の欠如を露呈している。 本稿では,セq2seqモデルの振る舞いを分析し,相互排他バイアスの欠如と全例を記憶する傾向の2つの要因を同定する。 広範に使用されている2つの構成性データセット上で、標準的なシーケンス・ツー・シーケンスモデルを用いて、経験的改善を示す。
  論文  参考訳（メタデータ） (2022-11-28T17:36:41Z)
• Flexible Networks for Learning Physical Dynamics of Deformable Objects [2.567499374977917]
  本稿では, 粒子ベース表現を用いた変形可能な物体の将来の状態を推定するために, 時間的ポイントネット (TP-Net) というモデルを提案する。 TP-Netは、並列に設定された各入力ポイントからグローバルな特徴を抽出する共有特徴抽出器と、これらの特徴を集約して将来の予測を行う予測ネットワークから構成される。 実験により,我々のモデルは,リアルタイム予測速度で,合成データセットと実世界のデータセットの両方で最先端の性能を達成できることが実証された。
  論文  参考訳（メタデータ） (2021-12-07T14:34:52Z)
• Parameter Decoupling Strategy for Semi-supervised 3D Left Atrium Segmentation [0.0]
  本稿では,パラメータ分離戦略に基づく半教師付きセグメンテーションモデルを提案する。 提案手法は,Atrial Challengeデータセット上での最先端の半教師付き手法と競合する結果を得た。
  論文  参考訳（メタデータ） (2021-09-20T14:51:42Z)
• Complex Event Forecasting with Prediction Suffix Trees: Extended Technical Report [70.7321040534471]
  複合イベント認識(CER)システムは、イベントのリアルタイムストリーム上のパターンを"即時"検出する能力によって、過去20年間に人気が高まっている。 このような現象が実際にCERエンジンによって検出される前に、パターンがいつ発生するかを予測する方法が不足している。 複雑なイベント予測の問題に対処しようとする形式的なフレームワークを提案する。
  論文  参考訳（メタデータ） (2021-09-01T09:52:31Z)
• Modeling Sequences as Distributions with Uncertainty for Sequential Recommendation [63.77513071533095]
  既存のシーケンシャルメソッドの多くは、ユーザが決定論的であると仮定する。 項目-項目遷移は、いくつかの項目において著しく変動し、ユーザの興味のランダム性を示す。 本稿では,不確実性を逐次モデルに注入する分散型トランスフォーマーシークエンシャルレコメンデーション(DT4SR)を提案する。
  論文  参考訳（メタデータ） (2021-06-11T04:35:21Z)
• Finding Geometric Models by Clustering in the Consensus Space [61.65661010039768]
  本稿では,未知数の幾何学的モデル,例えばホモグラフィーを求めるアルゴリズムを提案する。 複数の幾何モデルを用いることで精度が向上するアプリケーションをいくつか提示する。 これには、複数の一般化されたホモグラフからのポーズ推定、高速移動物体の軌道推定が含まれる。
  論文  参考訳（メタデータ） (2021-03-25T14:35:07Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。