-
题名STGA的变种及其互模拟验证
- 1
-
-
作者
李舟军
陈火旺
钟广军
王兵山
-
机构
国防科学技术大学计算机学院
-
出处
《计算机学报》
EI
CSCD
北大核心
2000年第4期345-355,共11页
-
基金
国家"八六三"高技术研究发展计划项目!(863-306-ZT05-06-1)
国家自然科学基金!(69873045)
-
文摘
为刻画和验证无穷值域上的传值进程，Ｈｅｎｎｅｓｓｙ和Ｌｉｎ先后提出符号迁移图（ＳＴＧ）和带赋值符号迁移图（ＳＴＧＡ）作为传值进程的语义表示模型，并给出了相应的强互模拟算法．为将该方法推广至实际应用中更常用的弱互模拟等价和观察同余的验证问题，该文首先引入了ＳＴＧＡ的一个变种，它与原模型的不同之处在于将符号迁移上赋值和符号动作的执行次序颠倒，因而可定义此种ＳＴＧＡ结点间的符号双迁移关系．文中提出了从正则传值进程生成此类ＳＴＧＡ的全部产生规则，并基于Ｌｉｎ的迟强互模拟算法给出了针对此类ＳＴＧＡ的早强互模拟算法．然后利用符号双迁移关系引入了带赋值的早符号观察图（ＥＳＯＧＡ）和早符号同余图（ＥＳＣＧＡ），将上述算法推广至早弱互模拟等价和早观察同余的情况．但符号迁移上赋值的出现有可能导致ＥＳＯＧＡ和ＥＳＣＧＡ为无穷图，从而使本文所给的弱互模拟算法在适用范围和效率上受到一定的局限．最后，作为一种可应用的情况，进一步考虑了符号迁移图的弱互模拟等价和观察同余验证问题．此时由符号双迁移关系生成的符号观察图和迟符号同余图必为有穷图，因而我们的弱互模拟等价算法是可行的．与此同时，文中还给出并证明了符号迁移图上的τ－循环和τ－边消去?
-
关键词
传值进程
符号迁移图
互模拟
算法
stga
-
Keywords
value-passing process, symbolic transition graph,symbolic transition graph with assignment, bisimulation, predicate equation system
-
分类号
TP301.6
[自动化与计算机技术—计算机系统结构]
-
-
题名马铃薯StGA2ox基因在块茎发育过程中的作用
- 2
-
-
作者
元元
宁白
敖恩宝力格
萨日娜
-
机构
内蒙古师范大学生命科学与技术学院
-
出处
《内蒙古师范大学学报(自然科学版蒙古文)》
2024年第4期6-10,70,共6页
-
文摘
GA2ox基因是赤霉素合成代谢途径中分解赤霉素或其前体的分解酶的编码基因。本研究利用病毒诱导的基因沉默技术对马铃薯StGA2ox基因的表达进行下调,探究其在赤霉素代谢途径中的作用以及对马铃薯生长发育的影响。结果表明,经基因沉默后StGA2or基因的相对表达量显著下降,相较于野生型和pTRV2空载体对照组,转基因植株的株高显著增加,但地下块茎的结薯量相对减少,说明StGA2ox基因的沉默对块茎形成造成一定的抑制。所得结果为马铃薯生长发育过程中赤霉素调节作用的研究,以及利用转基因技术培育马铃薯新品种提供了有价值的参考依据。
-
关键词
马铃薯
stga2ox基因
基因沉默
-
分类号
S532
[农业科学—作物学]
-
-
题名带复杂数据结构的模型检测工具
- 3
-
-
作者
张轶
林惠民
-
机构
中国科学院软件研究所计算机科学重点实验室
-
出处
《计算机研究与发展》
EI
CSCD
北大核心
2004年第11期1990-1999,共10页
-
基金
国家自然科学基金项目 (6983 3 0 2 0 )
-
文摘
模型检测是近二十几年来最成功的自动验证技术之一 ,而模型检测工具的开发是将模型检测和实际相结合的关键 为了有效地对涉及到复杂数据类型的并发传值系统进行模型检测 ,总结了以扩展的带赋值符号迁移图和模态图分别作为并发系统和逻辑公式的语义模型来实现模型检测工具的工作 ,特别是将复杂数据结构引入传值进程定义语言和带赋值符号迁移图
-
关键词
模型检测
传值进程
带赋值符号迁移图
谓词μ演算
复杂数据结构
-
Keywords
model-checking
value-passing process
stga
predicate μ-calculus
non-trivial data structures
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
