模型检验是硬件和软件形式化验证最成功的技术之一.目前大部分的模型检验技术是基于状态的而不考虑迁移上的操作和事件.这导致模型检验在验证使用事件进行交互的组件系统中面临新的困难,因此需要新的规约技术对状态事件系统进行规约.状...模型检验是硬件和软件形式化验证最成功的技术之一.目前大部分的模型检验技术是基于状态的而不考虑迁移上的操作和事件.这导致模型检验在验证使用事件进行交互的组件系统中面临新的困难,因此需要新的规约技术对状态事件系统进行规约.状态事件线性时序逻辑(State/Event Linear Temporal Logic,SE-LTL)给出了一种简洁和直接的方式表达包含状态和事件的系统属性.在SE-LTL中,状态和事件都可以作为原子命题.基于自动机理论的线性时序逻辑(Linear Temporal Logic,LTL)模型检验可以被用来对SE-LTL属性进行验证.然而SE-LTL属性在经典的stutter等价(stutter-equivalent)下无法保持,所以最有效的并发程序状态约简技术:偏序约简技术(Partial Order Reduction,POR)不能直接应用于SE-LTL的验证.该文提出一种新的方法利用已有的偏序约简技术对SE-LTL验证过程的状态空间进行约简.该方法分为两个部分:第一个部分是针对SE-LTL不带NEXT算子的约简方法;第二部分则是带NEXT算子的约简方法.第一部分的主要思想是从一个Büchi自动机(Automata,BA)中抽取出“状态部分”.“状态部分”的含义是该部分只与系统的状态相关.基于“状态部分”,给出关于BA和标签Kripke结构(Labeled Kripke Structure)的同步乘,并在同步乘的构造过程中嵌入偏序约简技术,从而约简同步乘的状态空间,即该文的约简技术是on-the-fly的.嵌入的偏序约简在已有的偏序约简基础上,面向SE-LTL公式中的事件引入新的可见操作的识别方法.为了能够将偏序约简技术应用到所有的SE-LTL公式,该文同时给出验证SE-LTL带NEXT算子的偏序约简算法.NEXT算子是偏序约简的另一个主要障碍.该部分是文中的第二部分工作.该部分的技术依然是on-the-fly的,并且需要与状态部分的识别相结合.通过将该文技术实现到SPIN模型检验器中对已有的模型进行验证.Spin是针对LTL的并发程序模型检验器.实现部分包括SE-LTL到BA的转化,以及on-the-fly的模型验证过程.实验的过程主要针对三个模型集:生产消费者模型,哲学家就餐问题以及公共对象请求代理体系结构中的GIOP协议.验证结果表明,对比完全基于状态的模型检验和不带偏序约简的状态事件模型检验,该文的方法具有更好的效率,并且能够被应用于状态事件系统,特别是安全有关嵌入式系统的验证.展开更多
事件时序关系抽取是一项重要的自然语言理解任务,可以广泛应用于诸如知识图谱构建、问答系统等任务.已有事件时序关系抽取方法往往将该任务视为句子级事件对的分类问题,而基于有限的局部句子信息导致其抽取的事件时序关系的精度较低,且...事件时序关系抽取是一项重要的自然语言理解任务,可以广泛应用于诸如知识图谱构建、问答系统等任务.已有事件时序关系抽取方法往往将该任务视为句子级事件对的分类问题,而基于有限的局部句子信息导致其抽取的事件时序关系的精度较低,且无法保证整体时序关系的全局一致性.针对此问题,提出一种融合上下文信息的篇章级事件时序关系抽取方法,使用基于双向长短期记忆(bidirectional long short-term memory,Bi-LSTM)的神经网络模型学习文章中事件对的时序关系表示,再利用自注意力机制融入上下文中其他事件对信息,从而得到更丰富的事件对时序关系表示用于时序关系分类.通过TB-Dense(timebank dense)和MATRES(multi-axis temporal relations for start-points)数据集的实验表明:此方法能够取得比当前主流的句子级方法更佳的抽取效果.展开更多
事件时序关系识别有助于读者理清文章脉络,把握全局发展趋势,是重要的自然语言理解任务之一。现有的事件时序关系识别方法专注于提取事件触发词前后的局部信息,然而事件句中的事件信息分布较为分散,导致模型在编码过程中丢失部分事件信...事件时序关系识别有助于读者理清文章脉络,把握全局发展趋势,是重要的自然语言理解任务之一。现有的事件时序关系识别方法专注于提取事件触发词前后的局部信息,然而事件句中的事件信息分布较为分散,导致模型在编码过程中丢失部分事件信息。针对上述问题,针对文本特征提出一种双路依存注意力机制来聚合事件句信息,通过单词的父子节点信息构建出双路依存矩阵,将句法信息融入到词嵌入中。将该机制与双向长短期记忆网络(bidirectional long short term memory,Bi-LSTM)结合,可以使事件时序关系模型的性能得到显著提高。该文在越南语数据集与英语数据集上进行对比实验,结果表明所提方法优于主流的神经网络方法。展开更多
现有事件时序关系识别方法缺少句法信息的加入,导致模型对事件的理解能力不足。事件依存路径作为分析事件时序关系的重要手段,能够指导模型理解文本结构。为生成包含事件句语义与句法的文本表征,提出一种融入事件依存路径的事件时序关...现有事件时序关系识别方法缺少句法信息的加入,导致模型对事件的理解能力不足。事件依存路径作为分析事件时序关系的重要手段,能够指导模型理解文本结构。为生成包含事件句语义与句法的文本表征,提出一种融入事件依存路径的事件时序关系识别方法,将事件的最短依存句法以外部知识的形式融入到事件编码中。此外,为了将文本语义与句法信息有效地融合,先将事件的最短依存路径转换为句法模板,然后将句法模板拼接到事件句文本中,基于自注意力机制与双向长短期记忆网络(Bi-directional Long Short-Term Memory,Bi-LSTM)结构编码事件不同特征,最后提出使用门控机制计算事件时序特征。在TimeBank-Dense数据集上进行实验,实验结果证明了所提方法的有效性。展开更多
话题跟踪是一项针对新闻话题进行相关信息识别、挖掘和自组织的研究课题,其关键问题之一是如何建立符合话题形态的统计模型.话题形态的研究涉及两个问题,其一是话题的结构特性,其二是话题变形.对比分析了现有词包式、层次树式和链式这3...话题跟踪是一项针对新闻话题进行相关信息识别、挖掘和自组织的研究课题,其关键问题之一是如何建立符合话题形态的统计模型.话题形态的研究涉及两个问题,其一是话题的结构特性,其二是话题变形.对比分析了现有词包式、层次树式和链式这3类主流话题模型的形态特征,尤其深入探讨了静态和动态话题模型拟合话题脉络的优势和劣势,并提出一种基于特征重叠比的核捕捉衰减评价策略,专门用于衡量静态和动态话题模型追踪话题发展趋势的能力.在此基础上,分别给出突发式增量式学习方法和时序事件链的更新算法,借以提高动态话题模型的核捕捉性能.实验基于国际标准评测语料TDT4,采用NIST(National Institute of Standards and Technology)提出的最小检测错误权衡系数评测法,并结合所提出的核捕捉衰减评价方法,对各类主要话题模型进行测试.实验结果显示,结构化的动态话题模型具有最佳的跟踪性能,且突发式增量式学习和时序事件链的更新算法分别给予动态话题模型0.4%和3.3%的性能改进.展开更多
Aiming at the industry cyber-physical system(ICPS)where Denial-of-Service(DoS)attacks and actuator failure coexist,the integrated security control problem of ICPS under multi-objective constraints was studied.First,fr...Aiming at the industry cyber-physical system(ICPS)where Denial-of-Service(DoS)attacks and actuator failure coexist,the integrated security control problem of ICPS under multi-objective constraints was studied.First,from the perspective of the defender,according to the differential impact of the system under DoS attacks of different energies,the DoS attacks energy grading detection standard was formulated,and the ICPS comprehensive security control framework was constructed.Secondly,a security transmission strategy based on event triggering was designed.Under the DoS attack energy classification detection mechanism,for large-energy attacks,the method based on time series analysis was considered to predict and compensate for lost data.Therefore,on the basis of passive and elastic response to small energy attacks,the active defense capability against DoS attacks was increased.Then by introducing the conecomplement linearization algorithm,the calculation methods of the state and fault estimation observer and the integrated safety controller were deduced,the goal of DoS attack active and passive hybrid intrusion tolerance and actuator failure active fault tolerance were realized.Finally,a simulation example of a four-capacity water tank system was given to verify the validity of the obtained conclusions.展开更多
文摘模型检验是硬件和软件形式化验证最成功的技术之一.目前大部分的模型检验技术是基于状态的而不考虑迁移上的操作和事件.这导致模型检验在验证使用事件进行交互的组件系统中面临新的困难,因此需要新的规约技术对状态事件系统进行规约.状态事件线性时序逻辑(State/Event Linear Temporal Logic,SE-LTL)给出了一种简洁和直接的方式表达包含状态和事件的系统属性.在SE-LTL中,状态和事件都可以作为原子命题.基于自动机理论的线性时序逻辑(Linear Temporal Logic,LTL)模型检验可以被用来对SE-LTL属性进行验证.然而SE-LTL属性在经典的stutter等价(stutter-equivalent)下无法保持,所以最有效的并发程序状态约简技术:偏序约简技术(Partial Order Reduction,POR)不能直接应用于SE-LTL的验证.该文提出一种新的方法利用已有的偏序约简技术对SE-LTL验证过程的状态空间进行约简.该方法分为两个部分:第一个部分是针对SE-LTL不带NEXT算子的约简方法;第二部分则是带NEXT算子的约简方法.第一部分的主要思想是从一个Büchi自动机(Automata,BA)中抽取出“状态部分”.“状态部分”的含义是该部分只与系统的状态相关.基于“状态部分”,给出关于BA和标签Kripke结构(Labeled Kripke Structure)的同步乘,并在同步乘的构造过程中嵌入偏序约简技术,从而约简同步乘的状态空间,即该文的约简技术是on-the-fly的.嵌入的偏序约简在已有的偏序约简基础上,面向SE-LTL公式中的事件引入新的可见操作的识别方法.为了能够将偏序约简技术应用到所有的SE-LTL公式,该文同时给出验证SE-LTL带NEXT算子的偏序约简算法.NEXT算子是偏序约简的另一个主要障碍.该部分是文中的第二部分工作.该部分的技术依然是on-the-fly的,并且需要与状态部分的识别相结合.通过将该文技术实现到SPIN模型检验器中对已有的模型进行验证.Spin是针对LTL的并发程序模型检验器.实现部分包括SE-LTL到BA的转化,以及on-the-fly的模型验证过程.实验的过程主要针对三个模型集:生产消费者模型,哲学家就餐问题以及公共对象请求代理体系结构中的GIOP协议.验证结果表明,对比完全基于状态的模型检验和不带偏序约简的状态事件模型检验,该文的方法具有更好的效率,并且能够被应用于状态事件系统,特别是安全有关嵌入式系统的验证.
文摘事件时序关系抽取是一项重要的自然语言理解任务,可以广泛应用于诸如知识图谱构建、问答系统等任务.已有事件时序关系抽取方法往往将该任务视为句子级事件对的分类问题,而基于有限的局部句子信息导致其抽取的事件时序关系的精度较低,且无法保证整体时序关系的全局一致性.针对此问题,提出一种融合上下文信息的篇章级事件时序关系抽取方法,使用基于双向长短期记忆(bidirectional long short-term memory,Bi-LSTM)的神经网络模型学习文章中事件对的时序关系表示,再利用自注意力机制融入上下文中其他事件对信息,从而得到更丰富的事件对时序关系表示用于时序关系分类.通过TB-Dense(timebank dense)和MATRES(multi-axis temporal relations for start-points)数据集的实验表明:此方法能够取得比当前主流的句子级方法更佳的抽取效果.
文摘事件时序关系识别有助于读者理清文章脉络,把握全局发展趋势,是重要的自然语言理解任务之一。现有的事件时序关系识别方法专注于提取事件触发词前后的局部信息,然而事件句中的事件信息分布较为分散,导致模型在编码过程中丢失部分事件信息。针对上述问题,针对文本特征提出一种双路依存注意力机制来聚合事件句信息,通过单词的父子节点信息构建出双路依存矩阵,将句法信息融入到词嵌入中。将该机制与双向长短期记忆网络(bidirectional long short term memory,Bi-LSTM)结合,可以使事件时序关系模型的性能得到显著提高。该文在越南语数据集与英语数据集上进行对比实验,结果表明所提方法优于主流的神经网络方法。
文摘现有事件时序关系识别方法缺少句法信息的加入,导致模型对事件的理解能力不足。事件依存路径作为分析事件时序关系的重要手段,能够指导模型理解文本结构。为生成包含事件句语义与句法的文本表征,提出一种融入事件依存路径的事件时序关系识别方法,将事件的最短依存句法以外部知识的形式融入到事件编码中。此外,为了将文本语义与句法信息有效地融合,先将事件的最短依存路径转换为句法模板,然后将句法模板拼接到事件句文本中,基于自注意力机制与双向长短期记忆网络(Bi-directional Long Short-Term Memory,Bi-LSTM)结构编码事件不同特征,最后提出使用门控机制计算事件时序特征。在TimeBank-Dense数据集上进行实验,实验结果证明了所提方法的有效性。
文摘话题跟踪是一项针对新闻话题进行相关信息识别、挖掘和自组织的研究课题,其关键问题之一是如何建立符合话题形态的统计模型.话题形态的研究涉及两个问题,其一是话题的结构特性,其二是话题变形.对比分析了现有词包式、层次树式和链式这3类主流话题模型的形态特征,尤其深入探讨了静态和动态话题模型拟合话题脉络的优势和劣势,并提出一种基于特征重叠比的核捕捉衰减评价策略,专门用于衡量静态和动态话题模型追踪话题发展趋势的能力.在此基础上,分别给出突发式增量式学习方法和时序事件链的更新算法,借以提高动态话题模型的核捕捉性能.实验基于国际标准评测语料TDT4,采用NIST(National Institute of Standards and Technology)提出的最小检测错误权衡系数评测法,并结合所提出的核捕捉衰减评价方法,对各类主要话题模型进行测试.实验结果显示,结构化的动态话题模型具有最佳的跟踪性能,且突发式增量式学习和时序事件链的更新算法分别给予动态话题模型0.4%和3.3%的性能改进.
基金supported by Gansu Higher Education Innovation Fund Project(No.2023B-439)。
文摘Aiming at the industry cyber-physical system(ICPS)where Denial-of-Service(DoS)attacks and actuator failure coexist,the integrated security control problem of ICPS under multi-objective constraints was studied.First,from the perspective of the defender,according to the differential impact of the system under DoS attacks of different energies,the DoS attacks energy grading detection standard was formulated,and the ICPS comprehensive security control framework was constructed.Secondly,a security transmission strategy based on event triggering was designed.Under the DoS attack energy classification detection mechanism,for large-energy attacks,the method based on time series analysis was considered to predict and compensate for lost data.Therefore,on the basis of passive and elastic response to small energy attacks,the active defense capability against DoS attacks was increased.Then by introducing the conecomplement linearization algorithm,the calculation methods of the state and fault estimation observer and the integrated safety controller were deduced,the goal of DoS attack active and passive hybrid intrusion tolerance and actuator failure active fault tolerance were realized.Finally,a simulation example of a four-capacity water tank system was given to verify the validity of the obtained conclusions.
