論文の概要: Separation Logic for Verifying Physical Collisions of CNC Programs

• arxiv url: http://arxiv.org/abs/2605.10437v2
• Date: Wed, 20 May 2026 01:56:18 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-21 14:55:43.997026
• Title: Separation Logic for Verifying Physical Collisions of CNC Programs
• Title（参考訳）: CNCプログラムの物理衝突検証のための分離論理
• Authors: Yeonseok Lee,
• Abstract要約: コンピュータ数値制御(CNC)の安全性検証は、伝統的に反復的なテスト要求の変更に依存してきた。 本稿では,物理シミュレーションを空間的,管理された論理力学モデルとして概念化する形式的検証フレームワークを概念化する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Safety verification in Computer Numerical Control (CNC) machining has traditionally relied on simulation-based methods that require repetitive tests when requirements change. This paper introduces a formal verification framework that conceptualizes the physical CNC workspace as a Spatial Heap, treating physical occupancy as a managed logical resource. Central to our approach is a Parser-Prover Handshake that decouples machine kinematics from formal logic. By mapping tool trajectories and safety buffers into a discrete spatial model prior to evaluation, the framework enables the use of Separation Logic (SL) to verify safety via formal triples. Within this model, physical collisions are redefined as logical Spatial Data Races, detected through the failure of the separating conjunction to establish disjointness. Furthermore, we extend the methodology to collaborative environments using Concurrent Separation Logic (CSL), where physical hand-offs are verified as formal ownership transfers. Additionally, the framework scales to multi-axis kinematics (e.g., 5-axis Table-Table configurations) by treating the workpiece as a dynamically mutable spatial resource. By serving as a complement to traditional geometric simulation, this approach reduces the number of required iterative test cycles, offering a foundation for autonomous, less-collision manufacturing.
• Abstract（参考訳）: コンピュータ数値制御(CNC)加工における安全性検証は、要求が変わったときに繰り返しテストを必要とするシミュレーションベースの手法に依存してきた。 本稿では、物理CNCワークスペースを空間ヒープとして概念化し、物理的占有力を管理論理資源として扱う形式的検証フレームワークを提案する。 私たちのアプローチの中心は、機械キネマティクスを形式論理から分離するParser-Prover Handshakeです。 評価に先立ってツールトラジェクトリと安全バッファを離散空間モデルにマッピングすることにより、このフレームワークは分離論理(SL)を使用して、形式的な三重項による安全性の検証を可能にする。 このモデルでは、物理的衝突は論理的空間データレースとして再定義され、分離結合の失敗によって検出され、不整合を確立する。 さらに,コンカレント分離論理(CSL)を用いて,物理的ハンドオフを正式なオーナシップ転送として検証し,協調環境に拡張する。 さらに、ワークを動的に変更可能な空間資源として扱うことにより、多軸キネマティクス(例えば、5軸テーブルテーブルテーブル構成)にスケールする。 従来の幾何学シミュレーションの補完として機能することにより、このアプローチは必要となる反復的なテストサイクルの数を減らし、自律的、非衝突的な製造の基礎を提供する。

関連論文リスト

• Rethinking Scientific Modeling: Toward Physically Consistent and Simulation-Executable Programmatic Generation [8.067859101380389]
  非実行可能または物理的に一貫性のない出力は、厳密な工学的制約の下では依然として一般的である。 物理に一貫性のある自動建築モデリングのための枠組みを提案する。 CivilInstructは、構造工学の知識と制約推論を形式化するドメイン固有のデータセットとして導入された。 MBEvalは、実行可能性と構造的ダイナミクスの一貫性を評価する検証駆動ベンチマークとして提示される。
  論文  参考訳（メタデータ） (2026-02-06T06:57:04Z)
• Physics-informed sensor coverage through structure preserving machine learning [8.009940044669191]
  適応的ソースローカライゼーションのための機械学習フレームワークを提案する。 エージェントは、リアルタイムな軌道計画とデータ同化のために結合された流体力学輸送システムの構造保存デジタルツインを使用する。
  論文  参考訳（メタデータ） (2025-09-12T15:54:13Z)
• Information Science Principles of Machine Learning: A Causal Chain Meta-Framework Based on Formalized Information Mapping [7.299890614172539]
  本研究は、機械学習における重要な課題、すなわち、統一的な形式的理論的枠組みの欠如と、モデル解釈可能性と倫理的安全性に関する基礎理論の欠如に対処する。 まず、一般的な機械学習段階における存在論的状態とキャリアマッピングを明確に定義し、形式的な情報モデルを構築する。 学習可能な述語と処理可能な述語を導入し、学習と処理機能を導入することにより、機械学習プロセスを管理する因果連鎖論理と制約法を解析する。
  論文  参考訳（メタデータ） (2025-05-19T14:39:41Z)
• Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics [64.72260320446158]
  マルコフジャンプ線形系に対する制御器の合成法を提案する。 本手法は,MJLSの離散(モードジャンピング)と連続(確率線形)の両方の挙動を捉える有限状態抽象化に基づいている。 本手法を複数の現実的なベンチマーク問題,特に温度制御と航空機の配送問題に適用する。
  論文  参考訳（メタデータ） (2022-12-01T17:36:30Z)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  我々はCoCoMoT(Computing Conformance Modulo Theories)フレームワークを紹介する。 まず、純粋な制御フロー設定で研究したSATベースのエンコーディングを、データ認識ケースに持ち上げる方法を示す。 次に,プロパティ保存型クラスタリングの概念に基づく新しい前処理手法を提案する。
  論文  参考訳（メタデータ） (2021-03-18T20:22:50Z)

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

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