期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
共找到65篇文章
< 1 2 … 4 >
每页显示 20 50 100
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
显示方式：
基于注意力机制的信息预处理多智能体强化学习算法
1
作者 杜泳韬 赵岭忠 翟仲毅 《国外电子测量技术》 2024年第3期91-97,共7页
多智能体强化学习在群体控制领域具有广泛应用,然而传统的强化学习方法(如Q-Learning或策略梯度)在多智能体环境中表现不佳。在训练过程中,每个智能体的策略不断变化。当一个智能体基于环境信息做出决策时,其他智能体的决策可能已经影... 多智能体强化学习在群体控制领域具有广泛应用,然而传统的强化学习方法(如Q-Learning或策略梯度)在多智能体环境中表现不佳。在训练过程中,每个智能体的策略不断变化。当一个智能体基于环境信息做出决策时,其他智能体的决策可能已经影响了环境信息,导致智能体感知的转移概率分布和奖赏函数发生变化,使得环境变得非平稳,训练无法有效进行。为了缓解这一问题,研究了一种基于多头自注意力的多智能体强化学习算法。该方法考虑了其他智能体的行动策略,利用多头自注意力算法使智能体能够学习对决策影响最大的因素,成功地学习了复杂的多智能体协调策略。在实验结果中平均回报达值到了0.82,远高于传统算法的表现。实验结果表明,所提出的基于多头自注意力的多智能体强化学习算法能够有效解决环境不平稳导致的多智能体学习困难问题,提高了多智能体强化学习算法的收敛速度和平稳性。 展开更多
关键词 多智能体强化学习 多头自注意力 信息预处理:策略梯度:非平稳
原文传递
从经典逻辑知识构建ASP知识库的新方法 被引量：6
2
作者 赵岭忠 王雪松 +1 位作者 钱俊彦 蔡国永 《计算机应用》 CSCD 北大核心 2010年第11期2932-2936,共5页
回答集程序设计(ASP)是一种主流的非单调知识表示工具。为了能够在利用ASP求解问题过程中使用现有的以经典逻辑表示的知识,给出了一种把以谓词逻辑公式表示的约束型知识和定义型知识转化为ASP程序或知识库的新方法,并以实例说明了其有... 回答集程序设计(ASP)是一种主流的非单调知识表示工具。为了能够在利用ASP求解问题过程中使用现有的以经典逻辑表示的知识,给出了一种把以谓词逻辑公式表示的约束型知识和定义型知识转化为ASP程序或知识库的新方法,并以实例说明了其有效性。该方法满足转化后ASP程序的回答集与原公式集的模型具有一一对应关系。在实际应用中,该方法提供了一项从现存的以谓词逻辑为表示语言的知识库,构建以ASP为知识表示语言的非单调知识库的技术。 展开更多
关键词 谓词逻辑 谓词公式 回答集程序设计 ASP知识库
下载PDF
基于关键迹和ASP的CSP模型检测 被引量：3
3
作者 赵岭忠 翟仲毅 +1 位作者 钱俊彦 郭云川 《软件学报》 EI CSCD 北大核心 2015年第10期2521-2544,共24页
模型检测是通信顺序进程(communicating sequential processes,简称CSP)形式化验证的重要手段.当前,CSP模型检测方法基于操作语义,需将进程转化为迁移系统,进而提取语义模型,但转化过程较为复杂;待验证性质采用CSP语言进行描述,虽然有... 模型检测是通信顺序进程(communicating sequential processes,简称CSP)形式化验证的重要手段.当前,CSP模型检测方法基于操作语义,需将进程转化为迁移系统,进而提取语义模型,但转化过程较为复杂;待验证性质采用CSP语言进行描述,虽然有利于精炼检测(refinement checking),但描述能力较弱,通用性不强.鉴于此,提出了一种新的CSP指称语义模型——关键迹模型(critical-trace model)及基于该指称语义模型的CSP模型检测方法,并证明了其验证的可靠性,避免了上述问题.关键迹模型采用递归策略计算,待验证性质采用线性时态逻辑(linear temporal logic,简称LTL)描述.基于回答集程序设计(answer set programming,简称ASP)实现了关键迹模型的自动生成及LTL的自动验证,并开发了一个CSP模型检测原型系统——T_ASP.实验结果表明:与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,且可同时验证多条性质,在性质不满足时还可提供多条反例. 展开更多
关键词 模型检测 通信顺序进程 关键迹模型 线性时态逻辑 回答集程序设计
下载PDF
基于ASP的CSP并发系统验证研究 被引量：4
4
作者 赵岭忠 张超 钱俊彦 《计算机科学》 CSCD 北大核心 2012年第12期125-132,共8页
传统并发通信顺序进程(CSP)性质的验证通常使用3个不同的模型层面,从而增加了系统的复杂性和验证工具开发的难度;同时,主流的并发系统模型验证工具不支持在系统的一次运行中验证多个性质,这也降低了性质验证的效率。首先将CSP程序转换为... 传统并发通信顺序进程(CSP)性质的验证通常使用3个不同的模型层面,从而增加了系统的复杂性和验证工具开发的难度;同时,主流的并发系统模型验证工具不支持在系统的一次运行中验证多个性质,这也降低了性质验证的效率。首先将CSP程序转换为ASP程序,然后将CSP进程并发规则和以LTL/CTL公式表示的待验证性质转换为ASP规则,从而建立了基于ASP验证CSP并发系统性质的统一框架。实验结果表明,基于ASP的CSP并发系统验证技术易于实现,在保持较高验证效率的同时,能够支持在验证软件的一次执行中验证多条LTL/CTL公式。 展开更多
关键词 通信顺序进程 回答集编程 LTL CTL
下载PDF
基于对象分布式实时系统约束的一致性研究 被引量：2
5
作者 赵岭忠 董荣胜 +1 位作者 蔡国永 古天龙 《计算机工程与应用》 CSCD 北大核心 2002年第15期60-62,71,共4页
在分布式实时系统中,时间约束规格的一致性是解决任务分配和调度等关键问题的必要前提。该文给出了一种基于对象分布式实时系统调度的通用模型,并对该模型进行了形式化描述。该模型克服了以往模型不能在应用系统的逻辑和功能部件上描述... 在分布式实时系统中,时间约束规格的一致性是解决任务分配和调度等关键问题的必要前提。该文给出了一种基于对象分布式实时系统调度的通用模型,并对该模型进行了形式化描述。该模型克服了以往模型不能在应用系统的逻辑和功能部件上描述系统实时约束的不足,允许从方法和活动上描述所需的约束,降低了单一约束描述的繁杂程度。为了解决使用该模型进行约束规格的一致性问题,该文给出了绝对时间约束、相对时间约束、一致性约束以及相对时间约束和一致性约束之间的一致性判定的必要条件。 展开更多
关键词 分布式实时系统 实时对象 调度模型 实时约束 约束一致性
下载PDF
基于进程迹的CSP模型验证框架 被引量：3
6
作者 赵岭忠 翟仲毅 钱俊彦 《计算机科学》 CSCD 北大核心 2013年第11期181-186,221,共7页
CSP(Communicating Sequential Processes)是构建并发系统和网络安全协议的经典方法。当前主流的CSP模型验证方法需将进程转化为迁移系统,转化过程比较复杂;性质采用迹进行规范,不利于活性的描述。提出了一种基于进程迹的CSP模型验证框... CSP(Communicating Sequential Processes)是构建并发系统和网络安全协议的经典方法。当前主流的CSP模型验证方法需将进程转化为迁移系统,转化过程比较复杂;性质采用迹进行规范,不利于活性的描述。提出了一种基于进程迹的CSP模型验证框架,其性质采用通用的规范方法LTL进行描述。利用ASP(Answer Set Programming)技术实现了一个CSP验证系统。实验表明,与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,在性质不满足时还可提供反例。 展开更多
关键词 通信顺序进程(CSP) 并发系统 迹模型 回答集编程(ASP)
下载PDF
基于ASP的CSP进程描述与组合研究 被引量：2
7
作者 赵岭忠 司徒凌云 +1 位作者 翟仲毅 钱俊彦 《计算机科学》 CSCD 北大核心 2013年第12期133-140,共8页
前期工作中,为解决CSP模型检测不支持一次运行验证多条性质的问题,构建了基于ASP的CSP模型检测框架,但其存在着可描述并发进程形态不完善与可验证并发系统规模受限的问题。构建了全新的并发系统ASP描述体系,其解决了前期工作中前缀描述... 前期工作中,为解决CSP模型检测不支持一次运行验证多条性质的问题,构建了基于ASP的CSP模型检测框架,但其存在着可描述并发进程形态不完善与可验证并发系统规模受限的问题。构建了全新的并发系统ASP描述体系,其解决了前期工作中前缀描述不允许出现类环状结构的问题,可完整描述各种形态的CSP进程。研究了并发组合进程生成技术,它可使多个进程自动化并发组合,并生成一个满足所有行为特性、具有一致结构特性的新进程,保持了验证框架内进程描述的一致性,有利于并发进程的抽象与验证。实验表明了基于ASP的CSP进程描述与组合进程生成技术的有效性,以及基于该ASP描述体系的系统性质验证的可行性。 展开更多
关键词 CSP ASP 模型检测
下载PDF
基于抽象解释的Prolog程序验证技术研究 被引量：1
8
作者 赵岭忠 古天龙 +1 位作者 蔡国永 钱俊彦 《计算机科学》 CSCD 北大核心 2008年第7期261-268,共8页
作为一种通用的语义近似理论,抽象解释已广泛应用于各类程序的形式化验证中。现有基于抽象解释的逻辑程序验证技术未涉及与程序点相关联的程序性质的验证,设计能够描述此类性质的逻辑程序具体语义和抽象语义是构造相应验证工具的关键。... 作为一种通用的语义近似理论,抽象解释已广泛应用于各类程序的形式化验证中。现有基于抽象解释的逻辑程序验证技术未涉及与程序点相关联的程序性质的验证,设计能够描述此类性质的逻辑程序具体语义和抽象语义是构造相应验证工具的关键。本文给出了一种基于抽象解释的Prolog程序验证方法,该方法采用了具有路径信息的Prolog语义及其抽象作为语义基础,因而可用于验证与程序点相关联的程序特性。本文例子表明了该验证方法的有效性。 展开更多
关键词 抽象解释 程序验证 PROLOG 不动点语义
下载PDF
目标独立的Prolog程序路径依赖分析语义 被引量：1
9
作者 赵岭忠 古天龙 钱俊彦 《计算机科学》 CSCD 北大核心 2008年第2期246-252,297,共8页
在Prolog程序分析中,考虑程序的执行路径和非逻辑的cut操作可提高程序分析的精度。当前用于Prolog程序路径依赖分析的语义因依赖于程序执行的目标而不适合目标独立的程序分析。为此,本文采用了一种携带路径信息并允许cut操作的Prolog抽... 在Prolog程序分析中,考虑程序的执行路径和非逻辑的cut操作可提高程序分析的精度。当前用于Prolog程序路径依赖分析的语义因依赖于程序执行的目标而不适合目标独立的程序分析。为此,本文采用了一种携带路径信息并允许cut操作的Prolog抽象语法,在此基础上给出了Prolog的操作语义和一种目标独立的标号树(LT)语义,并证明了LT语义相对于操作语义的正确性。LT语义可作为目标独立的Prolog程序路径依赖分析的基础。 展开更多
关键词 程序分析 Prolog语义 目标独立 上下文信息 抽象解释
下载PDF
知识单元在计算机科学专业教学中的应用 被引量：4
10
作者 赵岭忠 王雪松 钱俊彦 《高教论坛》 2009年第3期84-85,88,共3页
把IEEE-CS/ACM计算教程系列报告中知识单元划分的思想用于计算机科学专业教学大纲的修订和课程讲义的编写,针对当前计算机科学专业教学中存在的问题,给出了一种获得具有较小知识冗余、易于修订的教学大纲的方法和忠于大纲的课程讲义的... 把IEEE-CS/ACM计算教程系列报告中知识单元划分的思想用于计算机科学专业教学大纲的修订和课程讲义的编写,针对当前计算机科学专业教学中存在的问题,给出了一种获得具有较小知识冗余、易于修订的教学大纲的方法和忠于大纲的课程讲义的编写方法。 展开更多
关键词 计算机科学 知识单元 教学大纲 讲义
下载PDF
实时系统非周期任务的可预测调度研究 被引量：2
11
作者 赵岭忠 董荣胜 +1 位作者 古天龙 蔡国永 《桂林电子工业学院学报》 2001年第3期18-21,共4页
提出了一种实时系统任务模型 ,分析了该模型中周期和非周期任务可调度的条件 ,并给出了一种强实时非周期任务的可预测调度算法。该算法按照 RMS算法的原则统一调度系统任务 ,保证系统周期和非周期任务满足各自的时限约束 。
关键词 实时操作系统 周期任务 非周期任务 可预测调度
下载PDF
基于计算解语义的逻辑程序测试和调试框架
12
作者 赵岭忠 廖伟志 +1 位作者 钱俊彦 古天龙 《计算机科学》 CSCD 北大核心 2009年第9期115-121,共7页
逻辑程序开发过程中需要花费大量的时间用以程序调试,原因之一是调试通常包含大量的用户交互。减少对调试过程不必要的调用能够提高软件开发的效率。程序测试中得到的由同一个错误引发的多个症状是引发对调试过程不必要调用的因素之一... 逻辑程序开发过程中需要花费大量的时间用以程序调试,原因之一是调试通常包含大量的用户交互。减少对调试过程不必要的调用能够提高软件开发的效率。程序测试中得到的由同一个错误引发的多个症状是引发对调试过程不必要调用的因素之一。给出了一种逻辑程序测试和调试框架,其中测试用例的生成、症状的发现和调试(包括诊断和改错)交叉进行,由同一个错误引发的症状只有一个可引发调试过程执行,并以此方式避免了对调试过程不必要的调用。然后,利用一种基于约束的Prolog计算解语义,该框架被实例化为一种Prolog程序的测试和调试算法,本实例表明了该算法的应用。 展开更多
关键词 测试 调试 逻辑程序 计算解语义
下载PDF
一种基于熵的OBDD变量排序算法
13
作者 赵岭忠 王雪松 +1 位作者 古天龙 钱俊彦 《计算机科学》 CSCD 北大核心 2007年第2期216-219,共4页
有序二叉决策图(OBDD)是一种有效表示布尔函数的数据结构,其大小依赖于所采用的变量序。熵是定量描述布尔函数中变量重要性的一种方法。基于变量的熵值分析了高质量变量序的特征,给出了一种基于熵的OBDD变量排序算法。实验结果表明:该... 有序二叉决策图(OBDD)是一种有效表示布尔函数的数据结构,其大小依赖于所采用的变量序。熵是定量描述布尔函数中变量重要性的一种方法。基于变量的熵值分析了高质量变量序的特征,给出了一种基于熵的OBDD变量排序算法。实验结果表明:该算法与模拟退火算法和遗传算法结果相当,时间仅为相应算法的80.84%和29.79%。 展开更多
关键词 有序二叉决策图 变量序 熵
下载PDF
基于OBDD的含圈与或图搜索算法研究
14
作者 赵岭忠 王雪松 《计算机应用研究》 CSCD 北大核心 2011年第4期1325-1329,共5页
在含圈与或图理论框架基础上,给出了基于OBDD的含圈与或图符号表示方法,并提出了一种求解含圈与或图最小代价解图的符号搜索算法。实验结果表明,该算法在处理大规模含圈与或图时具有明显优势。
关键词 含圈与或图 最大可扩展子图 最小代价解图 有序二叉决策图
下载PDF
调用模式和正确调用模式语义在Prolog程序测试中的应用
15
作者 赵岭忠 钱俊彦 《计算机应用研究》 CSCD 北大核心 2008年第4期1008-1012,共5页
将基于调用模式语义和正确调用模式语义的程序分析技术应用于Prolog程序的CPM测试。通过调用模式分析获得内部过程被调用和成功调用的条件,利用前者删除不满足调用条件的测试帧,或当删除条件不满足时利用该条件更新测试规格中过程属性... 将基于调用模式语义和正确调用模式语义的程序分析技术应用于Prolog程序的CPM测试。通过调用模式分析获得内部过程被调用和成功调用的条件,利用前者删除不满足调用条件的测试帧,或当删除条件不满足时利用该条件更新测试规格中过程属性的划分准则;利用后者预测CPM测试的结果。该方法可较好地保持程序测试的质量,改善Prolog程序的CPM测试过程。 展开更多
关键词 PROLOG 调用模式语义 正确调用模式语义 主属性区分方法测试
下载PDF
改进形式语言与自动机理论课程教学刍议
16
作者 赵岭忠 王雪松 钱俊彦 《高教论坛》 2008年第3期113-115,共3页
分析了形式语言与自动机理论课程的特点以及该课程在桂林电子科技大学教学的现状,针对存在的问题,从课程内容设置、实验教学和理论教学三个方面提出了改进教学效果的几点建议。其基本思想是通过认识该课程的重要性,提高学生在课程学习... 分析了形式语言与自动机理论课程的特点以及该课程在桂林电子科技大学教学的现状,针对存在的问题,从课程内容设置、实验教学和理论教学三个方面提出了改进教学效果的几点建议。其基本思想是通过认识该课程的重要性,提高学生在课程学习中的积极性;通过把现代交互式教学方法贯彻到教学的各个环节,提高学生学习的趣味性和交互性。 展开更多
关键词 形式语言与自动机理论 动态性 交互性 教学辅助软件
下载PDF
网络最大流问题求解的符号ADD增广路径算法 被引量：9
17
作者 徐周波 古天龙 赵岭忠 《计算机科学》 CSCD 北大核心 2005年第10期38-40,54,共4页
本文通过对网络及网络最大流问题的符号代数判定图(ADD)描述,将网络中的结点和边用ADD隐式表示,并利用Gabow的容量变尺度算法的主要思想,将一般网络最大流问题化为一系列的单位容量网络最大流问题,结合Hachtel等的单位容量网络最大流问... 本文通过对网络及网络最大流问题的符号代数判定图(ADD)描述,将网络中的结点和边用ADD隐式表示,并利用Gabow的容量变尺度算法的主要思想,将一般网络最大流问题化为一系列的单位容量网络最大流问题,结合Hachtel等的单位容量网络最大流问题的求解算法,给出了网络最大流问题求解的符号ADD增广路径算法,简称为符号ADD算法。与Dinic算法、Karzanov算法相比,本文算法的空间复杂度得到了改善。实验结果表明,本文算法是切实有效的,且可处理更大规模的问题。 展开更多
关键词 符号算法 最大流 代数判定图(ADD) 剩余网络 网络最大流 路径算法 问题求解 ADD 符号 最大流问题 变尺度算法 空间复杂度 求解算法
下载PDF
网络最大流问题的一种新的符号ADD求解算法 被引量：15
18
作者 徐周波 古天龙 赵岭忠 《通信学报》 EI CSCD 北大核心 2005年第2期1-8,共8页
通过对网络及网络最大流问题的符号代数判定图描述,在Trff算法的基础上,给出了网络最大流问题的一种新的符号ADD求解算法。与Dinic、Karzanov算法相比,本文算法的空间复杂度较低。实验结果表明,该算法可处理更大规模的问题。
关键词 网络优化 最大流 符号算法 代数判定图
下载PDF
基于对象的分布式实时系统调度模型研究 被引量：5
19
作者 董荣胜 赵岭忠 +1 位作者 蔡国永 古天龙 《计算机研究与发展》 EI CSCD 北大核心 2002年第11期1464-1470,共7页
为了解决分布式实时系统有关分配和调度等问题 ,给出并用形式化方法描述了一种基于对象分布式实时系统调度的通用模型 .该模型包括表示时限的绝对时间约束、表示周期属性的周期约束、表示各种前趋关系和同步要求的相对时间约束以及保证... 为了解决分布式实时系统有关分配和调度等问题 ,给出并用形式化方法描述了一种基于对象分布式实时系统调度的通用模型 .该模型包括表示时限的绝对时间约束、表示周期属性的周期约束、表示各种前趋关系和同步要求的相对时间约束以及保证资源使用一致性的一致性约束 .此外该模型克服了以往模型不能在应用系统的逻辑和功能部件上描述系统实时约束的不足 ,允许从方法和活动上描述所需的约束 ,降低了单一约束描述的繁杂程度 .为了能够使用现有调度算法进行任务调度 ,讨论了约束转换的问题 ,给出了高层约束到底层约束的转换规则和相应的转换算法 . 展开更多
关键词 对象 分布式实时系统 调度模型 实时约束 约束转换 多处理机 程序设计
下载PDF
一种基于时间自动机的时钟等价性优化方法 被引量：5
20
作者 钱俊彦 赵岭忠 古天龙 《计算机工程》 EI CAS CSCD 北大核心 2005年第18期71-73,共3页
提出了一种优化模型检验时间自动机的时钟等价规则,通过优化的时钟等价规则,使时间自动机等价后的域自动机状态数尽可能少,并在此基础上定义了适合于优化时钟等价规则的域自动机。优化时钟等价规则,在一定程度上有效地解决了状态空间爆... 提出了一种优化模型检验时间自动机的时钟等价规则,通过优化的时钟等价规则,使时间自动机等价后的域自动机状态数尽可能少,并在此基础上定义了适合于优化时钟等价规则的域自动机。优化时钟等价规则,在一定程度上有效地解决了状态空间爆炸问题。 展开更多
关键词 模型检验 时间自动机 域自动机 时态逻辑
下载PDF
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
上一页 1 2 … 4 下一页 到第 页
使用帮助 返回顶部