摘要: 模型之间的等价关系和抽象模型的性质保持是保证验证正确的必要条件,参数化系统二维抽象从构成系统状态空间的二维方向分别进行抽象,证明了此抽象方法的正确性和合理性,即TDA模型与原始模型存在模拟关系,而且在TDA模型中成立的只对单个变量进行全称量化的单索引ACTL*公式,在任意规模的原始模型中也成立,为简化参数化系统验证提供了理论依据。
庞征斌,屈婉霞,郭阳,杨晓东. 参数化系统二维抽象的理论基础[J]. 计算机科学, 2011, 38(4): 295-301. https://doi.org/
PANG Zheng-bin,QU Wan-xia,GUO Yang,YANG Xiao-dong. Two-dimension Abstraction Theory for Parameterized System[J]. Computer Science, 2011, 38(4): 295-301. https://doi.org/