A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic

Authors Kim G. Larsen, Uli Fahrenberg, Claus Thrane

Thumbnail PDF


  • Filesize: 0.56 MB
  • 8 pages

Document Identifiers

Author Details

Kim G. Larsen
Uli Fahrenberg
Claus Thrane

Cite AsGet BibTex

Kim G. Larsen, Uli Fahrenberg, and Claus Thrane. A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 10-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)


We extend the usual notion of Kripke Structures with a weighted transition relation, and generalize the usual Boolean satisfaction relation 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.
  • Quantitative analysis
  • Kripke structures
  • characteristic formulae
  • bisimulation distance
  • weighted CTL


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail