利用自动机研究描述逻辑的推理问题

首先介绍如何把描述逻辑转化为一个不确定型有穷自动机,分析这种转化过程中存在的问题,在B．Nebel的基础上提出了利用自动机的最小化理论对上述得到的自动机进行优化处理,以提高推理的效率。     

AVS视频解码的错误检测与掩盖方法

研究了视频误码的语法/语义检测、相关性检测方法和错误掩盖方法,分析了AVS的技术特性。在此基础上提出了一种基于AVS的错误两步检测法和基于图像编码帧类型(I,P,B)的自适应错误掩盖方法。实验结果表明,两步检测法能对AVS码流中的错误进行准确定位,自适应错误掩盖方法对图像的恢复效果显著。同时该方法不中断解码器,不影响解码器的实时解码速度。     

Web服务自动语义标注的本体定位方法研究

面向服务架构中,分布式网络计算的实现依赖于服务交互问题的有效解决。为此,服务接口必须采用机器可理解的方式描述,从而为服务的动态发现和组合提供底层支持。服务语义标注技术满足了上述需求,它是指通过共享域本体中机器可理解的元数据表示服务元素。本文将服务语义标注过程分解为域标注和概念标注两个阶段,重点针对域标注注问题,并提出了一种基于机器学习的域标注算法,对实际服务的标注实验验证了该算法的有效性     

Modalities in linear logic weaker than the exponential “of course”: Algebraic and relational semantics

We present a semantic study of a family of modal intuitionistic linear systems, providing various logics with both an algebraic semantics and a relational semantics, to obtain completeness results. We call modality a unary operator on formulas which satisfies only one rale (regularity), and we consider any subsetW of a list of axioms which defines the exponential of course of linear logic. We define an algebraic semantics by interpreting the modality as a unary operation on an IL-algebra. Then we introduce a relational semantics based on pretopologies with an additional binary relationr between information states. The interpretation of is defined in a suitable way, which differs from the traditional one in classical modal logic. We prove that such models provide a complete semantics for our minimal modal system, as well as, by requiring the suitable conditions onr (in the spirit of correspondence theory), for any of its extensions axiomatized by any subsetW as above. We also prove an embedding theorem for modal IL-algebras into complete ones and, after introducing the notion of general frame, we apply it to obtain a duality between general frames and modal IL-algebras.     

NETMET: A program for generating and interpreting metaphors

Metaphors have computable semantics. A program called NETMET both generates metaphors and produces partial literal interpretations of metaphors. NETMET is based on Kittay's semantic field theory of metaphor and Black's interaction theory of metaphor. Input to NETMET consists of a list of literal propositions. NETMET creates metaphors by finding topic and source semantic fields, producing an analogical map from source to topic, then generating utterances in which terms in the source are identified with or predicated of terms in the topic. Given a metaphor, NETMET utilizes if-then rules to generate the implication complex of that metaphor. The literal leaves of the implication complex comprise a partial literal interpretation.Eric Steinhart has an MA in philosophy (Boston College) and completed his PhD dissertation (Formal Semantics for Metaphors) at SUNY at Stony Brook. He has written on technology, analogy, metaphor and idealism. His publications include Beyond the Proportional Analogy: A Structural Model of AnalogyPragmatics and Cognition, 2, 1 (1994). He is interested in the application of computational methods to philosophical topics and is working on a computational model of idealistic metaphysics.     

基于多视角的多类型错误全面检测方法

随着信息化社会的发展,数据的规模越发庞大,数据的种类也越发丰富.时至今日,数据已经成为国家和企业的重要战略资源,是科学化管理的重要保障.然而,随着社会生活产生的数据日益丰富,大量的脏数据也随之而来,数据质量问题油然而生.如何准确而全面地检测出数据集中所包含的错误数据,一直是数据科学中的痛点问题.尽管已有许多传统方法被广泛用于各行各业,如基于约束与统计的检测方法,但这些方法通常需要丰富的先验知识与昂贵的人力和时间成本.受限于此,这些方法往往难以准确而全面地检测数据.近年来,许多新型错误检测方法利用深度学习技术,通过时序推断、文本解析等方式取得了更好检测效果,但它们通常只适用于特定的领域或特定的错误类型,面对现实生活中的复杂情况,泛用性不足.基于上述情况,结合传统方法与深度学习技术的优点,提出了一个基于多视角的多类型错误全面检测模型CEDM.首先,从模式的角度,结合现有约束条件,在属性、单元和元组层面进行多维度的统计分析,构建出基础检测规则;然后,通过词嵌入捕获数据语义,从语义的角度分析属性相关性、单元关联性与元组相似性,进而基于语义关系,从多个维度上更新、扩展基础规则;最终,联合多个视角...     

自动驾驶交叉路口测试场景建模及验证方法

自动驾驶汽车在缓解交通拥堵和消除交通事故方面发挥着重要作用.为了保证自动驾驶系统的安全性和可靠性,在自动驾驶汽车部署到公共道路之前,必须进行全面的测试.现有的测试场景数据大多来源于交通事故和交通违法场景,而且自动驾驶系统最基本的安全需求就是遵守交通法规,这充分体现了自动驾驶汽车遵守交通规则的重要性.然而,目前严重缺少针对交通法规构建的自动驾驶测试场景.因此,本文从交通法规出发,根据自动驾驶系统安全需求,提出交叉路口测试场景的Petri网建模及形式化验证方法.首先,依据自动驾驶测试场景对交规进行分类,提取适合自动驾驶汽车的文本交规,并进行半形式化表征.其次,以覆盖道路交通安全法规以及测试场景功能测试规程为目标,融合交叉路口场景要素的交互行为,合理选择并组合测试场景要素,布设交叉路口测试场景.然后,基于交规的测试场景被建模为一个Petri网,其中,库所描述自动驾驶汽车的状态,变迁表示状态的触发条件,并选择时钟约束规范语言（CCSL）作为中间语义语言,将Petri网转换为一个可进行形式化验证的中间语义模型,提出具体的转换方法.最后,通过Tina软件分析验证交规场景模型的活性、有界性和可达性,结果表明所建模型的正确性,并基于SMT的分析工具MyCCSL来分析CCSL约束,采用LTL公式以形式化方法验证交规场景模型的一致性.     

基于SMT的区域控制器同步反应式模型的形式化验证

在安全关键系统的软件开发过程中,形式化验证是一种经检验的提高软件质量的技术.然而,无论从理论上还是从应用角度来看,软件的验证都必须是完整的,数据流验证应该是对实现层软件模型进行验证的必要体现.因此,环境输入、泛型函数、高阶迭代运算和中间变量对于分析形式化验证的可用性至关重要.为了验证同步反应式模型,工程师很容易验证控制流模型(即安全状态机).现有工作表明,这类工作无法全面地验证安全关键系统的同步反应式模型,尤其是数据流模型,导致这些方法没有达到工业应用的要求,这成为对工业安全软件进行形式化验证的一个挑战.提出了一种自动化验证方法.该方法可以实现对安全状态机和数据流模型的集成进行验证.采用了一种基于程序综合的方法,其中,SCADE模型描述了功能需求、安全性质和环境输入,可以通过对Lustre模型的程序综合,采用基于SMT的模型检查器进行验证.该技术将程序合成作为一种通用原理来提高形式化验证的完整性.在轨道交通的工业级应用(近200万行Lustre代码)上评估了该方法.实验结果表明,该方法在大规模同步反应式模型长期存在的复杂验证问题上是有效的.     

基于实时视频感知的虚拟体育交互系统

针对疫情常态化背景下,传统体育项目受场地、器材等限制,市场上相关产品价格昂贵、可扩展性不足等问题,提出了一种基于实时视频感知的虚拟体育交互系统.该系统设计视频数据采集模块和人体关节点提取模块,结合OpenPose获取人体的关节点坐标,实时捕捉人体手势以及肢体动作.动作语义理解模块包括运动动作理解和绘图动作理解.前者根据运动中肢体关节点的相对位置关系,识别运动动作语义.后者将手腕部关节点绘图动作轨迹生成为草图图像,使用AlexNet进行识别分类,解析为对应的绘制动作语义.该模型在边缘端设备的分类准确率为98.83%.采用基于Unity设计的草图游戏应用作为可视化交互界面,实现在虚拟场景中的运动交互.该系统使用实时视频感知交互方式实现居家运动健身,无需其他的外部设备,具有更强的参与度和趣味性.