Anti-chain based algorithms for timed/probabilistic refinement checking  

作　　者：Ting WANG Tieming CHEN Yang LIU Ye WANG 

机构地区：[1]College of Computer Science and Technology, Zhejiang University of Technology [2]School of Computer Engineering, Nanyang Technological University [3]School of Computer and Information Engineering, Zhejiang Gongshang University

出　　处：《Science China(Information Sciences)》2018年第5期182-198,共17页中国科学（信息科学）（英文版）

基　　金：supported by National Natural Science Foundation of China (Grant Nos. 61602412, 61103044, U1509214, 61402406);Natural Science Foundation of Zhejiang Province of China (Grant No. LY16F020035)

摘　　要：Refinement checking answers the question on whether an implementation model is a refinement of a specification model, which is of great value for system verification. Some refinement relationships, e.g., trace refinement and failures/divergence refinement, have been recognized for different verification purposes. In general, refinement checking algorithms often rely on subset construction, which incurs in the state space explosion problem. Recently the anti-chain based approach has been suggested for trace refinement check- ing, and the results show a significant improvement. In this paper, we investigate the problems of applying the anti-chain approach to timed refinement checking （a timed implementation vs. a timed or untimed specification） and probabilistic refinement checking （a probabilistic implementation vs. a non-probabilistic specification）, and show that the state space can be reduced considerably by employing the anti-chain ap- proach. All the algorithms have been integrated into the model checking tool PAT, and the experiments have been conducted to show the efficiency of the application of anti-chains.Refinement checking answers the question on whether an implementation model is a refinement of a specification model, which is of great value for system verification. Some refinement relationships, e.g., trace refinement and failures/divergence refinement, have been recognized for different verification purposes. In general, refinement checking algorithms often rely on subset construction, which incurs in the state space explosion problem. Recently the anti-chain based approach has been suggested for trace refinement check- ing, and the results show a significant improvement. In this paper, we investigate the problems of applying the anti-chain approach to timed refinement checking （a timed implementation vs. a timed or untimed specification） and probabilistic refinement checking （a probabilistic implementation vs. a non-probabilistic specification）, and show that the state space can be reduced considerably by employing the anti-chain ap- proach. All the algorithms have been integrated into the model checking tool PAT, and the experiments have been conducted to show the efficiency of the application of anti-chains.

关 键 词：model checking REFINEMENT anti-chain timed automata markov decision process 

分 类 号：O212[理学—概率论与数理统计]