### Abstract

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 linear temporal logic (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 non-trivial relation between branching and linear-time metric-based semantics that does not hold in equivalence-based semantics.

Language | English |
---|---|

Pages | 3-37 |

Number of pages | 35 |

Journal | Mathematical Structures in Computer Science |

Volume | 29 |

Issue number | Special Issue 1 |

Early online date | 25 Jul 2017 |

DOIs | |

Publication status | Published - 31 Jan 2019 |

### Fingerprint

### Keywords

- Markov chains
- linear-time metrics
- probabilistic linear temporal logic
- distances
- convergence

### Cite this

*Mathematical Structures in Computer Science*,

*29*(Special Issue 1), 3-37. https://doi.org/10.1017/S0960129517000160

}

*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 › Special issue

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

PY - 2019/1/31

Y1 - 2019/1/31

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 linear temporal logic (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 non-trivial 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 linear temporal logic (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 non-trivial relation between branching and linear-time metric-based semantics that does not hold in equivalence-based semantics.

KW - Markov chains

KW - linear-time metrics

KW - probabilistic linear temporal logic

KW - distances

KW - convergence

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

U2 - 10.1017/S0960129517000160

DO - 10.1017/S0960129517000160

M3 - Special issue

VL - 29

SP - 3

EP - 37

JO - Mathematical Structures in Computer Science

T2 - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

SN - 0960-1295

IS - Special Issue 1

ER -