## 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 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.

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 |