Keywords:
Quantitative analysis, Weighted Labelled Transition Systems, Point-wise trace distance, point-wise ε-simulation, discoutning, accumulated ε-simulation, weighted HML
Author: Claus Thrane Supervisor: Kim G. Larsen
Abstract:
We introduce, for the purpose of quantitative analysis, a notion of weighted labelled transition systems by extending the traditional notion of labeled transition systems with costs induced by weights and rates associated with transitions and labels. Moreover, we show how basic relations, such as trace equivalence, simulation and bisimulation may be lifted to a setting of quantities where their interpretation is no longer boolean, but instead defines distances, between systems, given as real valued numbers. We introduce two distinct quantitative versions of the relations, one which considers local (point-wise) differences of systems and another, which based on discounting, considers the accumulated difference. We study the properties of the relations, as well as the relationships among these. Finally we present a logical characterization of our simulation based relations, given by a weighted extension of HML.
Download:
Technical report [pdf]
