云南高校图书馆联盟文献共享服务平台- 苏开乐

苏开乐: 作品数：40被引量：117H指数：7; 导出分析报告; 供职机构：浙江师范大学数理与信息工程学院更多>>; 发文主题：开放逻辑时态认知逻辑有界模型检测时态安全协议更多>>; 发文领域：自动化与计算机技术理学电子电信更多>>; 发文期刊：《科技创新导报》《模式识别与人工智能》《计算机工程与应用》《数学年刊（A辑）》更多>>; 所获基金：国家自然科学基金广东省自然科学基金国家重点基础研究发展计划国家杰出青年科学基金更多>>

协议组合逻辑在实例化空间模型中的语义解释: 《广东技术师范学院学报》2016年第2期8-19,共12页肖茵茵苏开乐; 国家自然科学基金(60903054;61379019);国家"973"重点基础研究发展计划资助项目(2010CB328103);中国博士后科学基金面上项目(2013M540704);广东高校优秀青年创新人才培育项目(LYM11085;LYM11084)资助; 安全协议的验证是个不可判问题.为了对实例化空间逻辑ISL的语义表达能力给出理论上的衡量与评价,选择另一种实用的协议组合逻辑PCL,分析了ISL和PCL之间的关系.在此基础上,将PCL的索状空间语义模型转换为ISL的实例化空间语义模型,在实例...; 关键词：安全协议验证实例化空间协议组合逻辑索状空间语义解释

信息服务的构造与验证研究报告: 《科技创新导报》2016年第1期173-173,共1页苏开乐卢汉清刘静黄萱菁; 可满足性问题（SAT）,最大可满足性问题（MAX-SAT）与最大团问题（MC）都是典型的基本的NP-难解问题。该报告概述了这些难解问题的实验算法方面的国际研究现状和国内研究进展,并对国内外研究进展进行了比较,最后讨论和展望了难解问题求...; 关键词：可满足性最大可满足性最大团问题

一个高效BDD的简洁实现被引量：2: 《计算机学报》2014年第9期2021-2026,共6页苏开乐吕关锋宋炯; 国家“九七三”重点基础研究发展规划项目基金(2010CB328103);国家自然科学基金(60725207)资助~~; 二叉判定图BDD作为一种表示和操作布尔函数的数据结构,被广泛地应用在模型检测、系统验证等领域.在最坏情况下,BDD的空间规模是指数级的,因此为了设计和实现一个高效BDD包,研究者们做了大量技术性工作,同时涌现出多个高效BDD包.为了节...; 关键词：二叉判定图布尔函数内存分配

电子商务支付协议认证性的SVO逻辑验证被引量：7: 《计算机工程与应用》2014年第8期6-10,共5页肖茵茵苏开乐; 国家自然科学基金(No.60903054);国家重点基础研究发展规划(973)(No.2010CB328103);广东高校优秀青年创新人才培育项目(No.LYM11085;No.LYM11084); 与证伪法(如模型检测)相比,采用证真法(如定理证明和逻辑推理)能验证协议在任意会话中的正确性,但分析难度较高,验证过程较为复杂。使用SVO逻辑方法,以Netbill微支付协议为例,对电子商务支付协议的认证性进行形式化分析。扩展了SVO逻辑...; 关键词：SVO逻辑电子商务支付 Netbill协议认证性

实例化空间逻辑下的SET支付协议验证及改进被引量：4: 《华中科技大学学报（自然科学版）》2013年第7期97-102,共6页肖茵茵苏开乐马震远胡若; 国家杰出青年科学基金资助项目(60725207);国家重点基础研究发展计划资助项目(2010CB328103);国家自然科学基金资助项目(60903054);广东省高校优秀青年创新人才培育项目(LYM11085;LYM11084); 使用基于知识推理的实例化空间逻辑及其自动化验证工具SPV对SET支付协议的重要安全性质进行验证,并对协议进行改进.与模型检测法相比,可以验证协议在任意会话中的正确性;与定理证明等方法相比,验证过程是完全自动化的.在不影响原SET支...; 关键词：知识推理安全电子交易支付协议形式化方法实例化空间逻辑自动化验证

可满足赋值算子的设计与实现: 《计算机工程与科学》2010年第9期139-141,168,共4页王倩陈彩吕关锋苏开乐; 在很多应用领域中,我们都需要获取逻辑公式所有无冗余的可满足解集合,即集合中的任意两个解不能互相蕴涵。为了获取无冗余解集合,本文提出了两种实现方案。由于二叉决策图BDD具有对逻辑公式的高效表达特性,因此两种方案都是在逻辑公式...; 关键词：BDD 一致性理论可满足赋值算子

有界模型检测和串空间模型相结合的安全协议验证: 《小型微型计算机系统》2010年第8期1484-1488,共5页杨晋吉苏开乐肖茵茵李超明; 国家杰出青年基金项目(60725207)资助;国家“九七三”重点基础研究发展计划项目(2010CB328103)资助;广东省自然科学基金项目(06023195)资助;广东省科技计划攻关项目(2007B010400068)资助; 提出用BMC和串空间结合的方法对安全协议进行验证.首先是通过串空间的出测试理论先构造不安全协议的部分丛结构,通过该丛结构来约束协议运行的的规模和角色行为;然后用BMC对该丛结构进行建模,建立起对应的有限状态自动机和LTL验证规范,...; 关键词：有界模型检测串空间协议验证 NUSMV

一种求解认知难题的模型检测方法被引量：5: 《计算机学报》2010年第3期406-414,共9页骆翔宇苏开乐顾明; 国家自然科学基金重点项目(90718039);国家"九七三"重点基础研究发展规划项目基金(2010CB328103);国家杰出青年科学基金(60725207);国家自然科学基金(60763004);广西青年科学基金(桂科青0728090);中国博士后科学基金(20090450389)资助; 用公告逻辑建模并求解和与积认知难题.提出一种动态认知模型,将环境认知模型与公告导致的认知模型线性组合,从而在时态认知逻辑模型检测技术中扩展支持公告逻辑的建模与验证.该模型检测方法不仅可以用于搜索认知难题的所有解,而且可以...; 关键词：模型检测 OBDD 公告逻辑时态认知逻辑和与积难题

有界模型检测的优化被引量：10: 《软件学报》2009年第8期2005-2014,共10页杨晋吉苏开乐骆翔宇林瀚肖茵茵; 国家杰出青年基金No.60725207;国家自然科学基金Nos.60473004;60763004;广东省自然科学基金No.06023195;广东省科技攻关项目No.2007B010400068~~; G(p)和G(p→F(q))是有界模型检测(bounded model checking,简称BMC)中的两个重要的常用模态算子.对验证G(p)和G(p→F(q))编码转换公式进行优化.通过分析当验证这些模态算子时FSM(finite state machine)的状态转移和线性时序逻辑(linear-...; 关键词：模型检测有界模型检测可满足性问题模态算子递推公式

利用OBDD编码的快速二值图算法(英文): 《计算机科学与探索》2009年第3期303-308,共6页吕关锋苏开乐陈清亮徐旭东; The National Grand Fundamental Research 973 Program of China under Grant No.2005CB321900;the National Science Foundation for Distinguished Young Scholars of China under Grant No.60725207;the International Joint Research Project of National Science Foundation under Grant No.60911130005;the Start-up Research Fund for Introduced Talents in Jinan University;the Start-up Research Fund for Introduced Talents in Beijing University of Technology;the Discipline and Graduate Education Development Project Fund of Beijing Education Committee;the Distinguished Young Reseacher Nurturing Program in Univeristies of Guangdong under Grant No.LYM08017~~; 对利用有序二元判定图 OBDD 编码二值图像进行了研究,该方法可以节约大量的空间,并在此基础上,提出了各种二值图的算法,包括解码和集合运算(并、交、差、对称差、包含和互补)。实验结果表明这种基于OBDD 编码的方法比现有的二值图编码...; 关键词：有序二元判定图二值图集合运算

高级检索 检索式检索

时间限定

期刊范围

学科限定全选

高级检索 检索式检索

时间限定

期刊范围

学科限定全选

苏开乐

检索结果分析

署名顺序

下载全文

高级检索检索式检索

时间限定

期刊范围

学科限定全选

高级检索 检索式检索

时间限定

期刊范围

学科限定全选

苏开乐

检索结果分析

署名顺序

下载全文

用户登录

高级检索检索式检索