可满足性判定

作品数：11被引量：10H指数：1
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：常亮张海宾周清雷朱维军古天龙更多>>
相关机构：西安电子科技大学桂林电子科技大学郑州大学中国科学院大学更多>>
相关期刊：《计算机研究与发展》《西安电子科技大学学报》《电子科技大学学报》《电子学报》更多>>
相关基金：国家自然科学基金国家高技术研究发展计划国家教育部博士点基金河南省科技攻关计划更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于时间区间时序逻辑的实时系统统一模型检测
《电子科技大学学报》2014年第5期712-716,共5页朱维军 乔芃喆 周清雷 张海宾 
国家自然科学基金(U1204608;U1304606;61373043);中国博士后科学基金(2012M511588)
在同一个逻辑框架内无法自动验证实时区间模型的实时区间性质。为此,该文使用一个离散时间区间时序逻辑公式建立实时系统模型,使用另一个离散时间区间时序逻辑公式描述实时系统需要满足的性质,在此基础上,离散时间区间时序逻辑统一模型...
关键词：统一模型检测 实时系统 可满足性判定 时间区间时序逻辑 
分支时态描述逻辑ALC-CTL及其可满足性判定
《计算机科学》2014年第3期205-211,共7页李屾 常亮 孟瑜 李凤英 
国家自然科学基金(61363030;61100025;61262030);广西自然科学基金(2012GXNS FBA053169;2012GXNSFAA053220);广西可信软件重点实验室基金(KX201109)资助
时态描述逻辑是将描述逻辑与时态逻辑相结合后得到的逻辑系统,具有较强的描述能力;但是大部分的时态描述逻辑都是将时态算子同时引入到概念和公式中,使得公式可满足性问题的计算复杂度过高。将描述逻辑ALC与分支时态逻辑CTL相结合,提出...
关键词：时态描述逻辑 分支时态逻辑 可满足性问题 TABLEAU算法 复杂度 
扩展命题区间时序逻辑公式可满足性判定算法被引量：1
《电子科技大学学报》2011年第5期753-758,共6页朱维军 邓淼磊 周清雷 张海宾 
国家863高技术研究发展计划(2007AA010408);国家自然科学基金(61003079);教育部博士点基金(20100203120012);陕西省工业攻关计划(2009K01-36);中央高校基本科研业务费(JY10000903014)
针对扩展命题区间时序逻辑由于缺少验证算法因而不能用于模型检测问题,提出该逻辑的可满足性判定算法。首先,正则形子算法把带星算子或不带星算子的扩展命题区间时序逻辑公式翻译为其正则形公式;然后,正则图子算法根据正则形公式构造公...
关键词：扩展命题区间时序逻辑 模型检测 正则图 可满足性判定 
基于OBDD的Iteration-free CPDL判定算法
《桂林电子科技大学学报》2011年第3期221-225,共5页覃凤萍 古天龙 常亮 
国家自然科学基金(60963010)
命题动态逻辑是一种应用模态逻辑,用于程序行为的推理。Iteration-free CPDL是一种无迭代算子而含有逆算子的命题动态逻辑。对于给定的Iteration-free CPDL公式集,方法是应用NCNF变换和FLAT规则对其进行预处理,并对公式集重构模型,然后...
关键词：命题动态逻辑 可满足性判定 有序二叉决策图 
支持服务组合的需求模型及其可满足性判定被引量：2
《计算机科学与探索》2011年第5期458-466,共9页叶荣华 金芝 钟发荣 
国家自然科学基金 No.90818026;60873234;浙江省自然科学基金 No.Y1110483~~
服务组合一般是根据用户需求来查找匹配的服务并对其进行组合,但用户需求往往是基于自然语言的,很难用于服务的自动组合。提出了一种基于环境本体的组合服务需求模型,该模型以环境实体上的意图为基础,将关联意图集定义为任务。引入Petr...
关键词：组合服务需求 意图 任务 PETRI网 环境本体 
基于OBDD的描述逻辑SHOIQ判定算法研究与实现
《桂林电子科技大学学报》2011年第2期120-124,共5页李德波 古天龙 常亮 高西 
国家自然科学基金(60963010);广西研究生教育创新计划资助项目(2010105950812M24)
描述逻辑是语义Web的逻辑基础,已成为当前计算机科学和人工智能研究的热点。鉴于描述逻辑SHOIQ的经典判定算法在处理大规模问题上的不足,以OBDD能很好处理大规模问题为基础,给出了一种基于OBDD的SHOIQ判定算法。该算法利用相关规则和技...
关键词：描述逻辑 一致性 OBDD 可满足性判定 
基于OBDD的描述逻辑ALCIO判定算法
《广西科学院学报》2010年第4期401-405,共5页常亮 高申 李德波 古天龙 
国家自然科学基金项目(60903079;60963010)资助
给定描述逻辑ALCIO中的任一知识库,应用NNF变换和FLAT规则对其进行预处理,通过一个重构过程将知识库中TBox模型转化为布尔函数,然后将布尔函数转换为有序二叉决策图(OBDD)表示形式,从而调用已有的OBDD软件包进行可满足性判定,实现描述逻...
关键词：描述逻辑 有序二叉决策图 枚举算子 可满足性判定 
时间区间时序逻辑的判定性与表达能力
《计算机科学》2010年第11期227-229,共3页朱维军 周清雷 
国家(863)高技术研究发展计划(No2007AA010408);河南省重大科技攻关计划(No.092101210104)资助
模型检测技术在实时系统验证中被广泛使用。离散时间区间时序逻辑满足性是可判定的,因而也是可模型检测的。连续时间域时间区间时序逻辑是否可模型检测,则并不清楚。约束时间域到非负实数,证明了其可满足性是不可判定的,但存在该逻辑的...
关键词：时间区间时序逻辑 可满足性判定 表达能力 模型检测 
离散时间区间时序逻辑可满足性的判定被引量：4
《电子学报》2010年第5期1039-1045,共7页朱维军 张海宾 周清雷 
国家863高技术研究发展计划(No.2007AA010408);河南省重大科技攻关计划(No.092101220104);陕西省科技攻关计划(No.2009K01-36)
目前还没有模型检查的方法自动检测模型是否满足时间区间时序逻辑描述的性质.我们约束时间域到离散时间,证明了离散时间区间时序逻辑的可满足性是可判定的,因而是可模型检查的.提出了时间正则图模型,通过从离散时间区间时序逻辑到时间...
关键词：模型检查 离散时间区间时序逻辑 时间正则图 可满足性判定 
稠密时间区间时序逻辑的可满足性判定被引量：3
《西安电子科技大学学报》2007年第3期463-467,共5页张海宾 段振华 
国家自然科学基金资助项目(60373103);国家自然科学基金重大资助项目(60433010);博士点基金资助项目(20030701015)
定义了稠密时间区间时序逻辑(DTITL),它是区间时序逻辑的一种实时扩充.通过定义DTITL无穷状态空间上的具有有限个数等价类的等价关系,把DTITL的连续状态模型离散化为一阶区间时序逻辑模型.定义了一套规则来构造DTITL公式对应的有界整数...
关键词：实时系统 时序逻辑 模型检查 混合系统 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部