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

Lattice-valued Language Containment Relation for Quantitative Transition Systems

作　　者：汪国武[1,2] 沈应兄[3] 潘海玉[3,4] 

机构地区：[1]安徽工程大学计算机与信息学院,安徽芜湖241000 [2]安徽工程大学计算机应用技术重点实验室,安徽芜湖241000 [3]泰州学院计算机科学与技术学院,江苏泰州225300 [4]陕西师范大学计算机科学学院,陕西西安710062

出　　处：《模糊系统与数学》2016年第5期50-59,共10页Fuzzy Systems and Mathematics

基　　金：国家自然科学基金(11301321;11401361;61672023;61673352);中国博士后科学基金资助项目(2014M552408);安徽省自然科学基金(2013SQRL034ZD;TSKJ2016B02)

摘　　要：近十年来,量化形式化验证方法的研究取得了很多的研究成果。量化转换系统是一种新型的量化模型,该模型的主要特点是其动作集合上被赋予一个基于完备剩余格的格值等价关系。在量化转换系统的模型上,本文提出了一种格值语言包含关系去度量系统的一个状态所接受的语言能在多大程度上被另一个状态所接受的语言所包含,研究了这种关系的计算复杂性问题,并用格值版本的HennessyMilner逻辑的子逻辑提供了它的逻辑刻画。所有这些性质表明所提出的格值语言包含关系为并发和分布式系统的量化验证提供了重要的理论基础。During the past years, substantial progress has been made towards developing quantitative formal verification methods. In this paper,we present a lattice-valued relation between the states of a quantitative transition system whose actions are equipped with a complete residuated lattice--valued equality relation, called lattice-valued language containment relation, to measure to what extent the language of one state is included by that of the other. Then we provide an algorithm for computing the lattice-valued language containment relation over quantitative transition system,and establish a logical characterization of lattice-valued language containment relation in terms of lattice-valued version of a fragment of Hennessy-Milner logic. These properties suggest that our language containment relation provides an appropriate basis for a quantitative theory of concurrent and distributed systems.

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

分 类 号：O141[理学—数学] O159[理学—基础数学]