A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic
Uli Fahrenberg ; Kim G. Larsen ; Claus Thrane
Computing and Informatics, Tome 28 (2012) no. 1, / Harvested from Computing and Informatics
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.
Publié le : 2012-01-26
Classification:  Quantitative analysis; multi-valued CTL; weighted Kripke structures; bisimulation distances; system metrics
@article{cai145,
     author = {Uli Fahrenberg and Kim G. Larsen and Claus Thrane},
     title = {A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic},
     journal = {Computing and Informatics},
     volume = {28},
     number = {1},
     year = {2012},
     language = {en},
     url = {http://dml.mathdoc.fr/item/cai145}
}
Uli Fahrenberg; Kim G. Larsen; Claus Thrane. A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic. Computing and Informatics, Tome 28 (2012) no. 1, . http://gdmltest.u-ga.fr/item/cai145/