%0 Journal Article
%T Verifying automata specification of distributed probabilistic real-time systems<br>Verifying Automata Specification of Distributed Probabilistic Real-Time Systems
%A Luo Tiegeng
%A Chen Huowang
%A Wang Bingshan
%A Wang Ji
%A Gong Zhenghu
%A Qi Zhichang
%A <br>Luo Tiegeng
%A Chen Huowang
%A Wang Bingshan
%A Wang Ji
%A Gong Zhenghu
%A Qi Zhichang
%J 计算机科学技术学报
%D 1998
%I 
%X 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.
%K DPRS
%K GSMP
%K automatic verification
%K model checking
%K timed automata<br>计算机网络
%K 自动化检验
%K 实时系统
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=F57FEF5FAEE544283F43708D560ABF1B&aid=0BD724EC006C854FCE8D01D8E83ADAD7&yid=8CAA3A429E3EA654&vid=FC0714F8D2EB605D&iid=B31275AF3241DB2D&sid=4964C30D71DF45FF&eid=6341CCF6B158C5F9&journal_id=1000-9000&journal_name=计算机科学技术学报&referenced_num=0&reference_num=7