KRIPKE结构

作品数：35被引量：100H指数：6
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：李永明潘海玉鱼先锋周颖郑国梁更多>>
相关机构：陕西师范大学上海大学泰州学院北方民族大学更多>>
相关期刊：《计算机应用研究》《小型微型计算机系统》《内江师范学院学报》《模糊系统与数学》更多>>
相关基金：国家自然科学基金国家高技术研究发展计划国家教育部博士点基金国家重点基础研究发展计划更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于Kripke的状态保留模型修复算法
《桂林电子科技大学学报》2024年第6期599-605,共7页戴敏 潘海玉 
国家自然科学基金(62162014);广西自然科学基金(2018GXNSFAA281326);广西可信软件重点实验室基金(KX201911)。
针对模型验证中受到广泛关注的模型修复问题,在极小模型修复的基础上保留原模型中尽可能多的可达状态,并给出了具有多项式时间复杂度的修复算法。模型经过检验后,若被判定存在违反给定性质的行为,则可以借助经典模型检验的不动点思想,...
关键词：模型检验 模型修复 可达状态 计算树逻辑 KRIPKE结构 
模糊Kripke结构的子模型修复算法被引量：2
《郑州大学学报（理学版）》2023年第1期77-83,共7页王辉 石铁柱 钱俊彦 潘海玉 
国家自然科学基金项目(62162014);广西自然科学基金项目(2018GXNSFAA281326);广西可信软件重点实验室项目(kx201911)。
在模糊模型检测时,如果模糊Kripke结构不满足性质规约,模型检测工具会给出模型中违反性质规约的反例,这往往需要设计人员手工修复,会导致效率低下,因此如何对模糊Kripke结构进行自动修复具有极大的研究意义。由此,提出一个基于模糊table...
关键词：模型检测 计算树逻辑 模糊逻辑 模型修复 
基于量子逻辑的模糊线性时序逻辑的模型检测被引量：1
《模糊系统与数学》2021年第1期9-21,共13页杨维禹 刘文奇 
模型检测的主要问题是处理具有量化信息的系统的验证问题,该文在量子逻辑和时序逻辑的相关理论基础上引入了可能性理论以及模糊线性时间的可能性测度,研究了线性时序逻辑在模糊时态下的模型检测方法。通过引入可能性理论以及广义可能性K...
关键词：模型检测 量子逻辑 时序逻辑 可能性理论 广义可能性测度 广义可能性Kripke结构 
直觉模糊模型检测在工程决策上的应用被引量：1
《模糊系统与数学》2020年第2期142-150,共9页鱼先锋 李永明 
国家自然科学基金资助项目(61228305);商洛市科技计划项目(sk2018-03-01);商洛学院科技创新团队建设项目(18SCX002)。
将直觉模糊Kripke结构扩展到加权直觉模糊Kripke结构,将直觉模糊计算树逻辑诱导到加权直觉模糊计算树逻辑;研究在此之上的直觉模糊期望测度和多属性工程决策问题。用加权直觉模糊Kripke结构的权值自然地刻画了工程问题中的成本和收益,...
关键词：加权直觉模糊Kripke结构 工程决策 加权直觉模糊计算树逻辑 模型检测 
嵌入偏序约简的状态事件线性时序逻辑验证被引量：6
《计算机学报》2019年第10期2145-2159,共15页谢健 阚双龙 黄志球 王飞 杨志斌 李伟湋 
国家高技术研究发展计划项目（2015AA105303）;国家重点研发计划项目(2016YFB1000802）;江苏省自然科学基金青年基金（BK20170809）;中国博士后基金面上基金（2018M632304）资助
模型检验是硬件和软件形式化验证最成功的技术之一.目前大部分的模型检验技术是基于状态的而不考虑迁移上的操作和事件.这导致模型检验在验证使用事件进行交互的组件系统中面临新的困难,因此需要新的规约技术对状态事件系统进行规约.状...
关键词：偏序约简 状态事件线性时序逻辑 模型检验 同步乘 标签Kripke结构 
多值可能性模型检测器的设计与实现
《计算机技术与发展》2019年第5期62-65,69,共5页洪云端 李永明 
国家自然科学基金(11671244)
随着现代计算机软件和硬件的复杂性变大,模型检测作为一种形式化自动验证技术,与传统的检测技术相比有着一系列的优势,比如可以在系统实现之前对系统进行验证,可以提前发现问题,节约大量成本。传统的模型检测器大多是基于经典的模型检...
关键词：模型检测 多值可能性 KRIPKE结构 自动验证 模型检测器 
不确定型模糊Kripke结构的计算树逻辑模型检测被引量：11
《电子学报》2018年第1期152-159,共8页范艳焕 李永明 潘海玉 
国家自然科学基金(No.11671244;No.61261047;No.61672023;No.61673352);教育部博士点基金(No.20130202110001);青海省自然科学基金(No.2014-ZJ-908);江苏高校"青蓝工程"
本文研究了不确定型模糊Kripke结构的计算树逻辑的模型检测问题,并说明了该问题可以在对数多形式时间内解决.首先给出了不确定型模糊Kripke结构的定义,引入了模糊计算树逻辑的语法和语义.为了刻画存在量词?和任意量词在不确定型模糊Kr...
关键词：模型检测 计算树逻辑 模糊逻辑 KRIPKE结构 时态逻辑 
直觉模糊测度的计算树逻辑被引量：5
《计算机科学与探索》2017年第9期1523-1530,共8页鱼先锋 李超 李永明 
国家自然科学基金(No.61228305);陕西省教育厅专项科研计划项目(No.2015JK0605);商洛学院科研项目(No.15SKY001)~~
建立了直觉模糊Kripke结构(intuitionistic fuzzy Kripke structure,IFKS)模型,提出了基于直觉模糊Kripke结构的直觉模糊测度空间理论,阐述了IFKS的一系列性质。证明了任一路径转移的直觉模糊可达度(intuitionistic fuzzy probability,I...
关键词：直觉模糊Kripke结构 直觉模糊测度 直觉模糊计算树逻辑 模型检测 
模糊计算树逻辑的基本性质被引量：1
《内江师范学院学报》2016年第12期21-24,共4页朱晔 郦丽 江敏 
国家自然科学基金资助项目(61672023)
引入了基于Zadeh模糊逻辑的计算树逻辑的语法和语义,讨论了不同的模糊计算树逻辑公式之间的语义关系,分析了模糊计算树逻辑语义模型的模糊赋值函数发生变化时,对模糊计算树逻辑语义的影响.
关键词：KRIPKE结构 形式化验证 模糊逻辑 计算树逻辑 
不确定型多值Kripke结构的模型检测被引量：1
《模糊系统与数学》2016年第5期60-70,共11页郦丽 沈应兄 潘海玉 
国家自然科学基金(11301321;11401361);中国博士后科学基金资助项目(2014M552408)
多值模型检测是经典模型检测的一种扩展,主要用于具有不一致信息的系统的验证。为了对具有不一致和不确定性的系统进行形式化分析,本文提出非确定型多值Kripke结构作为此类系统的模型,引入一种多值计算树逻辑作为非确定型多值Kripke结...
关键词：多值模型检验 计算树逻辑 模糊自动机 DE MORGAN代数 
全选清除导出
共4页<1234>
检索报告 对象比较 聚类工具 使用帮助 返回顶部