Analyzing quantitative transition systems

Abstract

During the past years, substantial progress has been made towards developing quantitative formal verification methods. In this paper, we establish a lattice-valued relation between the states of a quantitative transition system(QTS), called lattice-valued language containment relation, to measure towhat extent the language of one state is included by that of the other.We study the relationship between lattice-valued language containment relation and two lattice-valued versions of similarity defined previously, and we explore the properties of compositionality of the lattice-valued language containment relation. These properties suggest that our language containment relation provides an appropriate basis for a quantitative theory of concurrent and distributed systems.