Projekter pr. år
Abstract
We study the strong and strutter trace distances on Markov chains (MCs). Our interest in these metrics is motivated by their relation to the probabilistic LTL-model checking problem: we prove that they correspond to the maximal differences in the probability of satisfying the same LTL and LTL-헑 ( LTL without next operator) formulas, respectively. The threshold problem for these distances (whether their value exceeds a given threshold) is NP-hard and not known to be decidable. Nevertheless, we provide an approximation schema where each lower and upper-approximant is computable in polynomial time in the size of the MC.
The upper-approximants are Kantorovich-like pseudometrics, i.e. branching-time distances, that converge point-wise to the linear-time metrics. This convergence is interesting in itself, since it reveals a nontrivial relation between branching and linear-time metric-based semantics that does not hold in the case of equivalence-based semantics.
The upper-approximants are Kantorovich-like pseudometrics, i.e. branching-time distances, that converge point-wise to the linear-time metrics. This convergence is interesting in itself, since it reveals a nontrivial relation between branching and linear-time metric-based semantics that does not hold in the case of equivalence-based semantics.
Originalsprog | Engelsk |
---|---|
Titel | Theoretical Aspects of Computing - ICTAC 2015 : 12th International Colloquium, Cali, Colombia, October 29-31, 2015, Proceedings |
Redaktører | Martin Leucker, Camilo Rueda, Frank D. Valencia |
Antal sider | 18 |
Forlag | Springer |
Publikationsdato | 2015 |
Sider | 349-367 |
ISBN (Trykt) | 978-3-319-25149-3 |
ISBN (Elektronisk) | 978-3-319-25150-9 |
DOI | |
Status | Udgivet - 2015 |
Begivenhed | 12th International Colloquium on Theoretical Aspects of Computing - Cali, Colombia Varighed: 29 okt. 2015 → 1 nov. 2015 Konferencens nummer: 12 |
Konference
Konference | 12th International Colloquium on Theoretical Aspects of Computing |
---|---|
Nummer | 12 |
Land/Område | Colombia |
By | Cali |
Periode | 29/10/2015 → 01/11/2015 |
Navn | Lecture Notes in Computer Science |
---|---|
Nummer | 9399 |
ISSN | 0302-9743 |
Fingeraftryk
Dyk ned i forskningsemnerne om 'Converging from Branching to Linear Metrics on Markov Chains'. Sammen danner de et unikt fingeraftryk.Projekter
- 3 Afsluttet
-
CASSTING: Collective Adaptive System SynThesIs using Non-zero-sum Games
Larsen, K. G., Skou, A., David, A. & Srba, J.
01/04/2013 → 31/03/2016
Projekter: Projekt › Forskning
-
SENSATION: Self Energy-Supporting Autonomous Computation
Larsen, K. G., Hansen, R. R., Koch, P., Nielsen, B. & Skou, A.
01/10/2012 → 30/09/2015
Projekter: Projekt › Forskning
-
IDEA4CPS: Foundations for Cyber-Physical Sytems
Larsen, K. G., Skou, A., Nielsen, B., Bulychev, P., Ravn, A. P. & Poulsen, D. B.
01/04/2011 → 30/04/2015
Projekter: Projekt › Forskning