### Resumé

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.

Originalsprog | Engelsk |
---|---|

Tidsskrift | Mathematical Structures in Computer Science |

Vol/bind | 29 |

Udgave nummer | Special Issue 1 |

Sider (fra-til) | 3-37 |

Antal sider | 35 |

ISSN | 0960-1295 |

DOI | |

Status | Udgivet - jan. 2019 |

### Fingerprint

### Citer dette

}

*Mathematical Structures in Computer Science*, bind 29, nr. Special Issue 1, s. 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.

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › 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 -