A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic

In: Computing and Informatics, vol. 29, no. 6+

U. Fahrenberg - K. G. Larsen - C. Thrane

Details:

Year, pages: 2010, 1311 - 1324

Keywords:

Quantitative analysis, multi-valued CTL, weighted Kripke structures, bisimulation distances, system metrics

About article:

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.

How to cite:

ISO 690:

Fahrenberg, U., G. Larsen, K., Thrane, C. 2010. A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic. In Computing and Informatics, vol. 29, no.6+, pp. 1311-1324. 1335-9150.

APA:

Fahrenberg, U., G. Larsen, K., Thrane, C. (2010). A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic. Computing and Informatics, 29(6+), 1311-1324. 1335-9150.