Verifying Automata Specification of Distributed Probabilistic Real-Time Systems

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.