| 基于FSA的模型检测算法研究 |
| |
| 引用本文： | 王扣武,张珺铭,龙士工,董方. 基于FSA的模型检测算法研究[J]. 贵州大学学报(自然科学版), 2012, 29(5): 58-62 |
| |
| 作者姓名： | 王扣武 张珺铭 龙士工 董方 |
| |
| 作者单位： | 1. 贵州大学 计算机科学与信息学院,贵州 贵阳,550025
2. 贵州大学 理学院,贵州 贵阳,550025 |
| |
| 基金项目： | 基金项目：国家自然科学基金（No.61163001） |
| |
| 摘 要： | 自动机就是描述系统行为的模型,通过它可以检测出系统实际工作时发生的状态,经过反复测试,诊断,以达到理想的模型。在基于自动机的模型检测中,前提是需要把非确定性FSA转化为确定性FSA,本文给出了非确定性自动机转换为确定性自动机的算法,最后分析该算法。
|
| 关 键 词： | 有限状态自动机 语言 字 模型检测 |
Algorithm Research Based on FSA Model Checking |
| |
| WANG Kou-wu , ZHANG Jun-ming , LONG Shi-gong , DONG Fang. Algorithm Research Based on FSA Model Checking[J]. Journal of Guizhou University(Natural Science), 2012, 29(5): 58-62 |
| |
| Authors: | WANG Kou-wu ZHANG Jun-ming LONG Shi-gong DONG Fang |
| |
| Affiliation: | 1. College of Computer Science and Information, Guizhou University, Guiyang 550025, China; 2. Science College, Guizhou University, Guiyang 550025, China) |
| |
| Abstract: | Automaton is a model that can describe the behaviors of a system in scientific research. The working states can be checked when it is used in practice. Only lots of times of tests and diagnoses should it be taken into practice. The premise is changing the non-deterministic FSA into the deterministic FSA in model checking which is based on automaton. This paper introduces finite-state automaton, gives out the algorithm of how a non-deter- ministic automaton shift into the corresponding deterministic automaton. At the end of this paper, this algorithm is analyzed. |
| |
| Keywords: | finite-state automata language word model checking |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
