摘要
自动机就是描述系统行为的模型,通过它可以检测出系统实际工作时发生的状态,经过反复测试,诊断,以达到理想的模型。在基于自动机的模型检测中,前提是需要把非确定性FSA转化为确定性FSA,本文给出了非确定性自动机转换为确定性自动机的算法,最后分析该算法。
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.
出处
《贵州大学学报（自然科学版）》
2012年第5期58-62,共5页
Journal of Guizhou University:Natural Sciences
基金
国家自然科学基金(No.61163001)
关键词
有限状态自动机
语言
字
模型检测
finite-state automata
language
word
model checking
