### Abstract

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 bisimilarity-like pseudometrics (hence, branching-time distances) that converge point-wise to the linear-time metrics. This convergence is interesting in itself, because it reveals a nontrivial relation between branching and linear-time metric-based semantics that does not hold in equivalence-based semantics.

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

Journal | Mathematical Structures in Computer Science |

Volume | 29 |

Issue number | Special Issue 1 |

Pages (from-to) | 3-37 |

Number of pages | 35 |

ISSN | 0960-1295 |

DOIs | |

Publication status | Published - Jan 2019 |

### Fingerprint

### Bibliographical note

Special Issue: Best Papers Presented at ICTAC 2015.### Cite this

}

*Mathematical Structures in Computer Science*, vol. 29, no. Special Issue 1, pp. 3-37. https://doi.org/10.1017/S0960129517000160

**Converging from branching to linear metrics on Markov chains.** / Bacci, Giorgio; Bacci, Giovanni; Larsen, Kim G.; Mardare, Radu.

Research output: Contribution to journal › Journal article › Research › peer-review

TY - JOUR

T1 - Converging from branching to linear metrics on Markov chains

AU - Bacci, Giorgio

AU - Bacci, Giovanni

AU - Larsen, Kim G.

AU - Mardare, Radu

N1 - Special Issue: Best Papers Presented at ICTAC 2015.

PY - 2019/1

Y1 - 2019/1

N2 - We study two well known linear-time metrics on Markov chains (MCs), namely, the strong and strutter trace distances. 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-X (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 bisimilarity-like pseudometrics (hence, branching-time distances) that converge point-wise to the linear-time metrics. This convergence is interesting in itself, because it reveals a nontrivial relation between branching and linear-time metric-based semantics that does not hold in equivalence-based semantics.

AB - We study two well known linear-time metrics on Markov chains (MCs), namely, the strong and strutter trace distances. 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-X (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 bisimilarity-like pseudometrics (hence, branching-time distances) that converge point-wise to the linear-time metrics. This convergence is interesting in itself, because it reveals a nontrivial relation between branching and linear-time metric-based semantics that does not hold in equivalence-based semantics.

UR - http://www.scopus.com/inward/record.url?scp=85026515483&partnerID=8YFLogxK

U2 - 10.1017/S0960129517000160

DO - 10.1017/S0960129517000160

M3 - Journal article

VL - 29

SP - 3

EP - 37

JO - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

SN - 0960-1295

IS - Special Issue 1

ER -