期刊导航
期刊开放获取
cqvip
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
4
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式：
文摘
详细
列表
相关度排序
被引量排序
时效性排序
基于可能性测度的计算树逻辑
被引量：
14
1
作者
薛艳
雷红轩
李永明
《计算机工程与科学》
CSCD
北大核心
2011年第9期70-75,共6页
首先,提出了可能的Kripke结构的定义,建立了可能的Kripke结构的可能性测度空间,并分析了可能的Kripke结构的一系列性质,即任一路径转移的可能性可由其初始状态的可能性分布与各转移的可能性取下确界而得到;依据可能的Kripke结构所定义...
首先,提出了可能的Kripke结构的定义,建立了可能的Kripke结构的可能性测度空间,并分析了可能的Kripke结构的一系列性质,即任一路径转移的可能性可由其初始状态的可能性分布与各转移的可能性取下确界而得到;依据可能的Kripke结构所定义的可能性测度具有其合理性等等。其次,给出了可能性计算树逻辑(PoCTL)的概念,讨论了两个PoCTL状态公式以及PoCTL与经典计算树逻辑(CTL)公式的等价性。最后,证明了PoCTL公式有与CTL*公式中"一致性"相对应的公式。
展开更多
关键词
可能
的
kripke
结构
可能
性测度
可能
性计算树逻辑
一致性
下载PDF
职称材料
基于可能性测度的计算树逻辑CTL~＊与可能性互模拟
被引量：
11
2
作者
邓辉
薛艳
+1 位作者
李亚利
李永明
《计算机科学》
CSCD
北大核心
2012年第10期258-263,共6页
提出了基于可能性测度的计算树逻辑CTL*(PoCTL*)的概念。给出了在可能的Kripke结构中可能性互模拟的定义并对其性质进行了详细的探讨。对商可能性Kripke结构及其相关构造进行了特别的研究。
关键词
可能
的
kripke
结构
可能
性测度
可能
性计算树逻辑PoCTL＊
可能
性互模拟
商
可能
性
kripke
结构
下载PDF
职称材料
可能性测度下计算树逻辑的若干性质
被引量：
7
3
作者
李亚利
李永明
《陕西师范大学学报（自然科学版）》
CAS
CSCD
北大核心
2013年第6期6-11,共6页
为讨论可能的计算树逻辑(PoCTL)与计算树逻辑(CTL)的关系,给出PoCTL公式与CTL公式等价的概念,利用公式的等价性证明了CTL是PoCTL的一个真子集.通过PoCTL模型检测算法与PoCTL公式的分析,解决了PoCTL模型检测的时间复杂度问题.最后对重复...
为讨论可能的计算树逻辑(PoCTL)与计算树逻辑(CTL)的关系,给出PoCTL公式与CTL公式等价的概念,利用公式的等价性证明了CTL是PoCTL的一个真子集.通过PoCTL模型检测算法与PoCTL公式的分析,解决了PoCTL模型检测的时间复杂度问题.最后对重复事件与持久性事件的定性性质及定量性质进行研究,用实例验证了CTL公式与PoCTL公式在可能性测度与概率测度下的本质区别.
展开更多
关键词
计算树逻辑
可能
的
kripke
结构
等价性
定性性质
定量性质
下载PDF
职称材料
可能性测度下的LTL模型检测并行化研究
被引量：
3
4
作者
雷丽晖
王静
《计算机科学》
CSCD
北大核心
2018年第4期71-75,88,共6页
分布式模型检测是一种缓解状态空间爆炸的有效途径,已有文献提出了定性的分布式模型验证算法,然而定量LTL验证算法并行化问题还未得到有效解决。对此,展开两个方面的工作:提出一种新的动态系统状态空间划分方法;在定性LTL分布式验证算...
分布式模型检测是一种缓解状态空间爆炸的有效途径,已有文献提出了定性的分布式模型验证算法,然而定量LTL验证算法并行化问题还未得到有效解决。对此,展开两个方面的工作:提出一种新的动态系统状态空间划分方法;在定性LTL分布式验证算法的基础上给出了定量模型检测并行化验证算法。首先,将系统模型转化为可能的Kripke结构并选取一个并发分量,依据状态之间的关系完成系统状态的分割,使得关系紧密的状态尽可能分布在同一个计算节点上;其次,调整划分结果以使得计算负载平衡;然后,将划分结果与其他并发分量的状态进行叉乘,以完成系统状态空间的划分;最后,将待检测性质用自动机表示,在两者的乘积上,利用扩展的基于嵌套DFS的分布式验证算法完成系统的定量验证。
展开更多
关键词
可能
的
kripke
结构
状态空间划分
定量分布式模型检测
下载PDF
职称材料
题名
基于可能性测度的计算树逻辑
被引量：
14
1
作者
薛艳
雷红轩
李永明
机构
陕西师范大学计算机科学学院
内江师范学院数学与信息科学学院
出处
《计算机工程与科学》
CSCD
北大核心
2011年第9期70-75,共6页
文摘
首先,提出了可能的Kripke结构的定义,建立了可能的Kripke结构的可能性测度空间,并分析了可能的Kripke结构的一系列性质,即任一路径转移的可能性可由其初始状态的可能性分布与各转移的可能性取下确界而得到;依据可能的Kripke结构所定义的可能性测度具有其合理性等等。其次,给出了可能性计算树逻辑(PoCTL)的概念,讨论了两个PoCTL状态公式以及PoCTL与经典计算树逻辑(CTL)公式的等价性。最后,证明了PoCTL公式有与CTL*公式中"一致性"相对应的公式。
关键词
可能
的
kripke
结构
可能
性测度
可能
性计算树逻辑
一致性
Keywords
possibilistic
kripke
structure
possibility measure
possibility computation tree logic
per-sistence property
分类号
TP301.2 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
基于可能性测度的计算树逻辑CTL~＊与可能性互模拟
被引量：
11
2
作者
邓辉
薛艳
李亚利
李永明
机构
陕西师范大学计算机科学学院
出处
《计算机科学》
CSCD
北大核心
2012年第10期258-263,共6页
基金
国家自然科学基金(60873119)
中央高校基本科研费(GK201001003)资助
文摘
提出了基于可能性测度的计算树逻辑CTL*(PoCTL*)的概念。给出了在可能的Kripke结构中可能性互模拟的定义并对其性质进行了详细的探讨。对商可能性Kripke结构及其相关构造进行了特别的研究。
关键词
可能
的
kripke
结构
可能
性测度
可能
性计算树逻辑PoCTL＊
可能
性互模拟
商
可能
性
kripke
结构
Keywords
Possibilistic
kripke
structure
Possibility measure
Possibilistic computation tree logic PoCTL＊
Possibilistic bisimulation
Quotient possibilistic
kripke
structure
分类号
TP301.2 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
可能性测度下计算树逻辑的若干性质
被引量：
7
3
作者
李亚利
李永明
机构
陕西师范大学计算机科学学院
出处
《陕西师范大学学报（自然科学版）》
CAS
CSCD
北大核心
2013年第6期6-11,共6页
基金
国家自然科学基金资助项目(11271237
61228305)
中央高校基本科研业务费专项资金项目(GK201001003)
文摘
为讨论可能的计算树逻辑(PoCTL)与计算树逻辑(CTL)的关系,给出PoCTL公式与CTL公式等价的概念,利用公式的等价性证明了CTL是PoCTL的一个真子集.通过PoCTL模型检测算法与PoCTL公式的分析,解决了PoCTL模型检测的时间复杂度问题.最后对重复事件与持久性事件的定性性质及定量性质进行研究,用实例验证了CTL公式与PoCTL公式在可能性测度与概率测度下的本质区别.
关键词
计算树逻辑
可能
的
kripke
结构
等价性
定性性质
定量性质
Keywords
computation tree logic
possibilistic
kripke
structure
equivalence property
qualitative property
quantitative property
分类号
TP301.2 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
可能性测度下的LTL模型检测并行化研究
被引量：
3
4
作者
雷丽晖
王静
机构
陕西师范大学计算机科学学院
出处
《计算机科学》
CSCD
北大核心
2018年第4期71-75,88,共6页
基金
国家自然科学基金(11271237
11301321)
中央高校基本科研业务费专项资金(GK201603086)资助
文摘
分布式模型检测是一种缓解状态空间爆炸的有效途径,已有文献提出了定性的分布式模型验证算法,然而定量LTL验证算法并行化问题还未得到有效解决。对此,展开两个方面的工作:提出一种新的动态系统状态空间划分方法;在定性LTL分布式验证算法的基础上给出了定量模型检测并行化验证算法。首先,将系统模型转化为可能的Kripke结构并选取一个并发分量,依据状态之间的关系完成系统状态的分割,使得关系紧密的状态尽可能分布在同一个计算节点上;其次,调整划分结果以使得计算负载平衡;然后,将划分结果与其他并发分量的状态进行叉乘,以完成系统状态空间的划分;最后,将待检测性质用自动机表示,在两者的乘积上,利用扩展的基于嵌套DFS的分布式验证算法完成系统的定量验证。
关键词
可能
的
kripke
结构
状态空间划分
定量分布式模型检测
Keywords
Possibilistic
kripke
structure
State partition of system
Quantitative distributed model checking
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
基于可能性测度的计算树逻辑
薛艳
雷红轩
李永明
《计算机工程与科学》
CSCD
北大核心
2011
14
下载PDF
职称材料
2
基于可能性测度的计算树逻辑CTL~＊与可能性互模拟
邓辉
薛艳
李亚利
李永明
《计算机科学》
CSCD
北大核心
2012
11
下载PDF
职称材料
3
可能性测度下计算树逻辑的若干性质
李亚利
李永明
《陕西师范大学学报（自然科学版）》
CAS
CSCD
北大核心
2013
7
下载PDF
职称材料
4
可能性测度下的LTL模型检测并行化研究
雷丽晖
王静
《计算机科学》
CSCD
北大核心
2018
3
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部
