构建网络物理系统的保守离散抽象的实用指南
A Pragmatic Guide to Building Conservative Discrete Abstractions of Cyber-Physical Systems
浏览论文内容
中文总结 AI 辅助
本教程提出一种按构造保守的闭环动力系统离散抽象构建工作流，含四模块化步骤，经三案例研究验证其设计选择对抽象结构、运行时间及验证结果的影响。
中文摘要 AI 辅助
符号模型检查是验证网络物理系统（CPS）语义丰富的时态逻辑属性的有效方法，但它依赖于将连续状态动力学离散化为有限状态抽象。为了将验证保证从抽象模型传递到具体CPS，抽象必须保守地近似具体状态空间和行为。因此，模型构建者必须在保持这种正确性的同时平衡悲观性与可处理性。然而，他们面临几个常见陷阱，例如对状态空间的下近似、对转移的下近似、对“退化”行为的不正确剪枝以及不正确的规约提升。本教程提出了一种实用的、按构造保守的工作流，用于构建闭环动力系统的离散抽象。该工作流包含四个可互换子程序的模块化步骤：（i）状态空间划分与抽象函数设计；（ii）通过轴对齐边界框、多面体或具有PAC覆盖证书的采样构建保守转移；（iii）使用经认证的删除和反例引导的抽象细化减少伪转移和自环；（iv）使用may-must语义正确提升LTL规约。我们在三个案例研究中演示了该端到端流程，并报告这些设计选择如何影响抽象结构、运行时间和验证结果。
英文摘要
Symbolic model checking is an effective approach for verifying semantically rich temporal-logic properties of cyber-physical systems, but it hinges on discretizing continuous-state dynamics into a finite-state abstraction. To transfer verification guarantees from the abstract model to the concrete CPS, the abstraction must conservatively approximate the concrete state space and behaviors. Hence, model-builders must maintain this soundness while balancing pessimism with tractability. However, they face several common pitfalls such as under-approximating the state space, under-approximating transitions, unsound pruning of "degenerate" behaviors, and improper specification lifting. This tutorial presents a pragmatic, conservative-by-construction workflow for building discrete abstractions of closed-loop dynamical systems. The workflow consists of four modular steps with interchangeable subroutines: (i) state-space partition and abstraction-function design, (ii) conservative transition construction via axis-aligned bounding boxes, polytopes, or sampling with PAC coverage certificates, (iii) mitigation of spurious transitions and self-loops using certified erasure and counterexample-guided abstraction refinement, and (iv) sound lifting of LTL specifications using may-must semantics. We demonstrate the end-to-end pipeline on three case studies and report how these design choices affect abstraction structure, runtime, and verification outcomes.
