命令式语言的高阶Action演算表示

Action演算簇（action calculi)是一种抽象的数学结构,已经表明它可以表示λ演算,进程代数,γ演算以及函数式语言等。作为Action演算族的进一步应用,针对一个典型的顺序命令式语言SIL,充分利用Action演算的可扩充性,定义了一个具体的Action演算AC（KSIL）,同时为了给出循环计算的表示引入了高阶性,给出了SIL的AC（KSIL）,语义,并证明了SIL的操作语义与AC（KSIL）语义之间的对应关系,最后讨论了顺序机制的控制及其控制规则定义方法,不仅表明Action演算可以方便地表示顺序计算,而且也证明了Action演算强大的描述能力。     

λ演算中的第二不动点定理*

作者研究λ演算中的第二不动点的性质．首先讨论关于第二不动点的3个命题之间的关系且证明了它们．然后为第二不动点组合子给以一个充分条件且作出一系列的第二不动点组合子．作者还提出和证明了多元第二不动点定理．     

有效的ν支持向量回归机的ν解路径算法

由Sch lkopf等人提出的v支持向量回归机具有通过参数控制支持向量和错误向量个数的优点,然而与标准的支持向量机相比,其形式更为复杂,迄今为止仍没有有效的算法计算v解路径.基于支持向量回归机的修改形式,提出了一种新的解路径算法,它能够追踪参数v对应的所有解,并通过理论分析和实验,说明了该算法能够尽可能地避免不可行的更新路径,并在有限步内拟合出所有的解路径.     

算子Fuzzy逻辑中的λ—蕴涵和λ—强蕴涵

在本文中,我们引进了算子模糊逻辑中的λ-蕴涵和λ-强蕴涵的概念,λ-逻辑结果和λ-弱逻辑结果的概念。证明了两子句的的λ-归结式是这两个子句的λ-逻辑结果,从而完成了λ-归结的完备性定理的证明。     

基于网络演算的簇树WSN性能上界分析

为保证WSN的服务质量(QoS),需精确求解其性能上界。对进入WSN节点的数据流进行漏桶管制,节点为数据流提供基于速率-延迟模型的服务保障,在已有簇状拓扑WSN性能模型研究基础上,利用确定性网络演算理论推导簇树WSN节点的有效带宽、缓冲区队列长度上界和数据流端到端延迟上界。     

无线传感器网络中(ε,δ)-近似聚集算法

提出了一种基于Bernoulli抽样的近似聚集算法,以满足无线传感器网络(简称WSN)中用户给定的任意精度需求.同时,还提出了两种样本数据的自适应算法,分别用于处理用户的精确度需求以及网络中的感知数据发生变化的情况.理论分析及实验结果表明,所提出的算法在近似结果的精确度、能量开销等方面均优于已有的近似聚集算法.     

基于流演算的多Agent请求/服务协作模型的研究

为了刻画多Agent环境中的交互特性,基于流演算理论和GoFlux语言,吸收了ConGolog语义,提出了CFlux语言。CFlux语言能有效地处理MAS中的For循环、并发、优先级并发、中断等操作,从而可以实现多Agent程序的并发交互执行。在此基础上,基于CFlux和一组通信动作提出一个请求/服务协作模型。最后,通过一个智能日程安排实例表明了上述理论。     

一种从面向对象Z规约到代码的精化演算方法

COOZ(complete object-oriented Z)的优势在于精确描述大型程序的规约.COOZ本身的结构 不支持精化演算,这限制了COOZ的应用能力,使COOZ难以作为完整的方法应用于软件的开发. 将精化演算引入COOZ,弥补了COOZ在设计和实现阶段的不足,同时也消除了规约与实现之间在 结构和表示方法上的完全分离,使程序开发在一个完整的框架下平滑进行.该文提出了基于CO OZ和精化演算的软件开发模型,通过实例讨论了数据精化和操作精化问题.在精化演算实现技 术方面构造了一种数据精化算子,提出一     

具有模态词□φ=□1V□2φ且可靠与完备的公理系统

提出具有模态词□φ=□₁V□₂φ的命题模态逻辑,给出其语言、语法与语义,其公理化系统是可靠与完备的,其中,□₁与□₂是给定的模态词.该逻辑的公理化系统具有与公理系统S5相似的语言,但具有不同的语法与语义.对于任意的公式φ,□φ=□₁V□₂φ;框架定义为三元组W,R₁,R₂,模型定义为四元组W,R₁,R₂,I;在完备性定理证明过程中,需要在由所有极大协调集所构成的集合上构造出两个等价关系,其典型模型的构建方法与经典典型模型的构建方法不同.如果□₁的可达关系R₁等于□₂的可达关系R₂,那么该逻辑的公理化系统变成S5.     

MDA中从PIM到PSM的模型转换

基于在MDA中PIM到PSM的模型转换实现,提出了用UML描述PIM的一种有效性补充(E-)LOTOS,试图达到在模型映射前实现对模型的有效逻辑验证;对模型转换的基础理论进行了探索,分析了目前在MDA中实现从PIM到PSM模型转换的主要途径和困难;最后展望了模型转换的实现前景。     

Taking Decisions Late: End-Based Choice Combined with Action Refinement

A choice in concurrent systems is usually taken by the starting of an action. We propose the alternative view that a choice is determined by the ending of actions as this alternative has relevant applications and interesting implications. The different points of view lead in particular to different refinement operators.We introduce a refinement operator on bundle event structures for the end-based view. The standard equivalences are not preserved by this refinement operator. Therefore, we also introduce and study new equivalences that are preserved by our refinement operator.     

汉英机器翻译中格式转换研究

格式在HNC理论中是指广义作用句各主语块位置的不同排列组合方式。由于主语块的排列方式在汉英两种语言中表达的差异,汉语句子翻译到英语时常常发生格式转换。格式转换是HNC机器翻译理论的一个重要内容,是机器翻译理论实践的基础和前提。以HNC机器翻译理论为指导,以真实文本的专利文献汉英句对为分析对象,研究专利机器翻译中汉英两种语言之间广义作用句的格式转换规律,制定了排除规则、识别规则和转换规则,对部分规则进行了人工评测,结果表明准确率能达到85%左右。     

面部运动单元检测研究综述

面部运动单元检测旨在让计算机从给定的人脸图像或视频中自动检测需要关注的运动单元目标。经过二十多年的研究,尤其是近年来越来越多的面部运动单元数据库的建立和深度学习的兴起,面部运动单元检测技术发展迅速。首先,阐述了面部运动单元的基本概念,介绍了已有的常用面部运动单元检测数据库,概括了包括预处理、特征提取、分类器学习等步骤在内的传统检测方法;然后针对区域学习、面部运动单元关联学习、弱监督学习等几个关键研究方向进行了系统性的回顾梳理与分析;最后讨论了目前面部运动单元检测研究存在的不足以及未来潜在的发展方向。     

弱监督与少样本学习场景下视频行为识别综述

近年来各类人体行为识别算法利用大量标记数据进行训练,取得了良好的识别精度。但在实际应用中,数据的获取以及标注过程都是非常耗时耗力的,这限制了算法的实际落地。针对弱监督及少样本场景下的视频行为识别深度学习方法进行综述。首先,在弱监督情况下,分类总结了半监督行为识别方法和无监督领域自适应下的视频行为识别方法;然后,对少样本场景下的视频行为识别算法进行详细综述;接着,总结了当前相关的人体行为识别数据集,并在该数据集上对各相关视频行为识别算法性能进行分析比较;最后,进行概括总结,并展望人体行为识别的未来发展方向。     

Strong normalization proofs by CPS-translations

This paper proposes a new proof method for strong normalization of classical natural deduction and calculi with control operators. For this purpose, we introduce a new CPS-translation, continuation and garbage passing style (CGPS ) translation. We show that this CGPS-translation method gives simple proofs of strong normalization of λμ_→∧∨⊥, which is introduced in [P. de Groote, Strong normalization of classical natural deduction with disjunction, in: S. Abramsky (Ed.), Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, in: Lecture Notes in Comput. Sci., vol. 2044, Springer, Berlin, 2001, pp. 182-196] by de Groote and corresponds to the classical natural deduction with disjunctions and permutative conversions.     

分布式元组空间协同模型的设计与描述

元组空间是一种结构化的分布式共享存储编程方式,使用一个共享的元组空间进行生成式通信。该文针对集中式元组空间的性能瓶颈、单点失效问题及可扩展性差等不足,提出一种混合式的分布式元组空间的体系架构,给出基于π-演算的分布计算演算模型,并对模型的语法和操作语义进行讨论,通过钩互模拟给出了系统的性质。