論文の概要: Timed Actors and Their Formal Verification
- arxiv url: http://arxiv.org/abs/2309.07302v1
- Date: Wed, 13 Sep 2023 20:50:11 GMT
- ステータス: 処理完了
- システム内更新日: 2023-10-23 07:50:34.673903
- Title: Timed Actors and Their Formal Verification
- Title（参考訳）: 時間的アクターとその形式的検証
- Authors: Marjan Sirjani, Ehsan Khamespanah
- Abstract要約: Timed Rebecaは非同期メッセージパッシングによって通信するカプセル化されたコンポーネントで構成されるシステムをモデル化するために使用することができる。
本稿では,FTTS (Floating-Time Transition System) とTTS (Common Timed Transition System) の両方を,これらのモデルのセマンティクスとして用いる方法について説明する。
モデルチェックツールセットは、スケジューリング可能性分析、デッドロックとキューオーバーフローチェック、アサーションベースのTimed Rebecaモデルの検証をサポートする。
- 参考スコア（独自算出の注目度）: 0.21756081703275998
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: In this paper we review the actor-based language, Timed Rebeca, with a focus
on its formal semantics and formal verification techniques. Timed Rebeca can be
used to model systems consisting of encapsulated components which communicate
by asynchronous message passing. Messages are put in the message buffer of the
receiver actor and can be seen as events. Components react to these
messages/events and execute the corresponding message/event handler. Real-time
features, like computation delay, network delay and periodic behavior, can be
modeled in the language. We explain how both Floating-Time Transition System
(FTTS) and common Timed Transition System (TTS) can be used as the semantics of
such models and the basis for model checking. We use FTTS when we are
interested in event-based properties, and it helps in state space reduction.
For checking the properties based on the value of variables at certain point in
time, we use the TTS semantics. The model checking toolset supports
schedulability analysis, deadlock and queue-overflow check, and assertion based
verification of Timed Rebeca models. TCTL model checking based on TTS is also
possible but is not integrated in the tool.
- Abstract（参考訳）: 本稿では,アクタベースの言語であるtimed rebecaについて,その形式的意味論と形式的検証技術に注目して検討する。
Timed Rebecaは非同期メッセージパッシングによって通信するカプセル化されたコンポーネントで構成されるシステムをモデル化するために使用できる。
メッセージは受信者アクタのメッセージバッファに置かれ、イベントとして見ることができる。
コンポーネントはこれらのメッセージ/イベントに応答し、対応するメッセージ/イベントハンドラを実行する。
計算遅延、ネットワーク遅延、周期的動作といったリアルタイム機能は、言語でモデル化することができる。
本稿では,FTTS (Floating-Time Transition System) とTTS (Common Timed Transition System) の両方を,そのようなモデルのセマンティクスやモデルチェックの基礎として用いる方法について説明する。
イベントベースのプロパティに関心がある場合はFTTSを使用し、状態空間の削減に役立ちます。
ある時点で変数の値に基づいてプロパティをチェックするには、TSセマンティクスを使用します。
モデルチェックツールセットは、スケジューリング可能性分析、デッドロックとキューオーバーフローチェック、アサーションベースのTimed Rebecaモデルの検証をサポートする。
TTSに基づくTCTLモデルチェックも可能だが、ツールには組み込まれていない。
関連論文リスト
- Remote Timing Attacks on Efficient Language Model Inference [63.79839291641793]
タイミング差を利用してタイミングアタックをマウントできることが示される。
90%以上の精度でユーザの会話の話題を学習することができるかを示す。
相手はブースティング攻撃を利用して、オープンソースのシステム用のメッセージに置かれたPIIを回復することができる。
論文 参考訳（メタデータ） (2024-10-22T16:51:36Z) - Complex Event Recognition with Symbolic Register Transducers: Extended Technical Report [51.86861492527722]
本稿では,オートマトンに基づく複合イベント認識システムを提案する。
本システムは,記号とレジスタオートマトンを組み合わせたオートマトンモデルに基づいている。
我々は、イベントストリーム上のパターンを検出するために、SRTをCERでどのように使用できるかを示す。
論文 参考訳（メタデータ） (2024-07-03T07:59:13Z) - Disentangling Spatial and Temporal Learning for Efficient Image-to-Video
Transfer Learning [59.26623999209235]
ビデオの空間的側面と時間的側面の学習を両立させるDiSTを提案する。
DiSTの非絡み合い学習は、大量の事前学習パラメータのバックプロパゲーションを避けるため、非常に効率的である。
5つのベンチマークの大規模な実験は、DiSTが既存の最先端メソッドよりも優れたパフォーマンスを提供することを示す。
論文 参考訳（メタデータ） (2023-09-14T17:58:33Z) - Efficiently Trained Low-Resource Mongolian Text-to-Speech System Based
On FullConv-TTS [0.0]
本稿では,RNN成分(繰り返し単位)を用いない深層畳み込みニューラルネットワークに基づく音声合成システムを提案する。
同時に、時間ワープ、周波数マスク、時間マスクといった一連のデータ拡張手法により、モデルの汎用性とロバスト性を向上する。
最後に, CNN コンポーネントのみを用いた TTS モデルは,Tacotron などの古典的 TTS モデルと比較してトレーニング時間を短縮できることを示した。
論文 参考訳（メタデータ） (2022-10-24T14:18:43Z) - A non-sequential hierarchy of message-passing models [0.0]
本稿では,大規模モデルと局所モデルの両方を含む通信モデルの統一階層について述べる。
私たちが考慮しているすべての通信モデルは、モナディック二階述語論理において公理化することができる。
論文 参考訳（メタデータ） (2022-10-24T09:31:25Z) - Neuro-symbolic Models for Interpretable Time Series Classification using
Temporal Logic Description [6.38434293310427]
解釈可能な機械学習モデルは、データのパターンを発見し、ドメインの専門家に理解しやすい洞察を与えるのに役立つ。
本稿では、信号時間論理(STL)とニューラルネットワーク(NN)を活用してTSCタスクを実現するニューロシンボリック時系列分類(NSTSC)を提案する。
論文 参考訳（メタデータ） (2022-09-15T20:50:20Z) - Topic Detection and Tracking with Time-Aware Document Embeddings [23.348627263872842]
我々は、時間的・テキスト的な情報をイベント検出のためのニュース文書の1つの表現に融合するニューラルネットワークを設計する。
振り返り設定では、クラスタリングアルゴリズムをタイムアウェアな埋め込みに適用し、News2013データセットのベースラインよりも大幅に改善したことを示す。
オンラインストリーミング設定では、既存の最先端のTDTパイプラインにドキュメントエンコーダを追加し、パフォーマンス全体のメリットを実証します。
論文 参考訳（メタデータ） (2021-12-12T06:25:15Z) - ESPnet2-TTS: Extending the Edge of TTS Research [62.92178873052468]
ESPnet2-TTSは、E2E-TTS(E2E-TTS)ツールキットである。
新機能としては、オンザフライフレキシブルプリプロセッシング、ニューラルボコーダとのジョイントトレーニング、フルバンドE2Eテキスト・トゥ・ウェーブフォームモデリングのような拡張を備えた最先端のTSモデルなどがある。
論文 参考訳（メタデータ） (2021-10-15T03:27:45Z) - End-to-End Text-to-Speech using Latent Duration based on VQ-VAE [48.151894340550385]
テキスト音声合成(TTS)におけるロバストかつ効率的なアライメントの実現の鍵となる明示的持続時間モデリング
本稿では,時間長をTSの離散潜在変数として組み込んだ明示的持続時間モデルを用いた新しいTSフレームワークを提案する。
論文 参考訳（メタデータ） (2020-10-19T15:34:49Z) - TIME: Text and Image Mutual-Translation Adversarial Networks [55.1298552773457]
テキストと画像相互変換対応ネットワーク(TIME)を提案する。
TIMEは、T2IジェネレータGと画像キャプション識別器Dをジェネレータネットワークフレームワークで学習する。
実験では、TIMEはCUBおよびMS-COCOデータセット上での最先端(SOTA)性能を達成する。
論文 参考訳（メタデータ） (2020-05-27T06:40:12Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。