We present a general framework for the analysis of quantitative and qualitative properties of reactive systems, based on a notion of weighted transition systems. We introduce and analyze three different types of distances on weighted transition systems, both in a linear and a branching version. Our quantitative notions appear to be reasonable extensions of the standard qualitative concepts, and the three different types introduced are shown to measure inequivalent properties. When applied to the formalism of weighted timed automata, we show that some standard decidability and undecidability results for timed automata extend to our quantitative setting. Key words: Quantitative analysis, weighted transition systems, weighted timed automata, simulation, trace inclusion, hemimetrics
Claus R. Thrane, Uli Fahrenberg, Kim G. Larsen