Lattice-valued simulations for quantitative transition systems

• Introduced an extension of labeled transition systems called quantitative transition systems.
• Presented an approximate similarity between states of quantitative transition systems.
• Discussed the fixed point and logical characterizations of approximate similarity.

Quantitative (bi)simulations taking values from non-negative real numbers enjoy numerous applications in the analysis of labeled transition systems, whose transitions, states, or labels contain quantitative information. To investigate the simulation semantics of labeled transition systems in the residuated lattice-valued logic setting, we introduce an extension of labeled transition systems, called the quantitative transition systems (QTSs), whose labels are equipped with a residuated lattice-valued equality relation. We then establish a lattice-valued relation between states of a QTS, called approximate similarity, to quantify to what extent one state is simulated by another. One main contribution of this paper is to show that unlike the classic setting where similarity has both fixed point and logical characterizations, these results do not hold for approximate similarity on QTSs in general, but they hold for QTSs having truth values from finite Heyting algebras.