Converging from Branching to Linear Metrics on Markov Chains

Research output: Contribution to book/anthology/report/conference proceedingBook chapterResearchpeer-review

16 Citations (Scopus)


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.
Original languageEnglish
Title of host publicationTheoretical Aspects of Computing - ICTAC 2015 : 12th International Colloquium, Cali, Colombia, October 29-31, 2015, Proceedings
EditorsMartin Leucker, Camilo Rueda, Frank D. Valencia
Number of pages18
Publication date2015
ISBN (Print)978-3-319-25149-3
ISBN (Electronic)978-3-319-25150-9
Publication statusPublished - 2015
Event12th International Colloquium on Theoretical Aspects of Computing - Cali, Colombia
Duration: 29 Oct 20151 Nov 2015
Conference number: 12


Conference12th International Colloquium on Theoretical Aspects of Computing
SeriesLecture Notes in Computer Science


Dive into the research topics of 'Converging from Branching to Linear Metrics on Markov Chains'. Together they form a unique fingerprint.

Cite this