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.

Keywords

MSC

68Q85, 68Q60, 68N30

Cite this article

@article{cai-11076,
  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  = {29},
  number  = {6+},
  pages   = {1311--1324},
  year    = {2010},
  issn    = {1335-9150},
  url     = {https://cai.type.sk/content/2010/6%2B/a-quantitative-characterization-of-weighted-kripke-structures-in-temporal-logic/}
}
Download .bib