基于概率时间自动机的模型检测反例表示研究  

Counterexample representation for probabilistic timed automata model checking

作　　者：王晶[1] 张广泉[1,2] 

机构地区：[1]苏州大学计算机科学与技术学院,江苏苏州215006 [2]中国科学院计算机科学国家重点实验室,北京100080

出　　处：《苏州大学学报（自然科学版）》2011年第2期36-42,47,共8页Journal of Soochow University(Natural Science Edition)

基　　金：中国科学院计算机科学国家重点实验室开放课题(SYSKF0908);江苏省高校自然科学研究项目(08KJB520010)

摘　　要：近年来,概率系统在实际中应用越来越广泛,其中模型检测基于概率系统的反例生成问题,已引起人们的广泛关注,现有的工作主要围绕模型检测Markov链反例生成展开.概率时间自动机(PTA)是Markov链的不确定性和系统时钟的扩展,针对模型检测PTA的反例表示问题,首先将PTA的语义表示为Markov决策过程(MDP),通过策略解决MDP不确定性,将MDP转换为离散时间Markov链(DTMC);然后将DTMC转换为带权有向图,则PTA中最小反例问题转化为带权有向图中最短路径问题;最后采用正则表达式表示求得的反例.Recently,probabilistic systems have been widely used,people have drawn attention to counterexample generation for probabilistic system model checking.Current works are mainly focusing on the counterexample generation for Markov chains.Probabilistic timed automata（PTA） is the extension of Markov chain with non-determinism and system clocks.This paper focuses on counterexample representation while model checking PTA.Firstly,the semantic of PTA can be regarded as Markov decision process（MDP）;secondly,we use adversary to convert MDP into discrete-time Markov chain（DTMC）;thirdly,we convert DTMC into weighted graph,counterexample generation for PTA can be converted into shortest path problem for weighted digraph;finally,we use regular expressions to represent the counterexample.

关 键 词：反例 概率时间自动机 离散时间Markov链 MARKOV决策过程 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]