摘要：According to the demand of credible property verification for complex information system, this paper presents a kind of until formula conditional probability property verification and analysis method acting on discrete probability model. A new more expressive probabilistic computation tree logic used to describe until formula conditional probability property of system model. We express until path formula as automaton and give the formal representation of until formula intersection operation automaton. The method of calculate the corresponding accept state reachable probability be described based on product model which realizes the simultaneous evolution of the model and c operation automaton. The example result verifies the feasibility and validity of the method.
