2019格值交替树自动机-魏秀娟 , 李永明.pdf

上善若水

160

17页

0次

2022-05-23

免费下载

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn

Journal of Software,2019,30(12):3605−3621 [doi: 10.13328/j.cnki.jos.005611] http://www.jos.org.cn

格值交替树自动机

∗

魏秀娟

李永明

1,2

(陕西师范大学数学与信息科学学院,陕西西安 710119)

(陕西师范大学计算机科学学院,陕西西安 710119)

通讯作者: 李永明, E-mail: liyongm@snnu.edu.cn

摘要: 交替(树)自动机因其本身关于取补运算的简洁性及其与非确定型(树)自动机的等价性,成为自动机与模

型检测领域研究的一个新方向.在格值交替自动机与经典交替树自动机概念的基础上,引入格值交替树自动机的概

念,并研究了格值交替树自动机的代数封闭性和表达能力.首先,证明了对格值交替树自动机的转移函数取对偶运

算,终止权重取补之后所得自动机与原自动机接受语言互补这一结论.其次,证明了格值交替树自动机关于交、并运

算的封闭性.最后,讨论了格值交替树自动机和格值树自动机、格值非确定型自动机的表达能力;证明了格值交替树

自动机与格值树自动机的等价性,并给出了二者相互转化的算法及其复杂度分析;同时,提供了用格值非确定型自动

机来模拟格值交替树自动机的方法.

关键词: 格值交替树自动机;格值正布尔公式;对偶运算;格值计算树;接受运行

中图法分类号: TP301

中文引用格式: 魏秀娟,李永明.格值交替树自动机.软件学报,2019,30(12):3605−3621. http://www.jos.org.cn/1000-9825/5611.htm

英文引用格式: Wei XJ, Li YM. L-valued alternating tree automata. Ruan Jian Xue Bao/Journal of Software, 2019,30(12):

3605−3621 (in Ch inese). http://www.jos.org.cn/1000-9825/5611.htm

L-valued Alternating T r ee Automata

WEI Xiu -Jua n

, LI Yong-Ming

1,2

(College of Mathematics and Information S cience, Shaanxi Normal Univ ersity, Xi’an 710119 , China)

(College of Computer Science, Shaanxi Normal Univ ersity, Xi’an 710119, China)

Abstra ct : Because of the simplicity of taking complement operation on alternating (tree) automata and the equivalence relationship

between alternating (tr ee) automata and nond eterministic (t ree) automata, t he study on alternating (tree) automat a becomes a new r es ear ch

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 operati ons on transitions and changing th e 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 po wer 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 auto mata.

Key words: L-valued alternating tree automata; L-valued positive Boolean formula; dual operation; L-valued computation tree;

accepting run

∗ 基金项目: 国家自然科学基金(11671244, 11271237); 高等学校博士学科点专项科研基金(20130202110001)

Foundation item: National Natural Science Found ation of China (11671244, 11271237); Research Fund for th e Doctoral Program of

Higher Education of China (20130202110001)

收稿时间: 2016-0 9-18; 修改时间: 2018-03-20; 采用时间: 2018-05-29

3606

Journal of Software 软件学报 Vol.30, No.12, December 2019

非确定性在计算理论中有着重要意义

[1−5]

.从逻辑层面看,非确定计算只涉及存在量词,而作为非确定的推

广,“交替”在存在量词的基础上又增加了全称量词.Chandra 将交替的概念与自动机相结合,提出了交替自动机

的概念

[6]

,随后,这一类型的自动机在形式化证明中被作为一种有用的模型普遍使用

[7−14]

Zhou

[15]

在原有交替

-有穷自动机接受条件的基础上定义了 6 种新形式的接受条件,并研究了交替

-有穷

自动机在这些条件下接受语言的能力.Vardi 在研究线性时序逻辑

[14]

时,给出了用自动机理论方法来研究模型检

测的新思路,即,把模型检测的可满足性问题转化为判断自动机语言是否为空的问题来讨论.Vardi 运用 Muller

等人给出的交替(Büchi) 自动机与非确定型(Büchi ) 自动机的等价性,为任意给定的线性时序逻辑公式构造相应

的交替 Büchi 自动机,使得该自动机接受的语言恰好等于满足原线性时序逻辑公式的计算的全体.

Kupfer ma n 等人

[16,17]

定量地对交替自动机展开研究,提出了实数集上加权交替自动机的概念,并讨论了特

殊语义(如 Max,Sum,Sup,Lim sup 语义)下加权交替(Büchi)自动机的表达能力,同时研究了特殊语义下加权交替

(Büchi)自动机的代数封闭性.鉴于权值取值和语义选取的局限性,实数集上加权交替自动机的讨论较为特殊.另

外,终止状态的影响并未考虑在内,这也体现了 Kupferman 等人

[16,17]

讨论的局限性.基于这些问题,Wei 等人提出

了格值交替自动机的概念

[18]

,概念的创新性体现于权值的设置.文献[18]将转移的权值作为运行树叶子节点的

标记,使得树语言计算简洁化,同时保证了对转移取对偶运算、终止权重取补后所得的自动机与原自动机接受

语言互补这一性质;此外,Wei 等人比较了格值交替自动机与格值非确定型自动机的表达能力.

树作为重要的非线性数据结构,在计算机科学中应用非常广泛.在编译源程序时,树可被用来表示源程序的

语法结构;在数据库系统中,树可作为信息的重要组织形式.因此,关于输入为树结构的自动机研究也是非常有

意义的.但到目前为止,针对交替树自动机的研究仅有较少学者涉及

[11,19]

.Muller 等人在文献[10, 11]中针对经典

情形下的交替(Büc hi)(树)自动机展开讨论时指出:对交替(Büchi )(树)自动机的转移函数取对偶运算,并将终止

状态和非终止状态互换所得的自动机与原自动机接受的语言互补;同时讨论了交替(B üchi) (树)自动机与非确

定型(Büchi)(树)自动机的表达能力.

量化情形下输入为树(k 元

-树)结构的交替自动机暂未有人展开讨论,针对此类计算模型是否有如上结论,

本文即从此初衷展开研究且仅考虑有限输入树的情形.这里将 Muller 等人提出的交替树自动机的概念

[10,11]

和

Wei 等人在格值交替自动机

[18]

上的权值设置方式相结合,引入了格值交替树自动机的概念,讨论了其代数封闭

性和表达能力.特别地,将状态转移函数取对偶运算,终止权重取补之后即可得到与原自动机接受语言互补的格

值交替树自动机.此外,讨论了格值交替树自动机与格值树自动机之间的表达能力,说明了二者的等价性.最后

指出可用格值非确定型自动机来模拟格值交替树自动机.

1 预备知识

首先介绍本文的预备知识,更多详细内容参见文献[18−21 ].

1.1 树的相关概念

定义 1

[20]

. 元素组(

,rk )称为一个分级的字母表,其中,

为有限集合,rk 为

到自然数集合 N 上的一个映射

(在这里称为级映射).

在不引起混淆的情况下,通常用

表示(

,rk ),简称字母表.对任意的 k≥0,

(k)

∈

|rk(

)=k}.

定义 2

[20]

. 设 H∩

=∅.H 上

-项(

-树或简称树)构成的集合 T

(H)为满足下面两个条件的最小的集合 T:

(1)

(0)

∪H⊆T;

(2) 如果 k≥1,

∈

(k)

,且

,…,

∈T,则

(

,…,

)∈T.

当 H=∅,T

(∅)简记为 T

定义 3

[20]

. 树的高度 Height 和位置集 Pos 是从集合 T

分别到自然数集 N 和由自然数集生成的幺半群的幂

集P(N

)上的映射,递归定义如下.

(1) 对任意的

∈

(0)

,Pos(

)={

},Height(

)=0;

of 17

免费下载

软件学报计算机技术

关注

评论