A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic
Keywords:Quantitative analysis, multi-valued CTL, weighted Kripke structures, bisimulation distances, system metrics
AbstractWe 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.
Download data is not yet available.
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 https://www.cai.sk/ojs/index.php/cai/article/view/145