論文の概要: A Note on Runtime Verification of Concurrent Systems

• arxiv url: http://arxiv.org/abs/2507.04830v1
• Date: Mon, 07 Jul 2025 09:50:59 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-07-08 15:46:35.367123
• Title: A Note on Runtime Verification of Concurrent Systems
• Title（参考訳）: 並行システムの実行時検証に関する一考察
• Authors: Martin Leucker,
• Abstract要約: 本稿では,トレースベースの論理を利用して並列システムの検証を行う方法を提案する。 本稿は,LTrL式のためのトレース一貫性B"uchi Automaticaの構築を思い出し,よく理解されたモニタ合成手順でどのように利用するかを説明する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: To maximize the information gained from a single execution when verifying a concurrent system, one can derive all concurrency-aware equivalent executions and check them against linear specifications. This paper offers an alternative perspective on verification of concurrent systems by leveraging trace-based logics rather than sequence-based formalisms. Linear Temporal Logic over Mazurkiewicz Traces (LTrL) operates on partial-order representations of executions, meaning that once a single execution is specified, all equivalent interleavings are implicitly considered. This paper introduces a three valued version of LTrL, indicating whether the so-far observed execution of the concurrent system is one of correct, incorrect or inconclusive, together with a suitable monitor synthesis procedure. To this end, the paper recalls a construction of trace-consistent B\"uchi automata for LTrL formulas and explains how to employ it in well-understood monitor synthesis procedures. In this way, a monitor results that yields for any linearization of an observed trace the same verification verdict.
• Abstract（参考訳）: 並列システムを検証する場合、単一の実行から得られる情報を最大化するために、すべての並行性を考慮した等価な実行を導出し、それらを線形仕様に対してチェックすることができる。 本稿では、列ベースの形式よりもトレースベースの論理を活用することで、並列システムの検証に代替的な視点を提供する。 Mazurkiewicz Traces (LTrL) 上の線形時間論理は、実行の部分順序表現で動作し、単一の実行が指定されると、すべての等価なインターリーブが暗黙的に考慮される。 本稿では,LTrLの3つの評価版を紹介し,並列システムの極端に観察された実行が,適切なモニタ合成手順とともに正しいか,正しくないか,それとも不確定かを示す。 この目的のために、LTrL式のためのトレース一貫性B\"uchi Automaticaの構築をリコールし、よく理解されたモニタ合成手順でどのように利用するかを説明する。 このようにして、観測されたトレースの線形化を導出するモニタ結果が、同じ検証結果となる。

関連論文リスト

• SPARE: Single-Pass Annotation with Reference-Guided Evaluation for Automatic Process Supervision and Reward Modelling [70.01883340129204]
  シングルパス。 リファレンスガイドによる評価(SPARE) 参照ソリューションにおける各ソリューションステップを1つまたは複数のステップにアライメントすることで、単一のパス毎のアノテーションを可能にする新しい構造化フレームワーク。 SPAREは2.6倍の効率を実現し、実行時の38%しか必要としない。
  論文  参考訳（メタデータ） (2025-06-18T14:37:59Z)
• Execution Guided Line-by-Line Code Generation [49.1574468325115]
  本稿では,言語モデル生成プロセスにリアルタイム実行信号を組み込んだニューラルコード生成手法を提案する。 提案手法であるExecutionGuidedFree Guidance (EGCFG) は,実行信号をモデルが生成するコードとして組み込む。
  論文  参考訳（メタデータ） (2025-06-12T17:50:05Z)
• Self-Calibrated Listwise Reranking with Large Language Models [137.6557607279876]
  大規模言語モデル (LLM) はシーケンシャル・ツー・シーケンス・アプローチによってタスクのランク付けに使用されている。 この階調のパラダイムは、より大きな候補集合を反復的に扱うためにスライディングウインドウ戦略を必要とする。 そこで本稿では,LLMを用いた自己校正リストのランク付け手法を提案する。
  論文  参考訳（メタデータ） (2024-11-07T10:31:31Z)
• Runtime Instrumentation for Reactive Components (Extended Version) [0.0]
  リアクティブソフトウェアは、システムのリアクティブ属性を裏付けるインスツルメンテーションメソッドを要求する。 本稿では,この2つの要求を満たすアウトラインモニタのための分散インスツルメンテーションアルゴリズムであるRIARCを提案する。 RIARCは次のホップIPルーティングアプローチを使ってこれらの課題を克服し、イベントを再配置し、モニタに適切に報告する。
  論文  参考訳（メタデータ） (2024-06-28T13:18:04Z)
• Bisimulation Learning [55.859538562698496]
  我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。 提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
  論文  参考訳（メタデータ） (2024-05-24T17:11:27Z)
• Tooling Offline Runtime Verification against Interaction Models : recognizing sliced behaviors using parameterized simulation [0.4199844472131921]
  オフライン実行時の検証には、仕様に対するシステムの実行の静的解析が含まれる。 分散システムでは、グローバルクロックが存在しないため、グローバルトレースの形での実行を特徴付けることは一般的に不可能である。 本稿では,インタラクションと呼ばれる形式仕様に対して,そのようなトレースの適合性を検証するアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2024-03-05T16:09:55Z)
• Sound Concurrent Traces for Online Monitoring Technical Report [0.0]
  並列プログラムは通常、抽象的なプログラム実行のためのトレースの収集に依存します。 まず、トレースが並列実行を表すときの概念を定義します。 次に,非ブロッキングベクトルクロックアルゴリズムを提案し,音の同時トレースをハエで収集する。
  論文  参考訳（メタデータ） (2024-02-28T15:11:39Z)
• Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
  システム実行から形式仕様を自動合成する問題を考察する。 時間論理式を合成するための古典的なアプローチの多くは、公式のサイズを最小化することを目的としている。 我々は,この概念を定式化し,有界な外見を持つ簡潔な公式を合成する学習アルゴリズムを考案する。
  論文  参考訳（メタデータ） (2023-10-26T14:13:15Z)
• Monitoring Algorithmic Fairness under Partial Observations [3.790015813774933]
  実行時検証技術は、デプロイされたシステムのアルゴリズム的公正性を監視するために導入された。 従来の監視技術は、監視されたシステムの状態の完全な可観測性を前提としている。 我々は、部分的に観測されたマルコフ連鎖としてモデル化されたシステムにフェアネスモニタリングを拡張した。
  論文  参考訳（メタデータ） (2023-08-01T07:35:54Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  我々はCoCoMoT(Computing Conformance Modulo Theories)フレームワークを紹介する。 まず、純粋な制御フロー設定で研究したSATベースのエンコーディングを、データ認識ケースに持ち上げる方法を示す。 次に,プロパティ保存型クラスタリングの概念に基づく新しい前処理手法を提案する。
  論文  参考訳（メタデータ） (2021-03-18T20:22:50Z)

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

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