Converging from branching to linear metrics on Markov chains

Research output: Contribution to journalJournal articleResearchpeer-review

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.
Original languageEnglish
JournalMathematical Structures in Computer Science
Volume29
Issue numberSpecial Issue 1
Pages (from-to)3-37
Number of pages35
ISSN0960-1295
DOIs
Publication statusPublished - Jan 2019

Fingerprint

Markov processes
Branching
Markov chain
Semantics
Linear Time
Metric
Model checking
Polynomials
Pseudometric
Probabilistic Model
Model Checking
Schema
Polynomial time
Exceed
NP-complete problem
Trace
Equivalence
Converge
Approximation
Operator

Bibliographical note

Special Issue: Best Papers Presented at ICTAC 2015.

Cite this

@article{844e94cb75cd470db47bc3da95154fef,
title = "Converging from branching to linear metrics on Markov chains",
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.",
author = "Giorgio Bacci and Giovanni Bacci and Larsen, {Kim G.} and Radu Mardare",
note = "Special Issue: Best Papers Presented at ICTAC 2015.",
year = "2019",
month = "1",
doi = "10.1017/S0960129517000160",
language = "English",
volume = "29",
pages = "3--37",
journal = "Mathematical Structures in Computer Science",
issn = "0960-1295",
publisher = "Cambridge University Press",
number = "Special Issue 1",

}

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

In: Mathematical Structures in Computer Science, Vol. 29, No. Special Issue 1, 01.2019, p. 3-37.

Research output: Contribution to journalJournal articleResearchpeer-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 -