Verifying Automata Specification of Distributed Probabilistic Real-Time Systems

摘要

In this paper, a qualitative model checking algorithm for verification of distributed prob- abilistic real-timed systems(DPRS) is presented. The model of DPRS, called real-time proba- bilistic process model(RPPM), is over continuous time domain. The properties of DPRS are described by using deterministic timed automata(DTA). The key part in the algorithm is to map continuous time to finite time intervals with flag variables. Compared with the existing algorithms, this algorithm uses more general delay time equivalence classes instead of the unit delay time equivalence classes restricted by event sequence, and avoids generating the equiva- lence classes of states only due to the passage of time. the result shows that this algorithm is cheaper.