A QUANTITATIVE CHARACTERIZATION OF WEIGHTED KRIPKE STRUCTURES IN TEMPORAL LOGIC
We extend the usual notion of Kripke structures with a weighted transition relation and generalize the classical Boolean interpretation of CTL to a map which assigns to states and temporal formulae a real-valued distance describing the degree of satisfaction. We describe a general approach to obtaining quantitative interpretations for a generic extension of the CTL syntax and show that, for one such interpretation, the logic is both adequate and expressive with respect to quantitative bisimulation.
weighted kripke structures quantitative analysis multi-valued ctl bisimulation distances system metrics