量化转换系统的格值语言包含关系

摘要：

近十年来,量化形式化验证方法的研究取得了很多的研究成果.量化转换系统是一种新型的量化模型,该模型的主要特点是其动作集合上被赋予一个基于完备剩余格的格值等价关系.在量化转换系统的模型上,本文提出了一种格值语言包含关系去度量系统的一个状态所接受的语言能在多大程度上被另一个状态所接受的语言所包含,研究了这种关系的计算复杂性问题,并用格值版本的Hennessy-Milner逻辑的子逻辑提供了它的逻辑刻画.所有这些性质表明所提出的格值语言包含关系为并发和分布式系统的量化验证提供了重要的理论基础.

关键词：标号转换系统、形式化验证、Hennessy-Milner逻辑、模糊自动机、完备剩余格

所属期刊栏目：30

分类号：O141;O159(数理逻辑、数学基础)

资助基金：国家自然科学基金;国家自然科学基金;国家自然科学基金;国家自然科学基金;中国博士后科学基金;安徽省自然科学基金;安徽省自然科学基金

在线出版日期：2017-03-31（万方平台首次上网日期，不代表论文的发表时间）

页码：50-59