論文の概要: 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プログラムの物理衝突検証のための分離論理
- 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軸テーブルテーブルテーブル構成)にスケールする。
従来の幾何学シミュレーションの補完として機能することにより、このアプローチは必要となる反復的なテストサイクルの数を減らし、自律的、非衝突的な製造の基礎を提供する。
関連論文リスト
- Semantic Drift and the Stability of Operator Control in Reasoning-Class Decision Support Systems [0.0]
ハイブリッドヒューマンマシン意思決定支援システムにおけるオペレータ制御の安定性確保の問題について検討する。
深い論理的推論の大規模言語モデルにおける意味的文脈ドリフトの潜在現象を検証し、述べる。
エンジニアリングレコメンデーションは動的リレーショナル仲裁ループを実装するために定式化されている。
論文 参考訳（メタデータ） (2026-07-08T16:54:30Z) - The Art of Interrogation: Consistency Amplifies Factuality in Spatial Reasoning [65.67266333751569]
現在のLRM(Large Reasoning Models)は、空間推論タスクにおいて顕著な汎用性を示すが、性能は著しく劣る。
本研究では,内的推論プロセスを対象とした自己指導型強化学習フレームワークを提案する。
このラベルのない整合性トレーニングは,地道的な監督によって訓練されたモデルの精度にアプローチし,多様なタスクやデータ領域にまたがる同様の一般化を実現することを示す。
論文 参考訳（メタデータ） (2026-06-10T10:50:06Z) - A Reproducible and Physically Feasible Dynamic Parameter Identification Framework for a Low-Cost Robot Arm [0.0]
本稿では,スマートアクチュエータによって駆動される低コストロボットアームのための動的パラメータ識別フレームワークを提案する。
慣性生成物は近似リンク対称性に従って除去され、剛体モデルが65から39となる。
提案したパイプラインは,プリプロセッシング,逆ダイナミックス・レグレッショナリ最小二乗(OLS),条件付き半有限プログラミング(SDP)プロジェクションと閉ループ入力誤差(CLIE)の補正を組み合わせたものである。
論文 参考訳（メタデータ） (2026-05-15T13:36:03Z) - Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic [0.0]
本稿では,GLLM法の神経生成能力を分離論理証明器による形式的検証と統合することを目的とした,G符号生成のためのニューラルシンボリックフレームワークを提案する。
最終的にこの研究は、人間の監督の必要性を減らし、より安全で確実な自動製造を実現する自己修正システムを開発することを目指している。
論文 参考訳（メタデータ） (2026-05-11T13:38:51Z) - Real-Time Projected Adaptive Control for Closed-Chain Co-Manipulative Continuum Robots [0.764671395172401]
協調操作型連続ロボット(CCR)では、複数の連続アームが共通の柔軟な物体をつかむことで協調する。
現実的なタスクでは、フレキシブルオブジェクトの物理パラメータはしばしば未知であり、操作によって異なる。
本稿では,動的レベルで定式化されたCCRの適応制御フレームワークを提案する。
論文 参考訳（メタデータ） (2026-04-05T22:03:23Z) - 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) - AutoLayout: Closed-Loop Layout Synthesis via Slow-Fast Collaborative Reasoning [102.71841660031065]
Autoは、クローズドループの自己検証プロセスをデュアルシステムフレームワークに統合する、完全に自動化された方法である。
Autoの有効性は8つの異なるシナリオで検証され、SOTA法よりも10.1%改善された。
論文 参考訳（メタデータ） (2025-07-06T08:35:22Z) - Information Science Principles of Machine Learning: A Causal Chain Meta-Framework Based on Formalized Information Mapping [7.299890614172539]
本研究は、機械学習における重要な課題、すなわち、統一的な形式的理論的枠組みの欠如と、モデル解釈可能性と倫理的安全性に関する基礎理論の欠如に対処する。
まず、一般的な機械学習段階における存在論的状態とキャリアマッピングを明確に定義し、形式的な情報モデルを構築する。
学習可能な述語と処理可能な述語を導入し、学習と処理機能を導入することにより、機械学習プロセスを管理する因果連鎖論理と制約法を解析する。
論文 参考訳（メタデータ） (2025-05-19T14:39:41Z) - Object-Centric Conformance Alignments with Synchronization (Extended Version) [57.76661079749309]
対象中心のペトリネットが一対多の関係を捉える能力と,その同一性に基づいたオブジェクトの比較と同期を行う識別子を持つペトリネットの能力を組み合わせた,新たな形式主義を提案する。
我々は、満足度変調理論(SMT)の符号化に基づく、そのようなネットに対する適合性チェック手法を提案する。
論文 参考訳（メタデータ） (2023-12-13T21:53:32Z) - 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) - Risk-Averse MPC via Visual-Inertial Input and Recurrent Networks for
Online Collision Avoidance [95.86944752753564]
本稿では,モデル予測制御(MPC)の定式化を拡張したオンライン経路計画アーキテクチャを提案する。
我々のアルゴリズムは、状態推定の共分散を推論するリカレントニューラルネットワーク(RNN)とオブジェクト検出パイプラインを組み合わせる。
本手法のロバスト性は, 複雑な四足歩行ロボットの力学で検証され, ほとんどのロボットプラットフォームに適用可能である。
論文 参考訳（メタデータ） (2020-07-28T07:34:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。