导读:本文包含了互模拟等价论文开题报告文献综述及选题提纲参考文献，主要关键词:形式化方法,互模拟等价,RDF图
互模拟等价论文文献综述
雷国庆[1]（2018）在《互模拟等价验证算法的比较与应用》一文中研究指出随着计算机科学的发展,形式化验证方法在软件和硬件领域的应用越来越广泛。互模拟等价关系是形式化方法中的一个重要概念,它表示两个转移系统之间的等价关系,当两个系统互模拟等价时,它们可以相互模拟彼此的动作。互模拟等价关系对并发系统的验证与分析具有重要作用,比如:两个转移系统满足相同的CTL(计算树逻辑)和CTL*公式当且仅当它们是互模拟等价的。互模拟等价验证算法可以分为局部算法和全局算法。本文主要研究这两类算法。本文的主要贡献如下所示:(1)对局部算法以及准局部算法的实现过程进行了优化,比较了它们的运行效率。之后,通过对标号转移系统的饱和处理将这两种算法推广到了弱互模拟等价的验证问题中。(2)实现并比较全局算法。全局算法的核心思想就是划分等价类,本文详细解释了这一思想的发展和演变过程。算法在一个初始分类的基础上对等价类不断地进行分割精化,直到满足如下条件:(1)所有互模拟的状态都属于同一等价类(2)一个等价类内的所有状态都是互模拟的。之后重点介绍了时间复杂度为O(mlogn)的Valmari算法,并分别用Java和C++实现了算法,然后将这两种版本的算法和CADP工具进行了比较。(3)全局算法的应用。上文提到的Valmari算法也是一种互模拟压缩算法,本文分别实现了由Valmari和Alexander Sch?tzle提出的两种互模拟压缩算法,并将其应用于知识图谱的互模拟压缩问题中,比较了两种算法的运行效果。根据实验数据可知,在PC平台上处理百万级规模的数据时可选择基于内存的Antti Valmari算法,在服务器的数据库中处理更大规模数据时可选择基于外存的Alexander Sch?tzle算法。(本文来源于《华东师范大学》期刊2018-04-01）
黄镇谨,陆阳,杨娟,王智文[2]（2016）在《连续时间Markov决策过程互模拟等价及逻辑保持》一文中研究指出模型检测中,Markov决策过程可以建模具有不确定性的系统,然而状态空间爆炸问题将会影响系统验证的成败与效率,互模拟等价可以用于系统状态的简约.在强互模拟关系的基础上,给出Markov决策过程模型弱互模拟等价关系的概念,导出了连续时间Markov决策过程及其内嵌离散时间Markov决策过程互模拟等价关系的内在联系;在强互模拟等价关系逻辑特征保持的基础上,给出弱互模拟等价关系下的逻辑保持性质,证明了弱互模拟等价的两个状态,同时满足除下一步算子外的连续随机逻辑公式,从而可以将原模型中的验证问题转换为简约后模型的验证问题,提高验证的效率.(本文来源于《控制理论与应用》期刊2016年08期）
杜平,姚从军[3]（2013）在《互模拟及其与模态等价之间的关系》一文中研究指出互模拟已成为模态逻辑模型论的一个核心概念。笔者在克里普克模型上定义了互模拟和互模拟不变性概念,接着证明模态逻辑具有互模拟不变性,最后讨论了互模拟与模态等价之间的关系。(本文来源于《毕节学院学报》期刊2013年08期）
钮俊,曾国荪,王伟[4]（2013）在《绿色评价模型的互模拟等价及逻辑保持》一文中研究指出绿色计算中,复杂系统的绿色评价是一个重要的研究课题,其核心任务是判断运行时时间、空间资源消耗是否满足环境约束或限定.设计时,采用模型检测技术,自动、完备、高效地进行绿色评价,是一种新颖且有效的解决方案,但可能出现的状态爆炸问题将影响评价成败或效率.引入随机决策过程作为绿色评价模型;用时态逻辑刻画包含行为正确性及时间、空间资源约束的绿色评价指标;定义不确定语义理解下评价模型状态的互模拟等价规则,给出互模拟商的构造方法以及商模型调度,并比较等价语义下的行为机理;运用结构化归纳法证明互模拟等价保持评价结论.分析表明,互模拟等价可用作状态约简手段,为基于模型的绿色评价提供理论支撑和技术手段.(本文来源于《计算机学报》期刊2013年05期）
邓辉,吴尽昭[5]（2013）在《线性半代数变迁系统的近似互模拟等价》一文中研究指出针对软件程序状态间转移关系存在不等式约束的问题,给出一种形式化的程序描述系统,即线性半代数变迁系统。在该系统的基础上,为简化软件程序结构,采用特征列的方法,提出了基于线性半代数系统共同零点的互模拟等价概念及计算方法。但在工程应用中大多数实验所得数据仅为给定误差范围内的近似值,精确的系统等价关系缺乏容错性及灵活性。为获得更恰当的系统关系,利用奇异值分解对系统进行近似处理,建立了系统的近似互模拟等价概念及计算方法。通过符号与数值混合计算,实现误差可计算及可控制。最终选取近似等价系统代替原复杂系统。并发通信程序中的实例分析表明,该方法在简化软件程序设计中具有合理性及有效性。(本文来源于《吉林大学学报(工学版)》期刊2013年04期）
李天冶[6]（2012）在《多目Pi演算互模拟等价自动验证研究》一文中研究指出本文通过对多目Pi演算的强开互模拟等价自动化验证算法的研究，针对已有算法中存在大量的递归调用、冗余数据、执行效率低等问题，建立了一套全新的数据结构用来表示多目Pi演算算式，并在此基础之上提出了对已有算法的优化建议。在多目Pi演算的强开互模拟等价自动化验证优化算法中，提出了一种新的算法执行方案，对算法中关键的Add方法和Match方法做出了修正，使得算法在处理拥有大量的并行与选择、抽象与凝结因子的多目Pi演算算式的时候，算法递归深度大量减少。同时对算法中的二元关系R和D的处理做出了修正，使得算法运行过程中的冗余数据大量减少，算法执行效率得到了优化。另外，本文还讨论了多目Pi演算的α等价与其强开互模拟等价验证之间的关系，并提出并实现了一个可行的α等价验证算法，使得算法整体的递归深度进一步减少，同时α等价验证算法也可以作为一个独立的功能呈现。(本文来源于《吉林大学》期刊2012-04-01）
邓辉,吴尽昭[7]（2011）在《多项式程序模型的互模拟等价》一文中研究指出针对程序的行为等价性,提出多项式程序模型的互模拟等价,适用于代数程序模型描述的软件系统设计和验证分析.给出多项式程序模型互模拟等价概念,建立互模拟等价的符号计算方法,选取结构简单的模型,简化程序设计,缓解状态爆炸导致的形式化验证方法计算复杂度过高而难于实现的问题.最后给出并发程序的相关实例.(本文来源于《北京交通大学学报》期刊2011年05期）
颜锋,田作威,严榴香[8]（2010）在《多态π演算的互模拟等价关系及其公理化》一文中研究指出类型系统在分布式系统理论中有着非常重要的作用。在为π演算引入多态类型系统后,需要对新的环境下进程的等价关系进行研究。在多态类型系统下,环境只能得知进程中通道的抽象类型,而无法得知通道的具体类型,此时环境的区分能力被削弱,所得到的互模拟关系更为粗糙。本文在以往文献研究的基础上给出了多态π演算互模拟的一个公理系统,并证明了公理系统的一致性和完备性。(本文来源于《计算机工程与科学》期刊2010年10期）
姚从军[9]（2010）在《同构、P-态射、互模拟与模态等价性》一文中研究指出结构的模态等价性是指这些结构上有效性的模态公式恰好相同。本文比较了模型之间的叁类关系:同构、P-态射、互模拟,从而得出互模拟关系概括了最大范围的模态等价性,因为模型之间的互模拟关系包含它们之间的同构关系和P-态射关系。同时,对框架等价性也给予了一定的研究,得出结论是:同构的框架一定是模态等价的,但具有另外两种关系的框架不一定是模态等价的。(本文来源于《西南大学学报(社会科学版)》期刊2010年02期）
吕银华[10]（2006）在《安全协议中的互模拟等价性验证》一文中研究指出随着信息服务和商业活动等越来越多地出现在开放的通讯网络上，用以保证上述服务的网络安全协议的可靠性成为备受人们关注的焦点。然而，由于外部面临恶劣的网络环境和内部缺乏系统化设计验证方法，网络安全协议变得非常脆弱和容易出错。 形式化的方法为验证和分析安全协议提供了有效的途径。它用形式化的语言抽象出复杂的密文通讯协议，并借助于高级的推理或证明系统实现协议的分析验证。建立在进程演算基础之上的互模拟等价性验证的方法，由于具有能确切地刻画协议运行的代数语义模型(Spi演算)和十分有效的等价性验证方法而成为近年来研究的热点。然后，Spi演算模型中还存在某些不足，更重要的是基于原有的互模拟关系的方法仅限于人工完成，不能实现自动验证。 我们的工作是针对上述不足之处展开的，目标是扩充Spi演算语言，在此基础上建立新型的互模拟等价关系，并实现该关系的自动证明，从而设计出安全协议互模拟等价性自动验证工具。主要研究内容和创新之处在于以下叁点： 1)扩充Spi演算语言，为密文通讯协议建立了新型Spi演算模型。扩充Spi演算语法，建立了公钥密码操作原语，使之能表示所有密钥体制的安全协议；修改了Spi演算中并发语义，限制了原先通道可以传递的机制，使之能描述协议中通讯主体跟其环境直接交互，从而可以更确切地刻画现实中的安全协议； 2)在新Spi演算里设计了符号操作语义和符号互模拟。我们的符号操作语义使输入进程仅接收环境中有意义的带符号的消息项，这样就很好地解决了输入进程可能产生的无穷分支问题。定义的符号Refed互模拟确保了两个进程只需要执行有限次的迁移动作，就可以判断出它们是否互模拟； 3)建立并证明了符号Reefed互模拟与原具体互模拟之间的可靠性关系，从而可以设计安全协议的互模拟等价性验证工具。 基于这项工作，可以实现安全协议的互模拟等价关系的自动验证，我们相信这对于应用在软件和集成电路中的自动检测也有很大的启发作用。本文最后做出了全文总结，并对本领域未来的研究提出了新的展望。(本文来源于《贵州大学》期刊2006-05-01）
互模拟等价论文开题报告
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
模型检测中,Markov决策过程可以建模具有不确定性的系统,然而状态空间爆炸问题将会影响系统验证的成败与效率,互模拟等价可以用于系统状态的简约.在强互模拟关系的基础上,给出Markov决策过程模型弱互模拟等价关系的概念,导出了连续时间Markov决策过程及其内嵌离散时间Markov决策过程互模拟等价关系的内在联系;在强互模拟等价关系逻辑特征保持的基础上,给出弱互模拟等价关系下的逻辑保持性质,证明了弱互模拟等价的两个状态,同时满足除下一步算子外的连续随机逻辑公式,从而可以将原模型中的验证问题转换为简约后模型的验证问题,提高验证的效率.
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
互模拟等价论文参考文献
[1].雷国庆.互模拟等价验证算法的比较与应用[D].华东师范大学.2018
[2].黄镇谨,陆阳,杨娟,王智文.连续时间Markov决策过程互模拟等价及逻辑保持[J].控制理论与应用.2016
[3].杜平,姚从军.互模拟及其与模态等价之间的关系[J].毕节学院学报.2013
[4].钮俊,曾国荪,王伟.绿色评价模型的互模拟等价及逻辑保持[J].计算机学报.2013
[5].邓辉,吴尽昭.线性半代数变迁系统的近似互模拟等价[J].吉林大学学报(工学版).2013
[6].李天冶.多目Pi演算互模拟等价自动验证研究[D].吉林大学.2012
[7].邓辉,吴尽昭.多项式程序模型的互模拟等价[J].北京交通大学学报.2011
[8].颜锋,田作威,严榴香.多态π演算的互模拟等价关系及其公理化[J].计算机工程与科学.2010
[9].姚从军.同构、P-态射、互模拟与模态等价性[J].西南大学学报(社会科学版).2010
[10].吕银华.安全协议中的互模拟等价性验证[D].贵州大学.2006