陕西省科技攻关计划(2009K01-36)

作品数：5被引量：6H指数：1
导出分析报告
相关作者：张海宾周清雷朱维军段振华聂鹏程更多>>
相关机构：西安电子科技大学郑州大学武汉大学更多>>
相关期刊：《电子学报》《西安电子科技大学学报》《华中科技大学学报（自然科学版）》更多>>
相关主题：时序逻辑SKYLINE算法多核并行多核可满足性判定更多>>
相关领域：自动化与计算机技术更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-5
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于枢轴选择策略的多核并行skyline算法
《四川大学学报（工程科学版）》2011年第1期109-115,共7页黄伯虎 张海宾 逄涛 聂鹏程 
国家重点基础研究发展计划资助项目(2010CB328102);国家自然科学基金重大国际合作资助项目(60910004);国家自然科学基金资助项目(60873018);陕西省科技攻关计划资助项目(2009K01-36);中央高校基本科研业务费专项资金资助项目(JY10000903004JY10000903014)
针对当前大规模高维数据集skyline计算效率较低的问题,提出了一种多核并行算法MPSSI(Multi-core Par-allel Skyline computation based on Sorting and Incomparability)。首先对数据集进行预排序处理,简化了后续计算过程;并通过精心选...
关键词：SKYLINE计算 多核 并行算法 排序 信息检索 
一种采用预排序策略的多核并行skyline算法
《华中科技大学学报（自然科学版）》2010年第10期31-34,共4页黄伯虎 段振华 张金磊 聂鹏程 
国家重点基础研究发展计划资助项目(2010CB328102);国家自然科学基金重大国际合作资助项目(60910004);国家自然科学基金资助项目(60873018);陕西省科技攻关计划资助项目(2009K01-36);中央高校基本科研业务费专项资金资助项目(JY10000903004;JY10000903014)
为提升大规模多维数据集的skyline计算效率,提出了一种多核并行算法MPSCS(multi-core parallelskyline computation based on sorting).首先按照任意一维对数据集进行预排序,然后划分为多个子集,使用skeleton并行程序设计模型进行并行...
关键词：并行算法 SKYLINE算法 并行编程 多核 预排序 
命题投影时序逻辑并发建模与自动验证被引量：2
《华中科技大学学报（自然科学版）》2010年第8期77-80,共4页朱维军 张海宾 周清雷 
国家高技术研究发展计划资助项目(2007AA010408);中国高校基本科研业务专项资金资助项目(JY10000903014);河南省重大科技攻关计划资助项目(092101210104);陕西省科技攻关计划资助项目(2009K01-36)
针对目前尚无模型检测方法对区间并发模型进行区间性质的自动验证的情况,采用命题投影时序逻辑中具有特定结构的一类公式来建立系统的区间并发模型,该逻辑的任意公式可以描述模型需要满足的区间性质,通过归约为已有的逻辑公式可满足性...
关键词：模型检测 时序逻辑 可计算性与判定性 命题投影时序逻辑 并发模型 统一逻辑框架 
框架时序逻辑语言MSVL中面向对象机制的实现被引量：1
《西安电子科技大学学报》2010年第3期559-564,575,共7页王小兵 段振华 
国家重点基础研究发展计划973资助项目(2010CB328102);国家自然科学基金重大国际合作资助项目(60910004);国家自然科学基金资助项目(60873018);武汉大学软件工程国家重点实验室开放基金资助项目(SKLSE20080713);陕西省科技攻关计划资助项目(2009K01-36);中央高校基本科研业务费专项资金资助项目(JY10000903004;JY10000903014)
针对目前时序逻辑语言存在框架问题、缺少面向对象机制、形式化程度过高等不足,提出了框架时序逻辑语言MSVL,包含新的框架操作符、等待语句和非确定的选择语句等技术,并且能够支持面向对象的程序设计.基于正则形和正则图,给出了MSVL解...
关键词：框架 时序逻辑 时序逻辑语言 面向对象程序设计 解释器 
离散时间区间时序逻辑可满足性的判定被引量：4
《电子学报》2010年第5期1039-1045,共7页朱维军 张海宾 周清雷 
国家863高技术研究发展计划(No.2007AA010408);河南省重大科技攻关计划(No.092101220104);陕西省科技攻关计划(No.2009K01-36)
目前还没有模型检查的方法自动检测模型是否满足时间区间时序逻辑描述的性质.我们约束时间域到离散时间,证明了离散时间区间时序逻辑的可满足性是可判定的,因而是可模型检查的.提出了时间正则图模型,通过从离散时间区间时序逻辑到时间...
关键词：模型检查 离散时间区间时序逻辑 时间正则图 可满足性判定 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部