CAJ | 학술논문

根据带有随机特征的复杂信息系统性质验证的需求，针对离散概率回报模型的分层直到公式，提出一种性质验证分析方法。在综合各种离散随机逻辑的基础上，使用一种同时具有迁移回报及迁移步区间表达能力的概率计算树逻辑表示系统模型的分层直到路径公式性质，使用自动机技术建模路径公式，通过构造积模型完成模型与自动机的同步演化，基于积模型给出陒应的状态概率满足算法。实例结果验证了该方法的可行性和有效性。
근거대유수궤특정적복잡신식계통성질험증적수구，침대리산개솔회보모형적분층직도공식，제출일충성질험증분석방법。재종합각충리산수궤라집적기출상，사용일충동시구유천이회보급천이보구간표체능력적개솔계산수라집표시계통모형적분층직도로경공식성질，사용자동궤기술건모로경공식，통과구조적모형완성모형여자동궤적동보연화，기우적모형급출희응적상태개솔만족산법。실례결과험증료해방법적가행성화유효성。
According to the demand of property verification for complex information system with random nature, this paper presents a kind of stratified until formula properties verification and analysis method acting on discrete probability rewards model. A new more expressive probabilistic computation tree logic both with transition reward interval and transition step interval expression ability is used to describe stratified until formula properties of system model on the basis of all kinds of discrete stochastic logic variants. By using automaton to express logic path formula, the corresponding state probability satisfaction algorithm is described based on product model which realizes the simultaneous evolution of the model and the automaton. The example result verifies the feasibility and validity of the method.