Büchi自动机确定化分析工具

无限字自动机的确定化是理论计算机研究重要的一部分,在形式化验证,时序逻辑,模型检测等方面有重要应用.自Büchi自动机提出半个世纪以来,其自动机的确定化算法始终是其中的基础.有别于当初只是在理论上对其大小上下界的探索,利用日新月异的高性能计算机技术不失为一种有效的辅助手段.为了深入研究非确定性Büchi自动机确定化算法的实现过程,希望重点研究确定化过程中的索引能否继续被优化的问题,实现确定化研究工具NB2DR.可以对非确定性Büchi自动机进行高效的确定化,并通过工具提供的分析其确定化过程来达到对其确定化算法改进的目的.通过对生成的确定性无限字自动机的索引的深入分析来探索相关索引的理论.该工具还实现了可以根据需要的Büchi自动机的大小与字母表参数,生成确定化的Rabin自动机族,亦可以反向根据需要的指定索引的大小来生成全部Büchi自动机族,测试生成无限字自动机的等价性等功能.

基于标记Büchi自动机的时态描述逻辑ALC-LTL模型检测

时态描述逻辑将描述逻辑的刻画能力引入到命题时态逻辑中,适合于在语义Web环境下对相关系统的时态性质进行刻画。为了对这些时态性质进行高效的验证,在ALC-LTL的基础上研究了时态描述逻辑的模型检测问题。一方面,使用时态描述逻辑ALC-LTL公式来表示待验证的时态规范;另一方面,在对系统建模时借助描述逻辑ALC对领域知识进行刻画。针对上述扩展后得到的模型检测问题,提出了基于自动机的ALC-LTL模型检测算法。模型检测算法由3个阶段组成:首先将时态规范的否定形式和系统模型分别构造成标记büchi自动机;接下来构造这两个自动机的乘积自动机,并将关于ALC的推理机制融入到乘积自动机的构造过程中;最后对该乘积自动机进行判空检测。与LTL模型检测相比,时态描述逻辑ALC-LTL的模型检测引入了描述逻辑的刻画和推理机制,可以在语义Web环境下对语义Web服务等复杂系统的时态性质进行刻画和验证。

从基于迁移的扩展Büchi自动机到Büchi自动机

目前的模型检测方法中,有一种方法是基于自动机来实现的.具体做法是:将抽象出的系统模型用Büchi自动机来表示,将需要验证的性质用LTL(lineartemporallogic)公式来表达;然后将LTL公式取反后转化为Büchi自动机,并检查这两个自动机接受语言之间的包含关系.有一类LTL公式转化为Büchi自动机的算法是:在计算过程中,首先得到一个标注在迁移上的扩展Büchi自动机(transition-basedgeneralizedBüchiautomaton,简称TGBA),然后把这种扩展Büchi自动机转换成非扩展的Büchi自动机.针对这类转换算法,根据Büchi自动机接受语言的特点,重新定义了基于迁移的扩展Büchi自动机的求交运算,减少了需要复制的状态个数,使转换后的自动机具有较少的状态.测试的结果表明:对随机产生的公式,新算法相对于以往的算法有明显的优势.

基于启发式SCCs的广义Büchi自动机判空检测算法

基于自动机理论模型检测的一个关键算法是判断有穷状态系统是否满足属性的判空检测.对标准Büchi自动机作判空检测,容易引起状态爆炸.本文以TGBA为研究对象,提出基于启发式SCCs的广义Büchi自动机判空检测算法.该算法在on-the-fly算法的基础上结合启发式深度优先搜索和SCCs检测算法,能较快地判断TGBA的非空性.通过正确性证明、复杂性分析和实验验证了该算法的正确可行性.在TGBA非空的情况下,该算法的时空性能比已有算法更优.

模糊Büchi自动机的等价刻画

模糊语言的研究是形式语言研究的焦点之一,然而如何对模糊语言进行刻画甚至更好地分类是其中一个重要研究方向.文章在模糊ω-语言的研究基础上,从模糊逻辑角度研究了模糊ω-正则语言的等价刻画.首先借助广义子集构造方法,证明了任一模糊Büchi自动机与具有分明初始状态和状态转移函数且具有模糊终状态的模糊Büchi自动机是等价的,藉此研究了模糊ω-正则语言的代数刻画和层次刻画,讨论了模糊ω-正则语言关于正则运算的封闭性;其次引入单体二阶Lukasiewicz逻辑的概念,给出模糊Büchi自动机识别语言的等价逻辑刻画;最后通过引入ω-星自由和ω-非周期模糊ω-语言,利用'层次化'处理技巧得到了多值逻辑意义下的分类定理,对模糊ω-正则语言给出了一种分类方法.

基于LTL Tableau的自动机构造

基于线性时序逻辑(LTL)的模型检验是使用较为广泛的技术。该种模型检验最终归结为有穷自动机的判空问题,其复杂性来源于性质和模型乘积自动机的状态空间膨胀。作者提出了一种构造迟滞交换Co-Büchi自动机(Stuffer Alternating Co-Büchi)的具有线性复杂度的方法,该方法能够降低最终乘积自动机的空间复杂度。

Büchi自动机的优化综述

对Büchi自动机进行优化是提高基于自动机的模型检测效率的重要手段。对直接模拟关系、延迟模拟关系和公平模拟关系的概念,进行了比较,并探讨了基于这些模拟关系的自动机优化方法。基于左右语言的优化是完全基于自动机理论的优化方法,于是深入探讨了利用左右语言对Büchi自动机的优化绍方法。最后对未来的研究方向作了简要的介绍。

基于Büchi自动机化简的JavaMOP监控器构造方法

为了提高JavaMOP对程序运行时验证的效率,提出一种基于Büchi自动机化简的JavaMOP监控器构造方法,降低JavaMOP运行时验证的时间和内存开销。该方法将线性时态逻辑(linear temporal logic,简称LTL)描述的属性规范转化为Büchi自动机,利用自动机化简规则对Büchi自动机进行冗余化简,化简后的Büchi自动机再转化为确定性有限自动机,并由此得到监控器的抽象表示。实验结果表明,与JavaMOP现有监控器的方法相比,该方法能够得到更小的Büchi自动机,从而加速JavaMOP监控器的构造过程。

一种基于Büchi自动机的LTL程序模型检测方法

时序逻辑程序的形式化验证对提高程序的正确性具有重要意义。基于自动机的理论,用标签转移系统(S)表示程序的行为,用时序逻辑公式(F)描述程序的性质,构建相应的Büchi自动机,从而证明形式化公式SF是否可满足。

Chi-CpG NP的制备及其对rNMB0315蛋白的免疫效果

目的制备黏膜免疫佐剂Chi-CpG NP,并检测其对重组B群脑膜炎奈瑟菌0315蛋白(rNMB0315)的免疫效果。方法用壳聚糖纳米颗粒(Chi NP)包裹免疫刺激分子(CpG-ODN)合成Chi-CpG NP,随后检测其理化性质和安全性。将不同黏膜免疫佐剂与rNMB0315充分混合、吸附,滴鼻免疫雌性BALB/c小鼠,检测PBS组、rNMB0315组、rNMB0315+CpG组、rNMB0315+Chi NP组、rNMB0315+Chi-CpG NP组小鼠免疫42天后的体液免疫(IgG、IgG1、IgG2a、sIgA)、细胞免疫水平[白细胞介素(IL)-4、γ干扰素(IFN-γ)、IL-17A]、免疫保护效果以及血清体外杀菌活性。结果成功制备的Chi-CpG NP呈球形,大小均一,有较好的吸附性能和良好的安全性。小鼠免疫42天后,体液免疫和细胞免疫水平rNMB0315+Chi-NP组、rNMB0315+Chi-CpG NP组高于rNMB0315组(P<0.05);rNMB0315+Chi-CpG NP组高于rNMB0315+CpG组和rNMB0315+Chi-NP组(P<0.05)。致死剂量B群脑膜炎奈瑟菌攻击各组小鼠后,rNMB0315+Chi-CpG NP组小鼠存活率最高;血清体外杀菌抗体滴度为1∶4。结论成功制备了Chi-CpG NP。Chi-CpG NP能增强rNMB0315蛋白的免疫效果,提高小鼠的存活率。

基于一维混合元胞自动机模型的汽车变厚度B柱设计

为了将连续变厚度轧制工艺更好地应用于车身轻量化设计和耐撞性设计,针对连续变厚度轧制(TRB)B柱不同区域厚度分布的设计问题,提出一维混合元胞自动机(ODHCA)模型。建立变厚度B柱的ODHCA模型,提取元胞厚度作为设计变量,确定其局部更新规则;根据连续变厚度轧制工艺的特点定义设计区域的约束条件,确定ODHCA方法的迭代方式与收敛准则。结果表明:应用ODHCA方法,在等质量情况下,胸部、腹部、骨盆位置侵入量分别降低了8.8%、13.4%、14.6%;而在质量降低14.2%时,上述各部位的位置侵入量分别降低了5.8%、9.6%、10.3%。因而,该方法可以改善B柱的变形模式,提高侧面碰撞安全性能,并满足轻量化要求。

基于元胞自动机的5B70铝合金载人密封舱室加强筋组织演化研究

针对5B70铝合金密封舱体加强筋的微观组织演变问题,基于元胞自动机理论,引入拓扑算法,建立晶粒形核、长大和再结晶模型,研究了单道次微铸锻工序中加强筋的微观组织演变过程,分析了应变量对动态再结晶与静态再结晶晶粒尺寸及体积分数的影响。结果表明:最佳微锻应变量为0.3;在微锻过程中由于塑性变形温度过低,动态再结晶体积分数最大仅为35%,在下一道次的微铸阶段,该组织发生完全静态再结晶,晶粒均匀细小,约为30μm。

基于自动机理论的UML活动图模型检验方法

UML活动图被认为是最合适的软件过程描述语言,研究UML活动图的模型检验方法是很有必要的。提出一种基于自动机理论的UML活动图的模型检验方法。该方法给出UML活动图的形式语义,通过计算RTC-STEP,得到LTS,并将LTS映射到Büchi自动机,用LTL表示系统性质,并将LTL公式转换为相应的Büchi自动机,用基于自动机理论的模型检验方法检验UML活动图。

量子Müller自动机与单体二阶量子逻辑

给出量子Müller自动机(简称LVMA)的概念,通过引入量子有限步可识别语言和量子状态构造方法,证明了在量子逻辑意义下4类量子Müller自动机彼此相互等价.利用该等价性,建立了量子无穷正则语言的代数刻画和层次刻画,籍此研究了量子无穷正则语言关于无穷正则运算的封闭性.同时,给出了量子Müller自动机所识别语言的单体二阶逻辑描述,深化和推广了量子逻辑意义下的Büchi基本定理.

基于自动机理论的符号模型检验

状态爆炸是模型检验需解决的一个关键问题.基于GPVW算法,以及从LTL公式导出识别该公式的Büchi自动机,用OBDD符号表示,通过符号操作求解自动机乘积.采用符号方法求解出含有初始状态或接受状态的最大连通图,判断自动机是否存在初始状态能否到达含有接收状态的最大连通分支,从而判定所接受的语言是否非空来模型检验LTL公式.采用本文所提出模型检验LTL公式的方法,能在一定程度上解决空间爆炸问题.

一种基于自动机理论的LTL检验符号优化方法

模型检验是一种重要的形式化自动验证技术。检验一个模型是否满足LTL公式,可以把LTL公式转换为一个表示相同无穷状态序列的ω自动机,通过转换后的ω自动机与系统自动机的乘积判空来进行模型检验。由于自动机的体积是模型检验的一个关键性问题,为了得到尽可能小的自动机,在LTL公式转换为ω自动机之前,对LTL公式进行预处理来减少冗余,然后基于ROBDD,通过布尔技术优化自动机。

线性时序逻辑转换Büchi自动机的按需即时算法

将线性时序逻辑公式转换成Büchi自动机是显式模型检测中的关键环节,Tableau规则是常用转换算法。该文提出了基于Tableau规则的改进算法,将线性时序逻辑公式转换成基于迁移的Büchi自动机。通过在状态和迁移中加入∪公式的满足信息,实现了用一个接受条件集合判断执行序列是否可接受,避免了使用多个接受条件集合进行判断。改进算法引入了按需即时(on-the-fly)去扩展化机制,算法展开状态节点的同时进行状态有效性检测,删除无效节点,合并等价状态和迁移,避免了后置化简。与其他转换工具进行比较实验表明,该算法具有执行速度快、生成自动机的状态数和迁移数少的特征。

UV-B对不同发育时期离体蓝莓主要果实品质及相关酶活性的影响

该研究以幼果期、白果期、转色期的离体‘北陆’蓝莓果实为试材,设置0(CK)、5、10、15min紫外光辐照处理,24h后取样分析蓝莓果实中可溶性糖、总酚、类黄酮和花青苷含量,以及苯丙氨酸裂解酶(PAL)和查尔酮异构酶(CHI)活性的变化,探究UV-B紫外照射处理对不同发育时期蓝莓主要果实品质及相关酶活的影响。结果显示:(1)对于幼果期蓝莓,5min UV-B处理可显著增加果实内可溶性糖含量;10min UV-B处理果实PAL活性增加效果最为显著;15min UV-B处理对果实总酚和花青苷积累的促进作用最大,但显著降低了类黄酮含量和CHI活性。(2)对于白果期蓝莓,5min UV-B处理显著增加了果实类黄酮含量和CHI活性,10min处理使果实可溶性糖和总酚含量较对照分别增加25%和18%;15min处理对果实花青苷含量和PAL活性影响作用最大。(3)对于转色期蓝莓,各处理除果实可溶性糖及类黄酮含量降低外,其余物质含量均显著增加。(4)UV-B处理并未改变果实发育过程中可溶性糖、总酚、类黄酮和花青苷含量及PAL、CHI酶活性的积累规律。(5)蓝莓果内PAL活性与其可溶性糖、总酚和类黄酮的积累呈极显著正相关关系,而CHI活性仅与其可溶性糖呈极显著正相关。研究表明,UV-B辐照处理促进了幼果期和白果期可溶性糖的积累,也能促进不同发育时期蓝莓果实总酚和花青苷及白果期类黄酮的积累,对蓝莓果实主要品质能够产生积极的影响。

AZ31B镁合金双道次热变形过程流变应力特征模拟研究

建立了一类镁合金双道次热变形过程的二维元胞自动机模型。考虑到镁合金具有六重对称的密排六方晶体结构,模型采用了六边形元胞网格。另外,通过计算位错密度演变和设定晶粒形核长大规则,模型将热变形过程中动态再结晶、静态回复、静态再结晶、亚动态再结晶和晶粒长大等单个物理过程耦合到一起。为了验证模型,将其应用到AZ31B镁合金单道次和双道次热压缩过程。探讨了不同变形温度、应变速率、道次间隔和预应变对应力-应变曲线的影响。将计算结果和实验结果进行了对比,吻合较好。

1999年集集地震前后台湾地区地震b值及应力场时空演化特征

地震b值时空分布及演化是地震孕育研究及地震危险性评价的重要指标.本文首先基于台湾地区1999年至2005年期间的地震目录数据,对该区进行地震b值时空扫描,得到了台湾地区的b值时空分布,分析了1999年M_(W)7.6台湾集集地震前后b值时空演化特征;进一步基于GPS速度场数据估算了地震前后区域的应变率和差应力率分布特征与变化;最后分析并探讨了b值分布、演化与差应力率场的关系.结果显示:(1)集集地震前后的1999—2005年,震中所在地震区的b值呈现出震前降低-震后先升高后降低的演化特征,反映区域应力的累积-释放-累积的过程;(2)集集地震震后的2003—2005年,由GPS速度场数据获得的震源区差应力率较大,意味着差应力累积速率较高,可能与震后中下地壳和上地幔黏弹性应力松弛有关,而相同时间段震源区的b值较高,意味着震源区附近上地壳差应力仍然较低,该时段震后过程仍在持续;(3)台湾西南和东部海岸山脉逆冲作用较强,差应力率较大,而b值较小,均可能意味着其背景差应力水平较高;台湾地区沿中央山脉由北至南存在扩张拉伸作用,差应力率较小,而b值较大,都意味着背景差应力水平可能较低.本文的结果对认知台湾地区地震活动变化、台湾地震孕育过程及地震b值与应力的关系具有重要作用.