Verifying Automata Specification ofDistributed Probabilistic Real-Time Systems  

作　　者：罗铁庚 陈火旺 王兵山 王戟 龚正虎 齐治昌 

出　　处：《Journal of Computer Science & Technology》1998年第6期588-596,共9页计算机科学技术学报（英文版）

摘　　要：In this paper, a qualitative model checking algorithm for verification of distributed probabilistic real-time systems (DPRS) is presented. The model of DPRS, called real-time probabilistic process model (RPPM), is over continuous time domain. The properties of DPRS aredescribed by using deterministic timed automata (DTA). The key part in the algorithm is tomap continuous time to finite time intervals with flag variables. Compared with the existingalgorithms, this algorithm uses more general delay time equivalence classes instead of the unitdelay time equivalence classes restricted by event sequence, and avoids generating the equivalence classes of states only due to the passage of time. The result shows that this algorithm ischeaper.In this paper, a qualitative model checking algorithm for verification of distributed probabilistic real-time systems (DPRS) is presented. The model of DPRS, called real-time probabilistic process model (RPPM), is over continuous time domain. The properties of DPRS aredescribed by using deterministic timed automata (DTA). The key part in the algorithm is tomap continuous time to finite time intervals with flag variables. Compared with the existingalgorithms, this algorithm uses more general delay time equivalence classes instead of the unitdelay time equivalence classes restricted by event sequence, and avoids generating the equivalence classes of states only due to the passage of time. The result shows that this algorithm ischeaper.

关 键 词：DPRS GSMP automatic verification model checking timed automata. 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]