抽象连续时间系统可达集的下近似

我们考虑证明给定状态集（“目标集”）中的每个点确实能被某个给定的非确定性连续时间动力系统从某个初始状态到达的问题。我们针对可具体化为各类连续和混合动力系统的抽象连续时间模型考虑此问题。本文提出的解决该问题的方法基于寻找目标集的一个合适超集 S，其性质为：系统每条完全位于 S 中的部分轨迹要么定义于初始时刻，要么可在时间上局部向后延伸，要么可被局部修改从而使得所得轨迹可在时间上局部向后延伸。这一问题的重构具有相对简单的逻辑表达，并便于应用各种局部存在性定理和局部动力学分析方法来证明可达性，从而使其适用于在 Mizar、Isabelle 等证明辅助工具中推理连续与混合动力系统的行为。