論文の概要: Keeping Behavioral Programs Alive: Specifying and Executing Liveness Requirements

• arxiv url: http://arxiv.org/abs/2404.01858v1
• Date: Tue, 2 Apr 2024 11:36:58 GMT
• ステータス: 処理完了
• システム内更新日: 2024-04-03 16:49:07.424168
• Title: Keeping Behavioral Programs Alive: Specifying and Executing Liveness Requirements
• Title（参考訳）: 行動プログラムを存続させる: 生活必需品の特定と実行
• Authors: Tom Yaacov, Achiya Elyasaf, Gera Weiss,
• Abstract要約: タスクがまだ完了していないことを示すために,"must-finish"を付けたタグ付け状態のイディオムを提案する。 また,B"uchiautoaへの翻訳に基づくセマンティクスと,マルコフ決定プロセス(MDP)に基づく2つの実行メカニズムも提供する。
• 参考スコア（独自算出の注目度）: 2.4387555567462647
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: One of the benefits of using executable specifications such as Behavioral Programming (BP) is the ability to align the system implementation with its requirements. This is facilitated in BP by a protocol that allows independent implementation modules that specify what the system may, must, and must not do. By that, each module can enforce a single system requirement, including negative specifications such as "don't do X after Y." The existing BP protocol, however, allows only the enforcement of safety requirements and does not support the execution of liveness properties such as "do X at least three times." To model liveness requirements in BP directly and independently, we propose idioms for tagging states with "must-finish," indicating that tasks are yet to be completed. We show that this idiom allows a direct specification of known requirements patterns from the literature. We also offer semantics and two execution mechanisms, one based on a translation to B\"uchi automata and the other based on a Markov decision process (MDP). The latter approach offers the possibility of utilizing deep reinforcement learning (DRL) algorithms, which bear the potential to handle large software systems effectively. This paper presents a qualitative and quantitative assessment of the proposed approach using a proof-of-concept tool. A formal analysis of the MDP-based execution mechanism is given in an appendix.
• Abstract（参考訳）: 振舞いプログラミング(BP)のような実行可能な仕様を使用する利点の1つは、システム実装をその要件と整合させる能力である。 これはBPにおいて、システムができること、すべきこと、すべきでないことを指定する独立した実装モジュールを許可するプロトコルによって促進される。 これにより、各モジュールは "Don't do X after Y" などの負の仕様を含む単一のシステム要件を強制することができる。 しかし、既存のBPプロトコルは、安全要件の実施のみを許可し、「少なくとも3回はXを行う」といった生活特性の実行をサポートしない。 BPの寿命要件を直接かつ独立にモデル化するために,タスクがまだ完了していないことを示す"must-finish"のタグ付け状態のイディオムを提案する。 このイディオムは、文献から既知の要求パターンを直接指定できることを示す。 また,B\"uchi Automaticaへの翻訳に基づくセマンティクスと,マルコフ決定プロセス(MDP)に基づく2つの実行メカニズムも提供する。 後者のアプローチは、大規模ソフトウェアシステムを効果的に扱う可能性を秘めている、深層強化学習(DRL)アルゴリズムを活用する可能性を提供する。 本稿では,概念実証ツールを用いて,提案手法の質的,定量的な評価を行う。 MDPベースの実行機構の形式解析を付録に記載する。

関連論文リスト

• Towards an Enforceable GDPR Specification [49.1574468325115]
  プライバシ・バイ・デザイン(PbD)は、EUなどの現代的なプライバシー規制によって規定されている。 PbDを実現する1つの新しい技術は強制(RE)である 法律規定の正式な仕様を作成するための一連の要件と反復的な方法論を提示する。
  論文  参考訳（メタデータ） (2024-02-27T09:38:51Z)
• LLM-based policy generation for intent-based management of applications [8.938462415711674]
  本稿では、ポリシーベースの抽象化を用いて必要なアクションを生成することにより、インテントを段階的に分解するパイプラインを提案する。 これにより、意図的なデプロイメントのためのクローズドコントロールループを作成することで、ポリシの実行を自動化することができます。 仮想ネットワーク機能のアプリケーションサービスチェーンを満足し、保証するためのユースケースで提案する。
  論文  参考訳（メタデータ） (2024-01-22T15:37:04Z)
• Conformance Checking for Pushdown Reactive Systems based on Visibly Pushdown Languages [0.0]
  プッシュダウンリアクティブシステムをテストすることは、正確で堅牢なソフトウェア開発プロセスを保証する上で重要であると考えられている。 本稿では,この整合性関係を用いて完全な障害カバレッジを持つテストスイートを,プッシュダウンリアクティブシステムに生成可能であることを示す。
  論文  参考訳（メタデータ） (2023-08-14T14:37:43Z)
• Towards Semantic Communication Protocols: A Probabilistic Logic Perspective [69.68769942563812]
  我々は,NPMを確率論理型言語ProbLogで記述された解釈可能なシンボルグラフに変換することによって構築された意味プロトコルモデル(SPM)を提案する。 その解釈性とメモリ効率を利用して、衝突回避のためのSPM再構成などのいくつかの応用を実演する。
  論文  参考訳（メタデータ） (2022-07-08T14:19:36Z)
• Reinforcement Learning for Task Specifications with Action-Constraints [4.046919218061427]
  有限状態マルコフ決定過程の最適制御ポリシーを学習する手法を提案する。 安全でないと考えられるアクションシーケンスの集合が有限状態オートマトンによって与えられると仮定する。 非マルコフ的行動系列と状態制約の存在下で最適なポリシーを学習するためのQ-learningアルゴリズムのバージョンを提案する。
  論文  参考訳（メタデータ） (2022-01-02T04:22:01Z)
• Pointwise Feasibility of Gaussian Process-based Safety-Critical Control under Model Uncertainty [77.18483084440182]
  制御バリア関数(CBF)と制御リアプノフ関数(CLF)は、制御システムの安全性と安定性をそれぞれ強化するための一般的なツールである。 本稿では, CBF と CLF を用いた安全クリティカルコントローラにおいて, モデル不確実性に対処するためのガウスプロセス(GP)に基づくアプローチを提案する。
  論文  参考訳（メタデータ） (2021-06-13T23:08:49Z)
• Modular Deep Reinforcement Learning for Continuous Motion Planning with Temporal Logic [59.94347858883343]
  本稿では,マルコフ決定過程(MDP)をモデルとした自律動的システムの運動計画について検討する。 LDGBA と MDP の間に組込み製品 MDP (EP-MDP) を設計することである。 モデルフリー強化学習(RL)のためのLDGBAベースの報酬形成と割引スキームは、EP-MDP状態にのみ依存する。
  論文  参考訳（メタデータ） (2021-02-24T01:11:25Z)
• SMT-based Safety Verification of Parameterised Multi-Agent Systems [78.04236259129524]
  パラメータ化マルチエージェントシステム(MAS)の検証について検討する。 特に、与えられた状態公式として特徴づけられる不要な状態が、所定のMASで到達可能かどうかについて検討する。
  論文  参考訳（メタデータ） (2020-08-11T15:24:05Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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