| 基于概率时间自动机的模型检测反例表示研究 |
| |
| 引用本文： | 王晶,张广泉.基于概率时间自动机的模型检测反例表示研究[J].苏州大学学报(医学版),2011,27(2). |
| |
| 作者姓名： | 王晶 张广泉 |
| |
| 作者单位： | 王晶,Wang Jing(苏州大学计算机科学与技术学院,江苏苏州,215006);张广泉,Zhang Guangquan(苏州大学计算机科学与技术学院,江苏苏州215006;中国科学院计算机科学国家重点实验室,北京100080) |
| |
| 基金项目： | 中国科学院计算机科学国家重点实验室开放课题，江苏省高校自然科学研究项目 |
| |
| 摘 要： | 近年来,概率系统在实际中应用越来越广泛,其中模型检测基于概率系统的反例生成问题,已引起人们的广泛关注,现有的工作主要围绕模型检测Markov链反例生成展开.概率时间自动机(PTA)是Markov链的不确定性和系统时钟的扩展,针对模型检测PTA的反例表示问题,首先将PTA的语义表示为Markov决策过程(MDP),通过策略解决MDP不确定性,将MDP转换为离散时间Markov链(DTMC);然后将DTMC转换为带权有向图,则PTA中最小反例问题转化为带权有向图中最短路径问题;最后采用正则表达式表示求得的反例.
|
| 关 键 词： | 反例 概率时间自动机 离散时间Markov链 Markov决策过程 |
Counterexample representation for probabilistic timed automata model checking |
| |
| Wang Jing,Zhang Guangquan.Counterexample representation for probabilistic timed automata model checking[J].Journal of Suzhou University(Natural Science),2011,27(2). |
| |
| Authors: | Wang Jing Zhang Guangquan |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 万方数据 等数据库收录！ |
|
