没有合适的资源?快使用搜索试试~ 我知道了~
温馨提示
半结构化数据正以其灵活性而成为解决Internet环境下互操作语义层面问题的重要工具和网络数据交换格式的标准。从基础理论层面上对版结构化数据进行研究,在考察了进程代数和空间逻辑的有关结果后,从模型和逻辑系统的角度对半结构化数据特别是XML语言进行刻画。在[1]的基础上,在数据模型中加入了受限算子,并提出一种新的空间逻辑――树逻辑,在其中引入了一个新的模态算子,它们的意义在于能够对私有数据的性质进行刻画和表达。此外,通过修正数据模型中的同余关系,使得模型符合数据的有序性,从而使其更为合理。在此基础上证明了树
资源推荐
资源详情
资源评论




























第
41
卷第
2
期
2005
年
3
月
南京大学学报(自然科学)
JOURNAL
OF
NANJING
UNlVERSITY
(NATURAL
SCIENCES)
Vol.
41
, No.2
Mar.
,
2005
面向半结构化数据的树逻辑及其性质研究*
韩婷婷楠,陈韬略,俞春,吕
建
(南京大学计算机软件新技术国家重点实验室,南京,
210093)
摘
要:
半结构化数据正以其灵活性而成为解决
Intemet
环境下互操作语义层面问题的重要工具和
网络数据交换格式的标准.从基础理论层面上对版结构化数据进行研究,在考察了进程代数和空间逻
辑的有关结果后,从模型和逻辑系统的角度对半结构化数据特别是
XML
语言进行刻画.在
[lJ
的基础
上,在数据模型中加入了受限算子,并提出一种新的空间逻辑一-树逻辑,在其中引入了一个新的模态
算子,它们的意义在于能够对私有数据的性质进行刻画和表达.此外,通过修正数据模型中的同余关
系,使得模型符合数据的有序性,从而使其更为合理.在此基础上证明了树逻辑系统公式可满足性的不
可判定性,从而说明针对整个树逻辑系统的模型检测算法是不存在的.同时选择了其中一个子逻辑系
统,给出了其模型检测算法,并证明了该算法的正确性.
关键词:
半结构化数据,树逻辑,不可判定性,模型检测
中图分类号:
TP
30
1.
6
Tree Logic for Semistructured Data and
It
s Properties
Han
Ting-Ting
,
Chen
Ta
o-
Lue ,
Yu
Chun ,
Lü
Jian
(S
归
te
Key
La
boratory for Novel
So
ftware Technology, Nanjing University,
Nanji
吨,
210093
,
China)
Abstract:
With
the development of
Intemet
,
the
semistructured data have already become a very important
t
,∞
1
to deal
with the problems of communication
at
the level of
semanti
臼
and
at
the sarne time become the standard of the data
exchangefo
口丑
in
Intemet.
From
the theoretical point of view, we characterize
the
semistructured
data
,臼.p
eciall
y the
XML language
, both in data model and in logic system inspired by the results of
pr
田
ess
algebra and
spatiall
,唔
ic.
Ba
sed on
[1
],
the
附
called
restriction operator
is
introduced into the data model and
at
the sarne time, we provide a new spatial
logic-tree
1
。如,
in which a new modal operator
is
added.
The
two operators are mainly used to manipulate and
d
臼
cribe
the properties of private data
elemen
毡,
which
becom
巳
s
more and more important in modeling and analyzing semistructured
data for security
or
other considerations.
Bes
ides, we refine the congruence relation in
the
data model
50
that
the order of
the data is
pr
巳
sented.
This
is
more rational since it is not always the sarne if the order of
two
su
b-
trees
is
exchanged.
The
properties of the tree logic
system
盯
e
studied.
We
prove the undecidability of the satisfaction problem for the
1
,唔
ic.
As
a
result
, model checking the whole tree logic system is
im
严)SS
ible.
In addition, we
chα
配
an
important
su
b-
Iogic system for
which a model checking algorithm is presented.
The
∞,
rrectn
臼
s
of the algori
thm
is
al50
proved.
Key words: semi-structure
da
钮,
tree logic , undecidability, model checking
*基金项目:国家重点基础研究发展规划
973
项目
(2002CB12002)
,国家自然科学基金
(60273034
,
60233010
,
60403014)
,
国家
863
高科技项目
(2002
AA1
16010)
,江苏省自然科学基金
(B
K2
002203
,
B
K2
002409)
收稿日期
:2003
-
09
-
23
H
通讯联系人,
E-matl:
hantt@ics
时
u.
edu.
cn

第
2
期
韩婷婷等:面向半结构化数据的树逻辑
.
163
.
Intemet
的迅猛发展,尤其是通信体系结
构的不断完善和丰富,使得建立
Intemet
规模
的信息供求关联的需求日益强烈.相对于传统
的结构化数据而言,半结构化数据具有相当的
灵活性,业已成为解决
Intemet
环境下互操作
语义层面问题的重要工具,因而备受学术界和
工业界的瞩目.半结构化数据的灵活性体现在
它介于原始非结构化数据和严格结构化了的数
据之间,一般而言,前者没有良定义的语法特
征,而后者(如关系型数据)的结构和语义则相
对固定的,因而它们都不能很好地满足不规则
或易变信息承载的需要.半结构化数据保留了
结构化数据的结构化特征,同时它能够通过语
义层面的附加内容来表示传统结构化数据所不
能或很难表示的信息.作为半结构化数据的典
型代表,
XML[2J
业已成为网络数据交换格式的
标准.由于不同数据源一般都能方便地转化为
XML
,因此元论作为-种中间过渡还是最终结
果,
XML
的运用必然会越来越广泛,其影响也
会越来越深远.目前,对
XML
的研究主要集中
在对数据有效地存取、查询、挖掘等具体技术和
应用相关的方面;在其基础理论方面的研究还
停留在起步阶段,如何通过借鉴传统关系型数
据库模型的理论,为半结构化数据建立数据模
型,并在此基础上探讨数据的存取、查询、挖掘
等机制,是我们研究的核心问题.
目前,对半结构化数据,特别是
XML
的理
论研究主要集中在两个方面,一是将其作为新
-代的程序设计和查询语言的研究,二是相关
的类型系统和逻辑系统的研究
[lJ
其中,前者
主要是针对
XML
标准处理语言,如
XSLT
的
扩充和功能增强,代表性工作有
Xduce[3J
和
Cd
uce[4J
等;而后者一方面是针对
XML
标准模
式定义,如
DTD
、
XML
Sc
hema
的抽象和扩充,
另一方面也提供了相关语言和机制的形式基
础
[5J
本文的工作主要针对后者进行.
迄今为止已经有一些学者进行了相关的研
究工作.在考察了进程代数和空间逻辑的有关
结果后,受
c.
Ca
lcagno[lJ
等人进程代数和空
间逻辑
(spatiallogic)[6J
的相关工作启发,提出
了从模型的角度利用一种类似于
Mobile
Am
bient[7J
演算的数据模型来刻画半结构化数
据;从逻辑系统的角度提出了一种特殊的空间
逻辑,证明了公式的正确性
(validity)
问题和其
可满足性问题是等价的,并解决了公式正确性
的判定问题.然而,我们发现其工作对半结构
化数据中私有数据建模问题的关注还远远不
够.鉴于私有数据普遍存在于半结构化数据
中,且对于半结构化数据的表示有着重要的作
用,因而研究私有数据就显得十分重要.另
外,将树或某种图模型作为半结构化数据的结
构已成为一种共识,由于半结构化数据的表达
是有序的,所以相应的结构也应是有序树或有
序图;但是现有演算的同余关系并没有很好地
反映这-点.综合考虑以上内容,本文的工作
在于对
[1J
所提出的数据模型和空间逻辑进行
了修正和改进;具体而言,本文提出一种扩充
的空间逻辑-一树逻辑,在其中引入了一个新
的模态算子,同时在数据模型中加入了与
π
演
算
[8J
中
restriction
算子类似的受限算子,它们
的共同作用在于对私有数据的性质进行刻画和
表达.此外,针对原有数据模型对数据顺序描
述的欠缺,本文通过修正数据模型中的同余关
系,使模型能符合数据的有序性,从而使其更为
合理.进而研究了树逻辑公式可满足性的判定
性问题,通过构造一阶逻辑系统和该逻辑系统
的映射,由一阶逻辑系统的不可判定性证明了
树逻辑系统公式可满足性的不可判定性;此结
果的意义在于,鉴于整个逻辑系统的模型检测
问题和可满足问题是等价的,从而证明了针对
整个逻辑系统的模型检测算法是不存在的,这
也意味着研究重点应该放在其中的有意义的子
逻辑上的模型检测算法上.基于此,本文选择
了其中一个较为重要的子逻辑系统,给出了其
模型检测算法,同时证明了该算法的正确性.
1
模态逻辑
本节给出带私有标号的数据模型作为扩充
的数据模型,并提出相应的模态逻辑系统.
剩余8页未读,继续阅读
资源评论


weixin_38652147
- 粉丝: 5
上传资源 快速赚钱
我的内容管理 展开
我的资源 快来上传第一个资源
我的收益
登录查看自己的收益我的积分 登录查看自己的积分
我的C币 登录后查看C币余额
我的收藏
我的下载
下载帮助


最新资源
- 略论农村中小学教育信息化工作策略.docx
- 某发电厂脱硫系统热控安装施工技术措施.doc
- matlab的电力系统谐波抑制仿真分析研究.doc
- 互联网环境下的高中英语教学策略.docx
- 公司人事管理规章制度-.doc
- PLC工业用智能风淋控制系统方案设计书参考资料.doc
- 都市假日园林绿化工程施工组织设计方案.doc
- 【STM32MP1线上课程】STM32MP1 online training_14_OpenSTLinux Develo
- STM8S片上闪存和控制系统介绍.pdf
- 工程挡土墙毕业设计计算书.doc
- 吉林省劳动合同书.doc
- 浙江省安装工程预算员应试笔记.doc
- 阐述电气自动化工程控制系统的现状及其发展趋势.docx
- 合肥市某住宅工程质量通病防治措施.doc
- 监理工作评价表.doc
- 小时学会Access轻松打造图书管理系统.docx
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈



安全验证
文档复制为VIP权益,开通VIP直接复制
