### Abstract

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.

Original language | English |
---|---|

Title of host publication | Theoretical Aspects of Computing - ICTAC 2015 : 12th International Colloquium, Cali, Colombia, October 29-31, 2015, Proceedings |

Editors | Martin Leucker, Camilo Rueda, Frank D. Valencia |

Number of pages | 18 |

Publisher | Springer |

Publication date | 2015 |

Pages | 349-367 |

ISBN (Print) | 978-3-319-25149-3 |

ISBN (Electronic) | 978-3-319-25150-9 |

DOIs | |

Publication status | Published - 2015 |

Event | 12th International Colloquium on Theoretical Aspects of Computing - Cali, Colombia Duration: 29 Oct 2015 → 1 Nov 2015 Conference number: 12 |

### Conference

Conference | 12th International Colloquium on Theoretical Aspects of Computing |
---|---|

Number | 12 |

Country | Colombia |

City | Cali |

Period | 29/10/2015 → 01/11/2015 |

Series | Lecture Notes in Computer Science |
---|---|

Number | 9399 |

ISSN | 0302-9743 |

### Fingerprint

### Cite this

*Theoretical Aspects of Computing - ICTAC 2015: 12th International Colloquium, Cali, Colombia, October 29-31, 2015, Proceedings*(pp. 349-367). Springer. Lecture Notes in Computer Science, No. 9399 https://doi.org/10.1007/978-3-319-25150-9_21

}

*Theoretical Aspects of Computing - ICTAC 2015: 12th International Colloquium, Cali, Colombia, October 29-31, 2015, Proceedings.*Springer, Lecture Notes in Computer Science, no. 9399, pp. 349-367, 12th International Colloquium on Theoretical Aspects of Computing , Cali, Colombia, 29/10/2015. https://doi.org/10.1007/978-3-319-25150-9_21

**Converging from Branching to Linear Metrics on Markov Chains.** / Bacci, Giorgio; Bacci, Giovanni; Larsen, Kim Guldstrand; Mardare, Radu Iulian.

Research output: Contribution to book/anthology/report/conference proceeding › Book chapter › Research › 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 -