論文の概要: Synchronous Signal Temporal Logic for Decidable Verification of Cyber-Physical Systems

• arxiv url: http://arxiv.org/abs/2603.25531v1
• Date: Thu, 26 Mar 2026 15:06:17 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-27 20:52:48.350172
• Title: Synchronous Signal Temporal Logic for Decidable Verification of Cyber-Physical Systems
• Title（参考訳）: サイバー物理系の決定可能な検証のための同期信号時間論理
• Authors: Partha Roop, Sobhan Chatterjee, Avinash Malik, Nathan Allen, Logan Kenwright,
• Abstract要約: 多くのサイバー物理システム(CPS)は、正しい実行、信頼性、信頼性が不可欠である安全クリティカルな環境で機能する。 Signal Temporal Logic (STL)は、安全クリティカルなCPSをチェックするための正式なフレームワークを提供する。 静的安全性と生存性を検証するSTLの断片であるSynchronous Signal Temporal Logic (SSTL)を提案する。
• 参考スコア（独自算出の注目度）: 1.0895848625126727
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Many Cyber Physical System (CPS) work in a safety-critical environment, where correct execution, reliability and trustworthiness are essential. Signal Temporal Logic (STL) provides a formal framework for checking safety-critical CPS. However, static verification of STL is undecidable in general, except when we want to verify using run-time-based methods, which have limitations. We propose Synchronous Signal Temporal Logic (SSTL), a decidable fragment of STL, which admits static safety and liveness property verification. In SSTL, we assume that a signal is sampled at fixed discrete steps, called ticks, and then propose a hypothesis, called the Signal Invariance Hypothesis (SIH), which is inspired by a similar hypothesis for synchronous programs. We define the syntax and semantics of SSTL and show that SIH is a necessary and sufficient condition for equivalence between an STL formula and its SSTL counterpart. By translating SSTL to LTL_P (LTL defined over predicates), we enable decidable model checking using the SPIN model checker. We demonstrate the approach on a 33-node human heart model and other case studies.
• Abstract（参考訳）: 多くのサイバー物理システム(CPS)は、正しい実行、信頼性、信頼性が不可欠である安全クリティカルな環境で機能する。 Signal Temporal Logic (STL)は、安全クリティカルなCPSをチェックするための正式なフレームワークを提供する。 しかし、STLの静的な検証は一般的には決定不可能であり、制限のある実行時ベースのメソッドを使用して検証したい場合を除いては、決定できない。 静的安全性と生存性を検証するSTLの断片であるSynchronous Signal Temporal Logic (SSTL)を提案する。 SSTLでは、信号が固定された離散的なステップでサンプリングされたと仮定し、同期プログラムの同様の仮説にインスパイアされたシグナル不変性仮説(SIH)を提案する。 SSTL の構文と意味を定義し,SIH が STL 式と SSTL 式との等価性の必要十分条件であることを示す。 SSTL を LTL_P (LTL defined over predicates) に変換することにより,SPIN モデルチェッカーを用いて決定可能なモデルチェックを可能にする。 我々は33ノードのヒト心臓モデルと他のケーススタディのアプローチを実証する。

関連論文リスト

• Feasibility Restoration under Conflicting STL Specifications with Pareto-Optimal Refinement [18.383508411056944]
  Signal Temporal Logic (STL) は、ロボット工学における表現的要求を規定する表現的言語である。 STL仕様は、安全規則、交通規制、タスクと目的を一緒に満たせない現実世界のアプリケーションでは矛盾する可能性がある。 本稿では,最小限の緩和による実現可能性の回復を図り,それを価値認識多目的最適化問題として定式化し,実現可能な解を洗練する,統合された2段階フレームワークを提案する。
  論文  参考訳（メタデータ） (2026-03-06T23:41:01Z)
• STLCG++: A Masking Approach for Differentiable Signal Temporal Logic Specification [9.039665244779185]
  STLCG++は、STL計算と時間ステップ間のバックプロパゲーションを並列化するマスキングベースのアプローチである。 また、時間間隔境界の微分を可能にするスムース化手法を導入し、勾配に基づく最適化タスクにおけるSTLの適用性を拡大する。
  論文  参考訳（メタデータ） (2025-01-08T00:06:43Z)
• Retrieval-Augmented Mining of Temporal Logic Specifications from Data [0.46040036610482665]
  この研究は、観測された振る舞いからデータ駆動的な方法でSTL要求を学習するタスクに対処する。 本稿では,ベイズ最適化(BO)と情報検索(IR)技術を組み合わせて,STL式の構造とパラメータを同時に学習する新しいフレームワークを提案する。
  論文  参考訳（メタデータ） (2024-05-23T09:29:00Z)
• Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions [59.605246463200736]
  雑音分布の明示的な表現に依存しない新しい制御器合成法を提案する。 まず、連続制御系を有限状態モデルに抽象化し、離散状態間の確率的遷移によってノイズを捕捉する。 我々は最先端の検証技術を用いてマルコフ決定プロセスの間隔を保証し、これらの保証が元の制御システムに受け継がれるコントローラを演算する。
  論文  参考訳（メタデータ） (2023-01-04T10:40:30Z)
• Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics [64.72260320446158]
  マルコフジャンプ線形系に対する制御器の合成法を提案する。 本手法は,MJLSの離散(モードジャンピング)と連続(確率線形)の両方の挙動を捉える有限状態抽象化に基づいている。 本手法を複数の現実的なベンチマーク問題,特に温度制御と航空機の配送問題に適用する。
  論文  参考訳（メタデータ） (2022-12-01T17:36:30Z)
• SMT-Based Safety Verification of Data-Aware Processes under Ontologies (Extended Version) [71.12474112166767]
  我々は、このスペクトルで最も調査されたモデルの1つ、すなわち単純なアーティファクトシステム(SAS)の変種を紹介する。 このDLは適切なモデル理論特性を享受し、後方到達性を適用可能なSASを定義することができ、対応する安全問題のPSPACEにおける決定可能性をもたらす。
  論文  参考訳（メタデータ） (2021-08-27T15:04:11Z)
• Backpropagation through Signal Temporal Logic Specifications: Infusing Logical Structure into Gradient-Based Methods [28.72161643908351]
  本稿では,STLCG(Signal Temporal Logic)公式の定量的意味を計算グラフを用いて計算する手法を提案する。 STLは、連続系とハイブリッド系の両方で生成される信号の空間的および時間的特性を指定できる、強力で表現力のある形式言語である。
  論文  参考訳（メタデータ） (2020-07-31T22:01:39Z)

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

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