科学发现的逻辑验证

R演算是一个关于逻辑连接词符号和量词符号的演算系统．它是一个根据事实反驳对科学理论进行修正的符号演算系统．文中以狭义相对论和生物进化论为例，使用R演算，对这两个科学理论的发现过程，在数理逻辑层面进行了验证．验证的结果表明：对Einstein时代的物理学而言，狭义相对论是唯一而且正确的选择．对Darwin时代的生物学而言，在接受自然选择原理等前提下，R演算可以推导出3种不同的，但逻辑上合理的进化论方案．Darwin提出的进化论是其中一种．有趣的是三者中的另一种，现在看来它具有一定的包容性．     

高阶时段演算及其完备性*

研究如何用时段演算来刻画程序的实时行为. 在实时程序设计里，程序变量被解释成时间的函数. 为了定义局部变量声明的语义，必须引进关于程序变量的量词.因此，建立高阶时段演算是必要的.首先建立了高阶时段演算理论，然后，用高阶时段演算去验证了一些程序的实时性质；最后，在假设所有程序变量均有穷可变的条件下，证明了高阶时段演算在抽象时间域上是完备的.     

π-演算观察等价的推理系统

提出带递归π－演算观察等价的推理系统，并证明了在受卫递归有穷控制子集上的完备性。该系统由推理规则和等式公理两部分组成，其断言采用条件等式的形式，直接刻画了进程项之间的符号互模拟关系。     

开互模拟的一条泛公理

π-演算公理化中较难处理的是有关局部化算子的等式, 传统的方法是使用带条件的推导规则或使用“区别”. 提出一条关于π-演算局部化算子的泛公理, 并证明它可在开互模拟的公理化中取代“区别”的作用. 本方法的好处是在公理化过程中我们只要处理一个互模拟, 而无须处理一族互模拟.     

移动进程的空间逻辑

提出了一个用于描述异步π-演算中移动进程的时态和空间性质的模态逻辑. 该逻辑具有基于谓词变量的递归构造. 建立了这一逻辑的语义理论, 并证明了语义的单调性, 从而保证了不动点的存在. 还设计了一个算法来自动地检测移动进程是否具有用该逻辑公式所描述的性质, 并证明了该算法的正确性.     

网格服务链模型的验证分析技术及应用

确保网格应用中大规模资源共享和复杂任务处理的正确性与可靠性是一项重要的工作．文中从形式化方法的角度出发，提出了基于状态Pi演算的网格服务链模型作为对网格中服务协作与组合进行建模和分析的理论工具．其中，状态Pi演算针对Web服务资源框架（WSRF）的思想，协调了系统状态与行为间的关系，扩展了Pi演算对系统状态的全生命周期管理能力．在此基础上，进一步结合了模型验证技术对网格服务链进行设计和运行时的逻辑性质分析．通过材料形变与断裂过程动态分析的网格应用案例，展示了采用上述方法对网格应用进行需求验证和可靠性分析的有效性．     

π-演算的符号迁移图及其早互模拟验证算法

提出符号迁移图作为π－演算进程直观而高效的表示模型，并给出了符号迁移图我种版本的早操作语义，在此基础上定义了相应版本的早互模拟和观察同余。同时引入了符号观察图和符号同余图以及τ－循环和τ－边消去定理。最后给出了关于强／弱早互模拟等价和早观察同余的符号验证算法，并证明了其正确性。     

适用于多种蕴涵算子的赋值空间上的测度与积分理论

对多种蕴涵算子导出的赋值空间进行统一处理,引入公用的Lebesgue测度,证明了相对于若干常见蕴涵算子而言,全体逻辑公式都是可测函数.建立了t(α重言式)理论,提出了一般的语义MP规则和一般的语义HS规则. 基于积分理论引入了逻辑公式的真度概念,提出了积分MP规则和积分HS规则.最后,通过通用逻辑度量空间概念在全体公式集上引入了伪距离,为近似推理提供了一种可能的框架.     

面向网构软件的环境显式化技术

网构化软件处于开放、动态、难控的环境之中，需能感知并适应环境的变化，以持续提供用户满意的服务．传统软件构造技术缺乏对环境感知和适应的系统支持．本文在前期工作基础上，提出一种面向网构软件的软件结构，通过为软件系统配备先验的环境模型和环境规约来实现环境处理的显式化．进而，介绍了我们使用这种方式来处理开放环境之分布异步性、感知信息的不一致性以及环境中人类用户行为特性等的若干具体技术进展．而后，讨论了一种先验环境模型及环境规约的开发方法原理，给出了相应的环境驱动逻辑的静态表达与运行实现机制．该方法和机制可较好地支持环境处理与应用业务逻辑间的关注分离．     

基于博弈论的开放环境下场景规约监控语义

在开放环境中,环境和系统本身行为的改变可能使得软件系统的实现不再满足原来规约,从而最终导致软件失效的发生.运行时监控是一种轻量级的形式化动态验证技术,已成为开放环境下检测软件失效的基本手段.针对基于场景的规约属性序列图,从博弈论的角度定义其多值监控语义:满足、无限可控、系统有限可控、系统紧急可控、环境有限可控、环境紧急可控和违例.通过多值监控语义的定义,监控器能够根据当前轨迹尽可能早地检测到系统失效或异常,并提供足够信息为失效的预防和恢复服务.实例研究表明了属性序列图多值监控语义的实用价值,并显示了其广泛的应用前景.     

Horn型推导关系

逻辑中的推导关系等同于公式之间的二元关系 ,刻画它所采用的证明规则等同于对这个二元关系所满足的条件的限制 .根据Gentzen证明论定义推导关系的方式定义一类推导关系 ,即Horn型推导关系 .应用模型论技巧 ,证明了这种推导关系并不能推广经典逻辑推导关系 .因而要定义扩充经典逻辑的非单调逻辑 ,必须在定义中采用“非”形式 .     

基于Schweizer-Sklar T-范数的模糊逻辑系统

基于Schweizer-SklarL范数，提出了一个新的模糊逻辑形式系统UL^＊证明了系统UL^＊的可靠性和完备性，并指出著名的SBL-系统是UL^＊的语义扩张，而IMTL△统是UL^＊当两个“非”运算重合时的特例．最后分析了UL^＊系统与其他模糊逻辑形式系统的关系，并从Yager的“与度”、Whalen的“模糊规则交互作用的强度”概念出发，说明了系统UL^＊中参数p的含义及其在近似推理中的应用。     

均一体系下庚烷着火和熄火的分析

以计算着火延迟时间为目的, 依据热力学理论, 推导了庚烷在均一体系中连续流动的控制体内的组分和温度的控制方程, 并用稳定状态法对庚烷的基元反应进行了计算. 稳定状态法的依据是, 在燃烧的快速化学反应过程中, 许多化学组分和基元反应处于瞬时稳态或部分平衡, 按照稳态求解反应速度和温度的微分方程, 计算将大为简化. 用稳定状态法得出了在连续流动控制体下的3个着火温度边界以及“S曲线”. 利用从1011种庚烷基元反应中得出的4步庚烷缩减反应机理, 所计算的着火延迟时间与实验结果非常吻合. 稳定状态法在计算庚烷的着火和熄火中大大缩减了计算成本, 为进行柴油发动机湍流燃烧的计算提供了一种简便方法.     

基于知识结构的认证协议验证

认知逻辑的Kripke语义,已被成功地运用到分析无黑客存在的安全网络下的通信协议.提出认知逻辑的Kripke语义的一种简单而自然的形式,称之为知识结构,并把这种语义用到分析黑客存在的非安全网络环境中的通信协议,特别是认证协议.与类BAN的那一类逻辑相比,文中的方法可以直接转化成算法实现,对协议本身进行操作,而不需对协议进行一些难以把握的抽象判断.而且,在这套理论的基础上开发了安全协议分析器SPV.文中的方法是基于证明的而不是证伪的,即证明协议的正确性而不是找协议漏洞.     

一种基于P/T网的低级并发程序验证模型

随着片上多处理器/多核技术的不断发展,采用机器级语言的并发程序(低级并发程序)有了更加广阔的应用前景.然而,低级并发程序的验证问题也成为程序语言领域一种新的挑战.并发程序安全性验证领域现有的工作多数是针对高级语言、规范或者演算,而针对机器级语言的甚少。这种情况的主要原因之一是缺少低级抽象模型.文中描述一种可验证的低级并发编程模型P-PMCC.P-PMCC程序是一个扩展的P/T网系统,其网结构用来刻画低级并发线程(原子的顺序汇编级代码)之间的并发关系.P-PMCC程序的验证采取模型检查和定理证明相结合的方法,分开考虑并发行为与顺序线程的规范和验证:前者借助于Petri网领域已有的方法,后者则借助现有的顺序程序的正确性证明方法。P-PMCC程序也可以看作并发程序的一种可验证的低级中间表示.     

马尔可夫逻辑网在信息抽取中的应用

提出了一个基于马尔可夫逻辑网的信息抽取方法,将所有记录的分割和记录去重在一个单独的整合推理过程中进行.由于采用马尔可夫逻辑和现有的推理算法,其主要工作是编写合适的逻辑公式,工程量比其他传统方法少得多.实验基于CiteSeer 和Cora这两个引文匹配数据集,其结果要明显优于之前的其他方法,同时也证明了马尔可夫逻辑网模型的精确性.     

非规则颗粒形态表征与离散元模拟方法研究

颗粒物质在自然界和人类生产与生活中广泛存在,对于非规则颗粒,其宏观物理力学特性与几何形态密切相关.本文以本课题组和合作者的相关研究为基础,介绍了非规则颗粒几何形态的获取、重构、评价、随机生成以及离散元模拟方法等方面的研究进展.总结了非规则颗粒形态不同获取方法的优缺点;将颗粒二维形态和三维形态分别划分为星形和非星形两种类型,介绍了各类型几何形态的计算几何重构方法;系统总结了非规则颗粒不同层次形态评价指标的定义,及基于计算几何的指标计算方法;介绍了基于逆蒙特卡罗法的二维星形与三维星形随机颗粒生成方法,以及可考虑一阶系数固有关系和其他阶系数经验相关性的二维非星形与三维非星形虚拟颗粒生成方法;对于非规则颗粒的离散元模拟方法,重点总结了颗粒几何形态表示、颗粒接触判断与颗粒接触力计算方法等核心问题的研究进展.     

语义Web的逻辑基础

分析了目前语义Web理论的研究现状和存在的问题, 分析了用传统描述逻辑作为语义Web逻辑基础的不充分性, 根据语义Web的特点和需求, 提出了一种新的动态描述逻辑DDL, 该DDL将静态知识和动态知识表示与推理有机地整合在一起. 特别的是, 给出了具体的动作描述方法, 并按照传统描述逻辑的语义解释方法给出了动作的语义解释, 从而该DDL形成了一种能同时处理静态知识和动态知识的统一的形式化逻辑框架. 该DDL具有清晰的语义特征, 既提供了可判定的推理服务, 又能有效地对静态知识、动态过程和运行机制进行表示和推理(动作的可实现性和动作之间的包含关系), 因此, 提出的动态描述逻辑DDL可以为语义Web提供合理的逻辑基础, 弥补了传统描述逻辑作为语义Web逻辑基础的不足.     

梯级水电站群长期发电优化调度多核并行随机动态规划方法

随机动态规划求解水电站群长期发电优化调度易产生"维数灾"问题,导致计算耗时急剧增加,求解效率降低.如何缓解维数灾和提高计算效率,一直是水库优化调度致力于研究的难点问题.在随机动态规划的并行性分析基础上,提出了基于Fork/Join并行框架的多核并行随机动态规划方法.该方法将单个时段内所有变量组合状态下的计算任务作为父任务,通过分治法递归分解为多个子任务,并平均分配到不同的内核同时计算实现细粒度并行求解.以澜沧江下游梯级水电站群为研究实例,建立了3个变量离散数不同的调度方案,并在多核环境下验证该方法的计算效率.结果表明,在2和4核环境下,该方法的计算耗时与串行方法相比,分别节省了约50%和70%,大幅度缩减计算耗时,可充分利用多核资源;同时,计算任务的规模越大,并行计算的耗时缩减幅度越大.因此,此方法为大规模水电系统优化调度提供了一种可行途径,其并行原理可为其他应用所借鉴.     

基于忆阻器实现多样化STDP学习规则的突触电路设计

忆阻器作为一种具有记忆效应的非线性电路元件,它受到电流刺激后的电导变化与人脑中神经突触的权重变化类似,可用于模拟人脑学习、记忆过程中的突触行为.本文提出了一种基于忆阻器所搭建的突触电路,包含了由运放、逻辑门、模拟开关等器件构成的增强模块和抑制模块,以及由忆阻器和模拟开关构成的忆阻突触模块.通过对增强和抑制模块输入直流脉冲对来模拟生物突触受到前后神经元的刺激.通过调节前后脉冲输入信号的时间差,发现输入信号间隔越短,忆阻器电导幅值变化越大,这与生物突触的STDP (spike-time-dependent-plasticity)学习曲线变化一致;为了实现突触模拟的多样性,本文进一步地构建了忆阻突触模块的四种替换电路,每种替换电路可对应模拟不同的学习规则.由此,完成了生物突触多样化STDP学习规则的模拟,解决了突触电路研究中模拟种类单一、输入条件苛刻等问题,有望运用于未来神经形态芯片的研制中.