%0 Journal Article
%T Two-dimension Abstraction Theory for Parameterized System<br>参数化系统二维抽象的理论基础
%A PANG Zheng-bin
%A QU Wan-xia
%A GUO Yang
%A YANG Xiao-dong
%A <br>庞征斌
%A 屈婉霞
%A 郭阳
%A 杨晓东
%J 计算机科学
%D 2011
%I 
%X 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.
%K Parameterized system verification
%K Two-dimension abstraction
%K Simulation
%K Property preservation<br>参数化系统验证，二维抽象，模拟，性质保持
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=235D91A5D23645A72C829640ED3737C3&yid=9377ED8094509821&vid=16D8618C6164A3ED&iid=E158A972A605785F&sid=AF507FDD66D991DA&eid=DFEE4E8C33C95CEF&journal_id=1002-137X&journal_name=计算机科学&referenced_num=0&reference_num=7