Resumé
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 | Colombia |
| By | Cali |
| Periode | 29/10/2015 → 01/11/2015 |
| Navn | Lecture Notes in Computer Science |
|---|---|
| Nummer | 9399 |
| ISSN | 0302-9743 |
Fingerprint
Citer dette
}
Converging from Branching to Linear Metrics on Markov Chains. / Bacci, Giorgio; Bacci, Giovanni; Larsen, Kim Guldstrand; Mardare, Radu Iulian.
Theoretical Aspects of Computing - ICTAC 2015: 12th International Colloquium, Cali, Colombia, October 29-31, 2015, Proceedings. red. / Martin Leucker; Camilo Rueda; Frank D. Valencia. Springer, 2015. s. 349-367 (Lecture Notes in Computer Science; Nr. 9399).Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Bidrag til bog/antologi › Forskning › peer review
TY - CHAP
T1 - Converging from Branching to Linear Metrics on Markov Chains
AU - Bacci, Giorgio
AU - Bacci, Giovanni
AU - Larsen, Kim Guldstrand
AU - Mardare, Radu Iulian
PY - 2015
Y1 - 2015
N2 - 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.
AB - 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.
U2 - 10.1007/978-3-319-25150-9_21
DO - 10.1007/978-3-319-25150-9_21
M3 - Book chapter
SN - 978-3-319-25149-3
T3 - Lecture Notes in Computer Science
SP - 349
EP - 367
BT - Theoretical Aspects of Computing - ICTAC 2015
A2 - Leucker, Martin
A2 - Rueda, Camilo
A2 - Valencia, Frank D.
PB - Springer
ER -