Abstract: 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.

Key words: Parameterized system verification, Two-dimension abstraction, Simulation, Property preservation