DROPS.MEMICS.2009.2345.pdf
- Filesize: 0.56 MB
- 8 pages
Document
A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic
Authors
-
Part of:
Volume:
Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09) (MEMICS 2009)
Series: Open Access Series in Informatics (OASIcs) - License:
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
- Publication Date: 2009-12-15
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)
https://doi.org/10.4230/DROPS.MEMICS.2009.2345
https://doi.org/10.4230/DROPS.MEMICS.2009.2345
Abstract
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.
Keywords
- Quantitative analysis
- Kripke structures
- characteristic formulae
- bisimulation distance
- weighted CTL
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads