The property verification methods of complex stochastic system based on directed graph

With the increasing complexity of computer hardware and software systems, how to ensure system accuracy and reliability becomes an increasingly pressing issue. The quantitative verification of multiple until formula property has important practical significance in the field of biology. In this paper, for particular probability reward model, we give the detailed analysis of properties verification methods of the multiple until formula with transition step and transition reward constraints based on the weighted directed graph. At last, the example analysis is given. The theoretical analysis and example result show that the feasibility and validity of the method.