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.
| Original language | English |
|---|---|
| Title of host publication | Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science |
| Publisher | Schloss Dagstuhl. Leibniz-Zentrum für Informatik |
| Publication date | 2009 |
| ISBN (Print) | 978-3-939897-15-6 |
| Publication status | Published - 2009 |
| Event | Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09) - Znojmo, Czech Republic Duration: 13 Nov 2009 → 15 Nov 2009 |
Conference
| Conference | Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09) |
|---|---|
| Country/Territory | Czech Republic |
| City | Znojmo |
| Period | 13/11/2009 → 15/11/2009 |
Keywords
- quantitative analysis
- Kripke structures
- charasteristic formula
- bisimulation distance
- weighted CTL