論文の概要: On modularity in reactive control architectures, with an application to formal verification

• arxiv url: http://arxiv.org/abs/2008.12515v3
• Date: Mon, 31 Jan 2022 02:19:04 GMT
• ステータス: 処理完了
• システム内更新日: 2022-10-24 02:12:48.352279
• Title: On modularity in reactive control architectures, with an application to formal verification
• Title（参考訳）: 形式的検証を応用したリアクティブ制御アーキテクチャのモジュール性について
• Authors: Oliver Biggar (1), Mohammad Zamani (2), Iman Shames (1) ((1) Australian National University, (2) Defence Science and Technology Group, Australia)
• Abstract要約: 決定構造と呼ぶグラフ構造制御アーキテクチャを提案する。 グラフ理論における加群の定義に触発され、決定構造における加群を定義する。 それぞれの決定構造がその加群への正準分解を持つことを示す。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Modularity is a central principle throughout the design process for cyber-physical systems. Modularity reduces complexity and increases reuse of behavior. In this paper we pose and answer the following question: how can we identify independent `modules' within the structure of reactive control architectures? To this end, we propose a graph-structured control architecture we call a decision structure, and show how it generalises some reactive control architectures which are popular in Artificial Intelligence (AI) and robotics, specifically Teleo-Reactive programs (TRs), Decision Trees (DTs), Behavior Trees (BTs) and Generalised Behavior Trees ($k$-BTs). Inspired by the definition of a module in graph theory, we define modules in decision structures and show how each decision structure possesses a canonical decomposition into its modules. We can naturally characterise each of the BTs, $k$-BTs, DTs and TRs by properties of their module decomposition. This allows us to recognise which decision structures are equivalent to each of these architectures in quadratic time. Our proposed concept of modules extends to formal verification, under any verification scheme capable of verifying a decision structure. Namely, we prove that a modification to a module within a decision structure has no greater flow-on effects than a modification to an individual action within that structure. This enables verification on modules to be done locally and hierarchically, where structures can be verified and then repeatedly locally modified, with modules replaced by modules while preserving correctness. To illustrate the findings, we present an example of a solar-powered drone controlled by a decision structure. We use a Linear Temporal Logic-based verification scheme to verify the correctness of this structure, and then show how one can modify modules while preserving its correctness.
• Abstract（参考訳）: モジュール性はサイバー物理システムの設計プロセスにおける中心的な原則である。 モジュール性は複雑さを減らし、振る舞いの再利用を促進する。 本稿では,リアクティブ制御アーキテクチャの構造において,独立した‘モジュール’をどうやって特定できるのか,という疑問に答える。 この目的のために、我々は、決定構造と呼ばれるグラフ構造制御アーキテクチャを提案し、人工知能(AI)やロボティクス、特にTeleo-Reactive Program(TR)、Decision Trees(DT)、Decision Trees(BT)、Generalized Behavior Trees(k$-BTs)で人気のあるリアクティブ制御アーキテクチャをどのように一般化するかを示す。 グラフ理論における加群の定義に着想を得て、決定構造における加群を定義し、各決定構造がその加群への正準分解を持つことを示す。 BT, $k$-BTs, DTs および TR のそれぞれを、モジュール分解の特性によって自然に特徴づけることができる。 これにより、2次時間でそれぞれのアーキテクチャにどの決定構造が等価であるかを認識することができる。 提案するモジュールの概念は,決定構造を検証可能な検証スキームの下で,形式的検証にまで拡張する。 すなわち、決定構造内のモジュールの変更が、その構造内の個々のアクションの変更よりも大きなフローオン効果を持たないことを証明する。 これにより、モジュールの検証をローカルおよび階層的に行い、構造を検証し、繰り返しローカルに修正し、モジュールをモジュールに置き換え、正確性を保ちながら行うことができる。 この結果を説明するために,意思決定構造によって制御される太陽光発電ドローンの例を示す。 線形時間論理に基づく検証手法を用いて、この構造の正しさを検証し、その正しさを保ちながらモジュールを変更する方法を示す。

関連論文リスト

• I Have an Attention Bridge to Sell You: Generalization Capabilities of Modular Translation Architectures [3.0696094577634963]
  モジュール性は翻訳品質にどう影響するか、そしてモジュールアーキテクチャが様々な評価シナリオでいかに一般化するかについて検討する。 与えられた計算予算に対して、非モジュラーアーキテクチャは、我々が研究しているすべてのモジュラー設計と常に同等か好適である。
  論文  参考訳（メタデータ） (2024-04-27T14:10:51Z)
• Pangu-Agent: A Fine-Tunable Generalist Agent with Structured Reasoning [50.47568731994238]
  人工知能(AI)エージェント作成の鍵となる方法は強化学習(RL)である 本稿では,構造化推論をAIエージェントのポリシーに統合し,学習するための一般的なフレームワークモデルを提案する。
  論文  参考訳（メタデータ） (2023-12-22T17:57:57Z)
• Discovering modular solutions that generalize compositionally [55.46688816816882]
  実演から純粋に線形変換までを識別することは、指数関数的な数の加群の組み合わせを学習することなく可能であることを示す。 さらに, 有限データからのメタラーニングにより, 多くの複雑な環境において, 構成を一般化するモジュラーポリシが発見可能であることを実証的に実証した。
  論文  参考訳（メタデータ） (2023-12-22T16:33:50Z)
• ModuleFormer: Modularity Emerges from Mixture-of-Experts [60.6148988099284]
  本稿では,大規模言語モデルの効率性と柔軟性を向上させるために,新しいニューラルネットワークアーキテクチャであるModuleFormerを提案する。 以前のSMoEベースのモジュラー言語モデルとは異なり、ModuleFormerは未処理のデータからモジュラリティを誘導することができる。
  論文  参考訳（メタデータ） (2023-06-07T17:59:57Z)
• Independent Modular Networks [3.10678167047537]
  モノリシックニューラルネットワークは、データ生成プロセスの構成的性質を排除している。 モジュールを役割に分割するモジュールネットワークアーキテクチャを提案する。 また,モジュール崩壊問題に対するモジュールネットワークのレジリエンスを改善するための正規化も提供する。
  論文  参考訳（メタデータ） (2023-06-02T07:29:36Z)
• Modular Deep Learning [120.36599591042908]
  トランスファーラーニングは近年、機械学習の主要なパラダイムとなっている。 負の干渉を伴わずに複数のタスクを専門とするモデルを開発する方法はまだ不明である。 これらの課題に対する有望な解決策として、モジュール型ディープラーニングが登場した。
  論文  参考訳（メタデータ） (2023-02-22T18:11:25Z)
• Disentangling Reasoning Capabilities from Language Models with Compositional Reasoning Transformers [72.04044221898059]
  ReasonFormerは、人間のモジュール的および構成的推論プロセスを反映するための統一的な推論フレームワークである。 表現モジュール(自動思考)と推論モジュール(制御思考)は、異なるレベルの認知を捉えるために切り離される。 統一された推論フレームワークは、単一のモデルで複数のタスクを解決し、エンドツーエンドでトレーニングされ、推論される。
  論文  参考訳（メタデータ） (2022-10-20T13:39:55Z)
• Is a Modular Architecture Enough? [80.32451720642209]
  我々は、シンプルで既知のモジュラーデータ分散のレンズを通して、共通のモジュラーアーキテクチャを徹底的に評価する。 モジュール化と疎結合のメリットを強調し、モジュール化システムの最適化において直面する課題に関する洞察を明らかにします。
  論文  参考訳（メタデータ） (2022-06-06T16:12:06Z)
• Behavior Trees in Robot Control Systems [0.0]
  振舞い木の主な考え方は、モジュラリティ、階層、フィードバックを活用することである。 ロボットタスクは、しばしばサブタスクの階層に分解されるため、そのようなモジュールの階層は自然である。 フィードバック制御は、低レベル制御システムにおける不確実性と障害を扱うための基本的なツールである。
  論文  参考訳（メタデータ） (2022-03-24T14:16:15Z)
• Robustness modularity in complex networks [1.749935196721634]
  本稿では,ロバストネスの概念に基づく新しい尺度を提案する。 ロバスト性モジュラリティは、ネットワークの構造がランダムに摂動しているときに、自明な分割を見つける確率である。 人工グラフと実グラフの試験により、異なるネットワークのコミュニティ構造の強度を評価し比較するために、ロバスト性モジュラリティが利用できることが明らかになった。
  論文  参考訳（メタデータ） (2021-10-05T19:00:45Z)
• Cognitive Capabilities for the CAAI in Cyber-Physical Production Systems [2.348805691644086]
  本稿では,サイバー物理生産システム(CPPS)における人工知能(CAAI)の認知モジュールについて述べる。 宣言的なユーザ目標と提供されたアルゴリズム知識ベースによって、動的パイプラインのオーケストレーションとコンフィギュレーションが可能になる。 ビッグデータプラットフォーム(BDP)はパイプラインをインスタンス化し、CPPSパフォーマンスを監視してさらなる評価を行う。
  論文  参考訳（メタデータ） (2020-12-03T10:55:56Z)

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

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