論文の概要: 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（参考訳）: サイバー物理系の決定可能な検証のための同期信号時間論理
• 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ノードのヒト心臓モデルと他のケーススタディのアプローチを実証する。

関連論文リスト

• Fast Constraint Extraction for Corrective Control under STL Specifications via Logical Dependency Tracking [13.336304771873214]
  鍵となる困難は、特にネスト式において、不確実なコンポーネントが実際に世界の満足度に影響を与えるかを特定することである。 本稿では,STL構造を通じて不確実性を伝播し,到達可能な集合の満足度に対する因果的寄与を捉える論理的依存性追跡フレームワークを提案する。
  論文  参考訳（メタデータ） (2026-09-08T20:44:28Z)
• Correct-by-Construction Behavior Tree Synthesis from Signal Temporal Logic Specifications with Application to Robotic Missions [5.524204636266904]
  動作木(BT)は、ロボット工学における複雑なタスク実行に広く採用されている。 この文字は、Signal Temporal Logic (STL)仕様から正しい構成BTを合成する。
  論文  参考訳（メタデータ） (2026-07-21T05:43:19Z)
• pdSTL: Probabilistic Differentiable Signal Temporal Logic for Stochastic Systems [0.0]
  pdSTL (probabilistic differentiable Signal Temporal Logic) は,確率的意味論を信頼軌道に対する可微分ロバスト性で統一するフレームワークである。 以上の結果から,pdSTLの効率性は,実世界の不確実性の下での安全マージンを維持する上で,決定論的微分可能なSTLよりも優れていた。
  論文  参考訳（メタデータ） (2026-06-17T20:01:56Z)
• Systematic Integration of Digital Twins and Constrained LLMs for Interpretable Cyber-Physical Anomaly Detection [0.0]
  産業制御システム(ICS)を標的としたサイバー攻撃は、ますます洗練され、識別が困難になっている。 このような攻撃を検知するには、低レベルの振る舞いキューと高レベルのセマンティック解釈を統合する必要がある。 本稿では,Digital Twin(DT)によるハイブリッド検出手法を提案する。
  論文  参考訳（メタデータ） (2026-04-04T16:38:12Z)
• Conformalized Signal Temporal Logic Inference under Covariate Shift [13.843989967082031]
  信号時間論理(STL)推論は力学系における時間的挙動の解釈可能な論理規則を学習する。 提案フレームワークは,STLの公式の解釈可能性を維持しつつ,デプロイ時のシンボル学習の信頼性を大幅に向上させる。
  論文  参考訳（メタデータ） (2026-03-28T00:38:01Z)
• 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)
• Probabilities Are Not Enough: Formal Controller Synthesis for Stochastic Dynamical Models with Epistemic Uncertainty [68.00748155945047]
  複雑な力学系のモデルにおける不確実性を捉えることは、安全なコントローラの設計に不可欠である。 いくつかのアプローチでは、安全と到達可能性に関する時間的仕様を満たすポリシーを形式的な抽象化を用いて合成する。 我々の貢献は、ノイズ、不確実なパラメータ、外乱を含む連続状態モデルに対する新しい抽象的制御法である。
  論文  参考訳（メタデータ） (2022-10-12T07:57:03Z)
• SMT-Based Safety Verification of Data-Aware Processes under Ontologies (Extended Version) [71.12474112166767]
  我々は、このスペクトルで最も調査されたモデルの1つ、すなわち単純なアーティファクトシステム(SAS)の変種を紹介する。 このDLは適切なモデル理論特性を享受し、後方到達性を適用可能なSASを定義することができ、対応する安全問題のPSPACEにおける決定可能性をもたらす。
  論文  参考訳（メタデータ） (2021-08-27T15:04:11Z)
• Stability and Identification of Random Asynchronous Linear Time-Invariant Systems [81.02274958043883]
  線形力学系の安定性に対するランダム化と非同期化の付加的な利点を示す。 未知のランダム化LTIシステムに対して,基礎となる力学を復元するための系統的同定手法を提案する。
  論文  参考訳（メタデータ） (2020-12-08T02:00:04Z)
• SMT-based Safety Verification of Parameterised Multi-Agent Systems [78.04236259129524]
  パラメータ化マルチエージェントシステム(MAS)の検証について検討する。 特に、与えられた状態公式として特徴づけられる不要な状態が、所定のMASで到達可能かどうかについて検討する。
  論文  参考訳（メタデータ） (2020-08-11T15:24:05Z)
• 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)

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

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