文章基本信息

标题：Verification Method of Conditional Probability Based on Automaton
本地全文：下载
作者：Ji, Mingyu ; Wu, Di ; Chen, Zhiyuan 等
期刊名称：Journal of Networks
印刷版ISSN：1796-2056
出版年度：2013
卷号：8
期号：6
页码：1329-1335
DOI：10.4304/jnw.8.6.1329-1335
语种：English
出版社：Academy Publisher
摘要：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.
关键词：model checking;until formula;conditional probability;intersection operation;automaton