A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic
Uli Fahrenberg, Kim G. Larsen, Claus Thrane · VBN Forskningsportal (Aalborg Universitet) · 2012
Abstract. We extend the usual notion of Kripke structures with a weighted tran-sition 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 in-terpretations 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.