AI 中文总结
针对异步多接口RAN规划的不安全中间状态问题，提出VeraRAN预执行验证框架，结合VeraSync修复与MI-POR状态修剪，有效提升规划安全性并降低状态探索开销。
AI 中文摘要
智能体RAN控制器会在独立实现的接口间整合移动性、能量与资源动作。即便每条命令均有效且目标状态安全，异步执行仍可能使网络经历不安全的中间状态。针对35B规划器的冻结研究显示，28.8%的局部有效规划仍存在异步不安全问题。我们提出VeraRAN，该工具通过为每个动作建模请求、交付、接受、应用、完成与观测环节，同时探索合理延迟与事件顺序，在执行前验证规划。当VeraRAN找到反例时，VeraSync会插入带版本的事件屏障，并重新验证修复后规划的安全性与完整性。MI-POR利用RAN生命周期与资源足迹修剪独立交错执行的情况。在声明修复域内的冻结后分层验证中，VeraSync重新验证了所有待验证规划，同时使87%的动作对保持无序；在属性分层审计中，MI-POR的表现与精确搜索相当，且在含20至40个动作的规划上减少了94.6%至95.0%的已探索状态。原生ns-O-RAN回放与独立实时E2审计表明区分这些事件的重要性：接受可能先于权威状态转换，因此依赖动作必须等待直接的APPLY证据或APPLY下游经合同支持的完成事件。
英文摘要
Agentic RAN controllers combine mobility, energy, and resource actions across independently implemented interfaces. Even when each command is valid and the target state is safe, asynchronous actuation can drive the network through unsafe intermediate states. In a frozen study of a 35B planner, 28.8% of locally valid plans remained asynchronously unsafe. We introduce VeraRAN, which checks plans before actuation by modeling request, delivery, acceptance, application, completion, and observation for each action while exploring plausible delays and event orders. When VeraRAN finds a counterexample, VeraSync inserts versioned event barriers and rechecks the repaired plan for safety and completion. MI-POR prunes independent interleavings using RAN lifecycle and resource footprints. In a post-freeze stratified confirmation within the declared repair domain, VeraSync re-certified every confirmation plan while leaving 87% of action pairs unordered. MI-POR matched exact search in a property-stratified audit and reduced explored states by 94.6-95.0% on 20-40-action plans. Native ns-O-RAN replay and an independent live E2 audit showed why distinguishing these events matters: acceptance may precede the authoritative state transition, so dependent actions must wait for direct APPLY evidence or a contract-backed completion event causally downstream of APPLY.
Comments10 pages, 4 figures, 1 table
