参数化系统二维抽象的理论基础

模型之间的等价关系和抽象模型的性质保持是保证验证正确的必要条件，参数化系统二维抽象从构成系统状态空间的二维方向分别进行抽象，证明了此抽象方法的正确性和合理性，即TDA模型与原始模型存在模拟关系，而且在TDA模型中成立的只对单个变量进行全称量化的单索引ACTL*公式，在任意规模的原始模型中也成立，为简化参数化系统验证提供了理论依据。

Two-dimension Abstraction Theory for Parameterized System

In order to preserve interesting properties of a system under consideration during verification, it is necessary to establish an equivalent relation between models. Two-dimension abstraction for parameterized system,where the size of the state transition graph for individual process is decreased independently at first, and the whole system composed of reduced processes is then abstracted based on the design principle of parameterized systems, thus avoiding the construction of the complete state space that might be too big to fit into memory. The paper gave the correctness and soundness proofs of two-dimension abstraction. It was shown that simulation relation exists between TDA model and concrete model, and TDA model is weak preserved with respect to ACTL* formula. Importantly, a singlcindcxed ACTL* formina satisfied by TDA model, is also satisfied by concrete models with arbitrary replicated(and a constant number of non-replicated) processes. This work lays the theoretical basis for simplifying parameterized system verification.