A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic

Authors

  • Uli Fahrenberg
  • Kim G. Larsen
  • Claus Thrane

Keywords:

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

Abstract

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.

Downloads

Download data is not yet available.

Author Biographies

Uli Fahrenberg

Department of Computer Science
Aalborg University
Selma Lagerlofs Vej 300
9220 Aalborg
Denmark

Kim G. Larsen

Department of Computer Science
Aalborg University
Selma Lagerlofs Vej 300
9220 Aalborg
Denmark

Claus Thrane

Department of Computer Science
Aalborg University
Selma Lagerlofs Vej 300
9220 Aalborg
Denmark

Downloads

Published

2012-01-26

How to Cite

Fahrenberg, U., Larsen, K. G., & Thrane, C. (2012). A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic. Computing and Informatics, 29(6+), 1311–1324. Retrieved from http://147.213.75.17/ojs/index.php/cai/article/view/145