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

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

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ü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自动机的求交运算,减少了需要复制的状态个数,使转换后的自动机具有较少的状态.测试的结果表明:对随机产生的公式,新算法相对于以往的算法有明显的优势.

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

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

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

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

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

模糊语言的研究是形式语言研究的焦点之一,然而如何对模糊语言进行刻画甚至更好地分类是其中一个重要研究方向.文章在模糊ω-语言的研究基础上,从模糊逻辑角度研究了模糊ω-正则语言的等价刻画.首先借助广义子集构造方法,证明了任一模糊Büchi自动机与具有分明初始状态和状态转移函数且具有模糊终状态的模糊Büchi自动机是等价的,藉此研究了模糊ω-正则语言的代数刻画和层次刻画,讨论了模糊ω-正则语言关于正则运算的封闭性;其次引入单体二阶Lukasiewicz逻辑的概念,给出模糊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是否可满足。

Visualization of Gene Mutation Complicated Pattern of Hepatitis B Virus Based on Cellular Automata

Hepatitis B virus shows instantaneous and high rate mutations in biological experiments, some sorts of which affect the efficiency of virus replication greatly through enhancing or depressing the viral replication, while others have no influence at all. Taking advantage of prominent features of cellular automata, we simulate the effect of hepatitis B virus gene mutation on its replication efficiency. The computer simulation results demonstrate the feasibility of our novel model by comparing with the results of biological experiments.

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辐照处理促进了幼果期和白果期可溶性糖的积累,也能促进不同发育时期蓝莓果实总酚和花青苷及白果期类黄酮的积累,对蓝莓果实主要品质能够产生积极的影响。

Type B非接触智能卡防冲突模型的设计与实现

在分析了TypeB非接触智能卡防冲突的基本工作原理的基础上,采用有限状态机模型对卡上防冲突协议的实现算法进行了数学表述和状态转换的设计,并采用统一建模语言UML中的状态图描述了卡上的防冲突过程。最后,在智能卡芯片上实现了防冲突协议,实际应用证明系统运行正确。

基于LTL Tableau的自动机构造

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

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

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

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值与应力的关系具有重要作用.

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

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

属性序列图:形式语法和语义

在基于场景的软件工程中,时态逻辑被广泛地用来推理并发系统的正确性.模型检验技术允许自动检验系统模型和给定的属性之间的一致性,这些属性常用线性时态逻辑公式来表示.不幸的是,由于这些公式具有复杂的结构使得模型检验技术很难应用在工业实践中.属性序列图可以用来解决这种问题,它是一种基于场景的可视化的语言,容易理解并且具有较强的表达能力,能够克服当前工业中常用的符号中存在的诸多表达缺陷.为了能够完全清晰地描述和理解属性序列图,使其能够广泛地应用,给出其形式语法和基于Bchi自动机的形式语义,并进行了实例研究,讨论了其应用前景.

基于线性时态逻辑的Petri网模型检测

Petri网是一种重要的数学工具,它能有效地对并发系统进行描述和建模。线性时态逻辑LTL则是描述和验证并发系统特性的一种重要的形式化工具,它能方便准确地描述并发系统的重要性质,如安全性和活性。文章深入描述了线性时态逻辑、Büchi自动机、Petri网和同步积之间的内在联系,并探讨了基于线性时态逻辑的Petri网模型检测策略。与其它方法比较,这种模型检测的策略结合了线性时态逻辑和Petri网模型的不同优点,增强了Petri网的模型分析和验证能力。最后,通过对一个并发系统形式化的模型检测分析,验证了相应的结论。

基于启发式NDFS的模型检测新算法

以带有多个可接受条件的广义Büchi自动机为研究对象,提出基于启发式NDFS的模型检测新算法.该算法结合on-the-fly算法与启发式NDFS算法,能较快地判断出广义Büchi自动机非空性,通过理论证明和实验验证了算法的正确性和可行性.与已有算法相比,在广义Büchi自动机非空的情况下,该算法减少了系统状态空间的搜索,提高了检测效率,且能形成相应反例,为缓解形式化验证中的状态空间爆炸问题提供了有效的解决途径,为安全苛求系统的安全性保障提供了有力支撑,丰富了基于模型的软件形式化开发方法.

实时系统形式规格说明在PVS中的建立

本文首先简介了时间自动机和时间B櫣chi自动机形式模型,结合时间化时序逻辑(TimedTemporalLogic)的语法和语义,利用定理证明器PVS(PrototypeVerificationSystem)实现了定义在时间自动机状态(或运行)上的时间化分支(或线性)时序逻辑规格说明的形式体系。在此基础上,结合一个经典的实时系统实例,用该体系对其实时特性进行了形式描述和形式验证,并得到了良好的结果。