正则表达式与有穷自动机等价性在Isabelle/HOL中的形式化  

Mechanizing equivalence of regular expression and FA in Isabelle/HOL

作　　者：吴春寒[1] 张兴元[1] 贺汛[1] 

机构地区：[1]解放军理工大学指挥自动化学院,江苏南京210007

出　　处：《解放军理工大学学报（自然科学版）》2010年第4期403-407,共5页Journal of PLA University of Science and Technology(Natural Science Edition)

基　　金：国家863计划资助项目(2008AA01A309)

摘　　要：针对正则表达式和有穷自动机,在机器辅助定理证明系统Isabelle/HOL中进行了形式化描述。通过对语言、正则表达式、确定和不确定有穷自动机在Isabelle/HOL中建立模型,定义了它们之间的相互转换函数并证明了这些函数的正确性,从而验证了正则表达式和有穷自动机在描述能力上的等价性,即:在同一有限字母表下,对任意正则表达式,都存在一个有穷自动机,使得二者描述的语言相同;反之亦然。通过分析与证明,表明采用机器辅助定理证明系统,对计算理论传统核心领域之一的自动机理论进行分析和证明是可行的。Aiming at regular expression and FA,formal description was given in Isabelle/HOL,a proof assistant system for high-order logic.By building logic models for language,regular expression,deterministic finite automata,and nondeterministic finite automata in Isabelle/HOL,the functions for their mutual translation were defined and their validity was proved.The equivalence theorem of regular expression and FA＇s language descriptive power was verified.The equivalence theorem was that under a certain finite alphabet,for all the regular expressions,there must be a finite automata whose representing language equaled to the language represented by the regular expression,and vice versa.Analysis and verification show that in machine-assisted verification system,the stringent analysis and the proof of automata theory,which is one of the core fields of computation theory,is feasible.

关 键 词：正则表达式 有穷自动机 形式化验证 Isabelle/HOL 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]