A quantitative characterization of weighted Kripke structures in temporal logic. (English) Zbl 1413.68073
Summary: 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.
MSC:
68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
03B44 | Temporal logic |
68Q60 | Specification and verification (program logics, model checking, etc.) |