論文の概要: Verification of Digital Twins using Classical and Statistical Model Checking

• arxiv url: http://arxiv.org/abs/2505.04322v1
• Date: Wed, 07 May 2025 11:12:46 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-08 19:07:36.050685
• Title: Verification of Digital Twins using Classical and Statistical Model Checking
• Title（参考訳）: 古典的・統計的モデル検査によるデジタル双生児の検証
• Authors: Raghavendran Gunasekaran, Boudewijn Haverkort,
• Abstract要約: デジタルツイン(DT)の概念は、産業と学術の両方で広く注目を集めている。 自律走行トラックのDTにこれらの技術を適用した結果について報告する。 これらの検証手法の結果、このDTはデッドロック自由度と機能的正しさの性質に固執するが、タイムラインの性質に固執するものではないことが示唆された。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: With the increasing adoption of digital techniques, the concept of digital twin (DT) has received a widespread attention in both industry and academia. While several definitions exist for a DT, most definitions focus on the existence of a virtual entity (VE) of a real-world object or process, often comprising interconnected models which interact with each other, undergoing changes continuously owing to the synchronization with the real-world object. These interactions might lead to inconsistencies at execution time, due to their highly stochastic and/or time-critical nature, which may lead to undesirable behavior. In addition, the continuously varying nature of VE owing to its synchronization with the real-world object further contributes to the complexity arising from these interactions and corresponding model execution times, which could possibly affect its overall functioning at runtime. This creates a need to perform (continuous) verification of the VE, to ensure that it behaves consistently at runtime by adhering to desired properties such as deadlock freeness, functional correctness, liveness and timeliness. Some critical properties such as deadlock freeness can only be verified using classical model checking; on the other hand, statistical model checking provides the possibility to model actual stochastic temporal behavior. We therefore propose to use both these techniques to verify the correctness and the fulfillment of desirable properties of VE. We present our observations and findings from applying these techniques on the DT of an autonomously driving truck. Results from these verification techniques suggest that this DT adheres to properties of deadlock freeness and functional correctness, but not adhering to timeliness properties.
• Abstract（参考訳）: デジタル技術の普及に伴い、デジタルツイン(DT)の概念は産業とアカデミックの両方で広く注目を集めている。 DTにはいくつかの定義があるが、ほとんどの定義は現実世界のオブジェクトやプロセスの仮想エンティティ(VE)の存在に焦点を当てている。 これらの相互作用は、非常に確率的かつ/または時間クリティカルな性質のため、実行時に不整合を引き起こし、望ましくない振る舞いを引き起こす可能性がある。 さらに、実世界のオブジェクトとの同期によって連続的に変化するVEの性質は、これらの相互作用とそれに対応するモデル実行時間から生じる複雑さにさらに寄与し、実行時の全体的な機能に影響を与える可能性がある。 これにより、デッドロック自由性、機能的正当性、生存性、タイムラインなどの望ましい特性に固執することで、VEの(連続的な)検証を実行する必要がある。 デッドロック自由性のようないくつかの重要な性質は古典的なモデル検査によってのみ検証できるが、統計モデル検査は実際の確率的時間的挙動をモデル化することができる。 そこで本稿では,これらの手法を用いて,VEの望ましい特性の正しさと満足度を検証することを提案する。 自律走行トラックのDTにこれらの技術を適用した結果について報告する。 これらの検証手法の結果、このDTはデッドロック自由度と機能的正しさの性質に固執するが、タイムラインの性質に固執するものではないことが示唆された。

関連論文リスト

• On the Identification of Temporally Causal Representation with Instantaneous Dependence [50.14432597910128]
  時間的因果表現学習は時系列観測から潜在因果過程を特定することを目的としている。 ほとんどの方法は、潜在因果過程が即時関係を持たないという仮定を必要とする。 我々は,インスタントtextbfOus textbfLatent dynamics のための textbfIDentification フレームワークを提案する。
  論文  参考訳（メタデータ） (2024-05-24T08:08:05Z)
• A Poisson-Gamma Dynamic Factor Model with Time-Varying Transition Dynamics [51.147876395589925]
  非定常PGDSは、基礎となる遷移行列が時間とともに進化できるように提案されている。 後続シミュレーションを行うために, 完全共役かつ効率的なギブスサンプリング装置を開発した。 実験により,提案した非定常PGDSは,関連するモデルと比較して予測性能が向上することを示した。
  論文  参考訳（メタデータ） (2024-02-26T04:39:01Z)
• Object-Centric Conformance Alignments with Synchronization (Extended Version) [57.76661079749309]
  対象中心のペトリネットが一対多の関係を捉える能力と,その同一性に基づいたオブジェクトの比較と同期を行う識別子を持つペトリネットの能力を組み合わせた,新たな形式主義を提案する。 我々は、満足度変調理論(SMT)の符号化に基づく、そのようなネットに対する適合性チェック手法を提案する。
  論文  参考訳（メタデータ） (2023-12-13T21:53:32Z)
• Introducing 3DCNN ResNets for ASD full-body kinematic assessment: a comparison with hand-crafted features [1.3499500088995464]
  本稿では,新しい3DCNN ResNetを提案するとともに,モータASD評価に広く用いられている手作り機能と比較する。 具体的には、複数のモータータスクと、両方のアプローチを用いたトレーニングモデルを備えたバーチャルリアリティ環境を開発した。 その結果,提案モデルでは最大85$pm$3%の精度を達成し,短い1～3分間のサンプルで最先端のエンド・ツー・エンドモデルを上回る結果を得た。
  論文  参考訳（メタデータ） (2023-11-24T14:56:36Z)
• TimeTuner: Diagnosing Time Representations for Time-Series Forecasting with Counterfactual Explanations [3.8357850372472915]
  本稿では,モデル行動が局所化,定常性,時系列表現の相関とどのように関連しているかをアナリストが理解するために,新しいビジュアル分析フレームワークであるTimeTunerを提案する。 TimeTunerは時系列表現を特徴付けるのに役立ち、機能エンジニアリングのプロセスを導くのに役立ちます。
  論文  参考訳（メタデータ） (2023-07-19T11:40:15Z)
• Edge Continual Learning for Dynamic Digital Twins over Wireless Networks [68.65520952712914]
  デジタルツイン(DT)は、現実世界とメタバースの間の重要なリンクを構成する。 本稿では,物理的双生児とそれに対応するサイバー双生児の親和性を正確にモデル化する新しいエッジ連続学習フレームワークを提案する。 提案するフレームワークは,破滅的忘れ込みに対して頑健な,高精度かつ同期的なCTモデルを実現する。
  論文  参考訳（メタデータ） (2022-04-10T23:25:37Z)

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

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