論文の概要: Verification of Quantitative Temporal Properties in RealTime-DEVS
- arxiv url: http://arxiv.org/abs/2409.18732v1
- Date: Fri, 27 Sep 2024 13:23:24 GMT
- ステータス: 処理完了
- システム内更新日: 2024-10-01 15:09:41.723384
- Title: Verification of Quantitative Temporal Properties in RealTime-DEVS
- Title(参考訳): リアルタイムDEVSにおける定量的時間特性の検証
- Authors: Ariel González, Maximiliano Cristiá, Carlos Luna,
- Abstract要約: リアルタイムDEVSは、定量的な時間的要求を伴うシステムをモデル化することができる。
RT-DEVSモデルに現れる反復的量的時間特性のクラスを検証するために、モデルチェッカーUppaalを使用する。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/publicdomain/zero/1.0/
- Abstract: Real-Time DEVS (RT-DEVS) can model systems with quantitative temporal requirements. Ensuring that such models verify some temporal properties requires to use something beyond simulation. In this work we use the model checker Uppaal to verify a class of recurrent quantitative temporal properties appearing in RT-DEVS models. Secondly, by introducing mutations to quantitative temporal properties we are able to find errors in RT-DEVS models and their implementations. A case study from the railway domain is presented.
- Abstract(参考訳): Real-Time DEVS (RT-DEVS) は、定量的な時間的要求を持つシステムをモデル化することができる。
そのようなモデルがいくつかの時間的特性を検証するためには、シミュレーション以上のものを使用する必要がある。
本研究では,RT-DEVSモデルで繰り返し発生する定量的時間特性のクラスを検証するために,モデルチェッカーUppaalを使用する。
次に、定量的時間特性に突然変異を導入することで、RT-DEVSモデルとその実装にエラーを見つけることができる。
鉄道ドメインのケーススタディが紹介されている。
関連論文リスト
- DOTA: Distributional Test-Time Adaptation of Vision-Language Models [52.98590762456236]
トレーニングフリーテスト時動的アダプタ(TDA)は、この問題に対処するための有望なアプローチである。
単体テスト時間適応法(Dota)の簡易かつ効果的な方法を提案する。
Dotaは継続的にテストサンプルの分布を推定し、モデルがデプロイメント環境に継続的に適応できるようにします。
論文 参考訳(メタデータ) (2024-09-28T15:03:28Z) - Graph Spatiotemporal Process for Multivariate Time Series Anomaly
Detection with Missing Values [67.76168547245237]
本稿では,グラフ時間過程と異常スコアラを用いて異常を検出するGST-Proという新しいフレームワークを提案する。
実験結果から,GST-Pro法は時系列データ中の異常を効果的に検出し,最先端の手法より優れていることがわかった。
論文 参考訳(メタデータ) (2024-01-11T10:10:16Z) - Explainable Time Series Anomaly Detection using Masked Latent Generative Modeling [1.3927943269211591]
本稿では,新しい時系列異常検出法であるTimeVQVAE-ADを提案する。
TimeVQVAE-ADは、優れた説明性を提供しながら、優れた検出精度を実現する。
私たちはGitHubに実装を提供しています。
論文 参考訳(メタデータ) (2023-11-21T11:59:16Z) - OpenSTL: A Comprehensive Benchmark of Spatio-Temporal Predictive
Learning [67.07363529640784]
提案するOpenSTLは,一般的なアプローチを再帰的モデルと再帰的モデルに分類する。
我々は, 合成移動物体軌道, 人間の動き, 運転シーン, 交通流, 天気予報など, さまざまな領域にわたるデータセットの標準評価を行う。
リカレントフリーモデルは、リカレントモデルよりも効率と性能のバランスが良いことがわかった。
論文 参考訳(メタデータ) (2023-06-20T03:02:14Z) - Artificial neural networks and time series of counts: A class of
nonlinear INGARCH models [0.0]
INGARCHモデルを人工知能ニューラルネットワーク(ANN)応答関数と組み合わせて非線形INGARCHモデルのクラスを得る方法を示す。
ANNフレームワークは、対応するニューラルモデルの退化バージョンとして、既存のINGARCHモデルの解釈を可能にする。
有界数と非有界数の時系列の実証分析により、ニューラルINGARCHモデルは、情報損失の観点から、合理的に退化した競合モデルより優れていることが示された。
論文 参考訳(メタデータ) (2023-04-03T14:26:16Z) - Gated Recurrent Neural Networks with Weighted Time-Delay Feedback [59.125047512495456]
重み付き時間遅延フィードバック機構を備えた新しいゲートリカレントユニット(GRU)を導入する。
我々は、$tau$-GRUが、最先端のリカレントユニットやゲート型リカレントアーキテクチャよりも早く収束し、より一般化できることを示します。
論文 参考訳(メタデータ) (2022-12-01T02:26:34Z) - Discovering Dynamic Patterns from Spatiotemporal Data with Time-Varying
Low-Rank Autoregression [12.923271427789267]
低ランクテンソル因子化により係数がパラメータ化される時間還元ベクトル自己回帰モデルを開発した。
時間的文脈において、複雑な時間変化系の挙動は、提案モデルにおける時間的モードによって明らかにすることができる。
論文 参考訳(メタデータ) (2022-11-28T15:59:52Z) - TILDE-Q: A Transformation Invariant Loss Function for Time-Series
Forecasting [8.086595073181604]
時系列予測は、エネルギー、天気、交通、経済など、さまざまな領域における現実世界の問題に対処することができる。
時系列予測はよく研究されている分野であり、シーケンシャルデータの急激な変化などの複雑な時間的パターンを予測することは、現在のモデルでは依然として課題となっている。
本稿では, 振幅および位相歪みだけでなく, 時系列列の形状をモデルで捉えることができる, TILDEQ と呼ばれる新しいコンパクトな損失関数を提案する。
論文 参考訳(メタデータ) (2022-10-26T21:32:20Z) - TACTiS: Transformer-Attentional Copulas for Time Series [76.71406465526454]
時間変化量の推定は、医療や金融などの分野における意思決定の基本的な構成要素である。
本稿では,アテンションベースデコーダを用いて関節分布を推定する多元的手法を提案する。
本研究では,本モデルが実世界の複数のデータセットに対して最先端の予測を生成することを示す。
論文 参考訳(メタデータ) (2022-02-07T21:37:29Z) - Anomaly Detection of Time Series with Smoothness-Inducing Sequential
Variational Auto-Encoder [59.69303945834122]
Smoothness-Inducing Sequential Variational Auto-Encoder (SISVAE) モデルを提案する。
我々のモデルは、フレキシブルニューラルネットワークを用いて各タイムスタンプの平均と分散をパラメータ化する。
合成データセットと公開実世界のベンチマークの両方において,本モデルの有効性を示す。
論文 参考訳(メタデータ) (2021-02-02T06:15:15Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。