論文の概要: Deciding branching hyperproperties for real time systems
- arxiv url: http://arxiv.org/abs/2405.12104v1
- Date: Mon, 20 May 2024 15:21:12 GMT
- ステータス: 処理完了
- システム内更新日: 2024-05-21 12:25:40.660495
- Title: Deciding branching hyperproperties for real time systems
- Title（参考訳）: リアルタイムシステムのための分岐ハイパープロパティの決定
- Authors: Nabarun Deka, Minjian Zhang, Rohit Chadha, Mahesh Viswanathan,
- Abstract要約: リアルタイムシステムのセキュリティ特性は、しばしば超越性についての推論を伴う。
このような特性の例としては、情報フロー、サイドチャネルアタック、サービスレベルの合意などがある。
- 参考スコア（独自算出の注目度）: 1.1892416745067433
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Security properties of real-time systems often involve reasoning about hyper-properties, as opposed to properties of single executions or trees of executions. These hyper-properties need to additionally be expressive enough to reason about real-time constraints. Examples of such properties include information flow, side channel attacks and service-level agreements. In this paper we study computational problems related to a branching-time, hyper-property extension of metric temporal logic (MTL) that we call HCMTL*. We consider both the interval-based and point-based semantics of this logic. The verification problem that we consider is to determine if a given HCMTL* formula $\varphi$ is true in a system represented by a timed automaton. We show that this problem is undecidable. We then show that the verification problem is decidable if we consider executions upto a fixed time horizon $T$. Our decidability result relies on reducing the verification problem to the truth of an MSO formula over reals with a bounded time interval.
- Abstract（参考訳）: リアルタイムシステムのセキュリティ特性は、単一の実行や実行ツリーのプロパティとは対照的に、しばしばハイパープロパティに関する推論を伴う。
これらの超越性は、リアルタイムの制約について考えるのに十分な表現力を持つ必要がある。
このような特性の例としては、情報フロー、サイドチャネルアタック、サービスレベルの合意などがある。
本稿では,HCMTL*と呼ぶ計量時相論理(MTL)の分岐時間,超完全性拡張に関連する計算問題について検討する。
この論理のインターバルベースとポイントベースのセマンティクスの両方を考慮する。
我々が考慮する検証問題は、時間付きオートマトンで表されるシステムにおいて、与えられたHCMTL*式$\varphi$が真かどうかを決定することである。
私たちはこの問題が決定不能であることを示します。
次に、一定の時間的地平線までの実行を考えると、検証問題は決定可能であることを示す。
我々の決定性は、時間間隔が制限された実数上の MSO 公式の真理に検証問題を還元することに依存する。
関連論文リスト
- On the Identification of Temporally Causal Representation with Instantaneous Dependence [50.14432597910128]
時間的因果表現学習は時系列観測から潜在因果過程を特定することを目的としている。
ほとんどの方法は、潜在因果過程が即時関係を持たないという仮定を必要とする。
我々は,インスタントtextbfOus textbfLatent dynamics のための textbfIDentification フレームワークを提案する。
論文 参考訳（メタデータ） (2024-05-24T08:08:05Z) - Non-Deterministic Planning for Hyperproperty Verification [4.726777092009553]
提案手法は,ハイパープロパティの自動検証に強力な中間言語を提供することを示す。
本稿では,HyperLTL検証問題に対して,非決定論的マルチエージェント計画インスタンスを構築するアルゴリズムを提案する。
提案手法は,HyperLTLの大きな断片に対して,従来のFOND,あるいはPOND計画問題に対応していることを示す。
論文 参考訳（メタデータ） (2024-05-22T09:57:49Z) - DASA: Delay-Adaptive Multi-Agent Stochastic Approximation [64.32538247395627]
我々は,N$エージェントが並列に動作し,中央サーバと通信することで,一般的な近似問題を高速化することを目的とした設定を考える。
遅延とストラグラーの効果を軽減するために,マルチエージェント近似のための遅延適応アルゴリズムである textttDASA を提案する。
論文 参考訳（メタデータ） (2024-03-25T22:49:56Z) - Stochastic Approximation with Delayed Updates: Finite-Time Rates under Markovian Sampling [73.5602474095954]
マルコフサンプリングの遅延更新による近似スキームの非漸近的性能について検討した。
我々の理論的な発見は、幅広いアルゴリズムの遅延の有限時間効果に光を当てた。
論文 参考訳（メタデータ） (2024-02-19T03:08:02Z) - Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
システム実行から形式仕様を自動合成する問題を考察する。
時間論理式を合成するための古典的なアプローチの多くは、公式のサイズを最小化することを目的としている。
我々は,この概念を定式化し,有界な外見を持つ簡潔な公式を合成する学習アルゴリズムを考案する。
論文 参考訳（メタデータ） (2023-10-26T14:13:15Z) - HyperAttention: Long-context Attention in Near-Linear Time [78.33061530066185]
本稿では,長期的文脈の複雑さの増大に伴う計算課題に対処するため,HyperAttentionという近似的な注意機構を提案する。
実証的には、大規模なエントリを特定するためにLocality Sensitive Hashing(LSH)を使用して、HyperAttentionは既存のメソッドよりも優れています。
各種長文長データセットにおけるHyperAttentionの実証的性能を検証した。
論文 参考訳（メタデータ） (2023-10-09T17:05:25Z) - A direct optimization algorithm for input-constrained MPC [3.0992677770545254]
この技術ノートは、入力制約付きMPC問題を考察し、その結果のボックス制約付きQPの構造を利用する。
提案アルゴリズムの反復回数はテキストのみに依存していることを示す。
提案アルゴリズムの実行時認証能力は,オープンループ不安定AFTI-16例を用いて理論的,数値的に検証する。
論文 参考訳（メタデータ） (2023-06-26T21:39:14Z) - Execution Time Program Verification With Tight Bounds [6.36836017515443]
本稿では,コア命令型プログラミング言語の実行時間境界を推論するための証明システムを提案する。
3つのケースに対してHoareロジックを定義し、注釈付きコスト対応操作セマンティクスに関してその健全性を証明する。
証明システムの実用性は、サンプルプログラムに適用するために必要な異なるモジュールのOCamlの実装で実証される。
論文 参考訳（メタデータ） (2022-10-20T09:02:13Z) - On the Complexity of Rational Verification [5.230352342979224]
合理的検証とは、同時マルチエージェントシステムの時間論理特性が保持する問題を指す。
合理的な検証の複雑さは仕様によって大幅に低減できることを示す。
平均支払ユーティリティ関数によって与えられるプレイヤーの目標を考慮した場合、合理的な検証のための改善された結果を提供する。
論文 参考訳（メタデータ） (2022-07-06T12:56:22Z) - Acting in Delayed Environments with Non-Stationary Markov Policies [57.52103323209643]
本稿では,MDPにおける学習と計画のためのフレームワークについて紹介する。
実行が遅れると、元の状態空間における決定論的マルコフポリシーは最大報酬を得るのに十分であるが、非定常である必要があることを証明します。
我々は、状態拡張に頼らずに遅延実行タスクを解く非定常Q学習スタイルのモデルベースアルゴリズムを考案した。
論文 参考訳（メタデータ） (2021-01-28T13:35:37Z) - Logically Consistent Loss for Visual Question Answering [66.83963844316561]
ニューラルネットワークに基づく視覚質問応答(VQA)の現在の進歩は、同じ分布(すなわち、d)の仮定による一貫性を保証することができない。
マルチタスク学習フレームワークにおける論理的一貫した損失を定式化することにより,この問題に対処するための新しいモデルに依存しない論理制約を提案する。
実験により、提案された損失公式とハイブリッドバッチの導入により、一貫性が向上し、性能が向上することを確認した。
論文 参考訳（メタデータ） (2020-11-19T20:31:05Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。