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

Lattice-valued Language Containment Relation for Quantitative Transition Systems

近十年来,量化形式化验证方法的研究取得了很多的研究成果。量化转换系统是一种新型的量化模型,该模型的主要特点是其动作集合上被赋予一个基于完备剩余格的格值等价关系。在量化转换系统的模型上,本文提出了一种格值语言包含关系去度量系统的一个状态所接受的语言能在多大程度上被另一个状态所接受的语言所包含,研究了这种关系的计算复杂性问题,并用格值版本的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.