摘要
交替(树)自动机因其本身关于取补运算的简洁性及其与非确定型(树)自动机的等价性,成为自动机与模型检测领域研究的一个新方向.在格值交替自动机与经典交替树自动机概念的基础上,引入格值交替树自动机的概念,并研究了格值交替树自动机的代数封闭性和表达能力.首先,证明了对格值交替树自动机的转移函数取对偶运算,终止权重取补之后所得自动机与原自动机接受语言互补这一结论.其次,证明了格值交替树自动机关于交、并运算的封闭性.最后,讨论了格值交替树自动机和格值树自动机、格值非确定型自动机的表达能力;证明了格值交替树自动机与格值树自动机的等价性,并给出了二者相互转化的算法及其复杂度分析;同时,提供了用格值非确定型自动机来模拟格值交替树自动机的方法.
Because of the simplicity of taking complement operation on alternating(tree)automata and the equivalence relationship between alternating(tree)automata and nondeterministic(tree)automata,the study on alternating(tree)automata becomes a new research area of automata and model checking.Based on notions of L-valued alternating automata and alternating tree automata,the notion of L-valued alternating tree automata is introduce,and closure properties and expressive power of L-valued alternating tree automata are studied.Firstly,it is proved that after taking dual operations on transitions and changing the weight of each final state to its complement,a new L-valued alternating tree automaton is achieved which is the complement of the starting one.Afterwards,the closure is illustrated under conjunction and disjunction of languages accepted by L-valued alternating tree automata.Finally,the expressive power of L-valued alternating tree automata,L-valued tree automata,and L-valued nondeterministic automata are discussed.The equivalence relationship is proved between L-valued alternating tree automata and L-valued tree automata,the algorithms are given between them and complexities are discussed of algorithms;simultaneously,a method is provided to show how to use L-valued nondeterministic automata to simulate L-valued alternating tree automata.
作者
魏秀娟
李永明
WEI Xiu-Juan;LI Yong-Ming(College of Mathematics and Information Science,Shaanxi Normal University,Xi’an 710119,China;College of Computer Science,Shaanxi Normal University,Xi’an 710119,China)
出处
《软件学报》
EI
CSCD
北大核心
2019年第12期3605-3621,共17页
Journal of Software
基金
国家自然科学基金(11671244,11271237)
高等学校博士学科点专项科研基金(20130202110001)~~
关键词
格值交替树自动机
格值正布尔公式
对偶运算
格值计算树
接受运行
L-valued alternating tree automata
L-valued positive Boolean formula
dual operation
L-valued computation tree
accepting run