Converging from Branching to Linear Metrics on Markov Chains

Publikation: Bidrag til bog/antologi/rapport/konference proceedingBidrag til bog/antologiForskningpeer review

11 Citationer (Scopus)

Resumé

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.
OriginalsprogEngelsk
TitelTheoretical Aspects of Computing - ICTAC 2015 : 12th International Colloquium, Cali, Colombia, October 29-31, 2015, Proceedings
RedaktørerMartin Leucker, Camilo Rueda, Frank D. Valencia
Antal sider18
ForlagSpringer
Publikationsdato2015
Sider349-367
ISBN (Trykt)978-3-319-25149-3
ISBN (Elektronisk)978-3-319-25150-9
DOI
StatusUdgivet - 2015
Begivenhed12th International Colloquium on Theoretical Aspects of Computing - Cali, Colombia
Varighed: 29 okt. 20151 nov. 2015
Konferencens nummer: 12

Konference

Konference12th International Colloquium on Theoretical Aspects of Computing
Nummer12
LandColombia
ByCali
Periode29/10/201501/11/2015
NavnLecture Notes in Computer Science
Nummer9399
ISSN0302-9743

Fingerprint

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

Citer dette

Bacci, G., Bacci, G., Larsen, K. G., & Mardare, R. I. (2015). Converging from Branching to Linear Metrics on Markov Chains. I M. Leucker, C. Rueda, & F. D. Valencia (red.), Theoretical Aspects of Computing - ICTAC 2015: 12th International Colloquium, Cali, Colombia, October 29-31, 2015, Proceedings (s. 349-367). Springer. Lecture Notes in Computer Science, Nr. 9399 https://doi.org/10.1007/978-3-319-25150-9_21
Bacci, Giorgio ; Bacci, Giovanni ; Larsen, Kim Guldstrand ; Mardare, Radu Iulian. / Converging from Branching to Linear Metrics on Markov Chains. Theoretical Aspects of Computing - ICTAC 2015: 12th International Colloquium, Cali, Colombia, October 29-31, 2015, Proceedings. red. / Martin Leucker ; Camilo Rueda ; Frank D. Valencia. Springer, 2015. s. 349-367 (Lecture Notes in Computer Science; Nr. 9399).
@inbook{7e55a29bb9114e719ef95ab0193746bc,
title = "Converging from Branching to Linear Metrics on Markov Chains",
abstract = "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.",
author = "Giorgio Bacci and Giovanni Bacci and Larsen, {Kim Guldstrand} and Mardare, {Radu Iulian}",
year = "2015",
doi = "10.1007/978-3-319-25150-9_21",
language = "English",
isbn = "978-3-319-25149-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
number = "9399",
pages = "349--367",
editor = "Martin Leucker and Camilo Rueda and Valencia, {Frank D.}",
booktitle = "Theoretical Aspects of Computing - ICTAC 2015",
address = "Germany",

}

Bacci, G, Bacci, G, Larsen, KG & Mardare, RI 2015, Converging from Branching to Linear Metrics on Markov Chains. i M Leucker, C Rueda & FD Valencia (red), Theoretical Aspects of Computing - ICTAC 2015: 12th International Colloquium, Cali, Colombia, October 29-31, 2015, Proceedings. Springer, Lecture Notes in Computer Science, nr. 9399, s. 349-367, 12th International Colloquium on Theoretical Aspects of Computing , Cali, Colombia, 29/10/2015. https://doi.org/10.1007/978-3-319-25150-9_21

Converging from Branching to Linear Metrics on Markov Chains. / Bacci, Giorgio; Bacci, Giovanni; Larsen, Kim Guldstrand; Mardare, Radu Iulian.

Theoretical Aspects of Computing - ICTAC 2015: 12th International Colloquium, Cali, Colombia, October 29-31, 2015, Proceedings. red. / Martin Leucker; Camilo Rueda; Frank D. Valencia. Springer, 2015. s. 349-367 (Lecture Notes in Computer Science; Nr. 9399).

Publikation: Bidrag til bog/antologi/rapport/konference proceedingBidrag til bog/antologiForskningpeer review

TY - CHAP

T1 - Converging from Branching to Linear Metrics on Markov Chains

AU - Bacci, Giorgio

AU - Bacci, Giovanni

AU - Larsen, Kim Guldstrand

AU - Mardare, Radu Iulian

PY - 2015

Y1 - 2015

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

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

U2 - 10.1007/978-3-319-25150-9_21

DO - 10.1007/978-3-319-25150-9_21

M3 - Book chapter

SN - 978-3-319-25149-3

T3 - Lecture Notes in Computer Science

SP - 349

EP - 367

BT - Theoretical Aspects of Computing - ICTAC 2015

A2 - Leucker, Martin

A2 - Rueda, Camilo

A2 - Valencia, Frank D.

PB - Springer

ER -

Bacci G, Bacci G, Larsen KG, Mardare RI. Converging from Branching to Linear Metrics on Markov Chains. I Leucker M, Rueda C, Valencia FD, red., Theoretical Aspects of Computing - ICTAC 2015: 12th International Colloquium, Cali, Colombia, October 29-31, 2015, Proceedings. Springer. 2015. s. 349-367. (Lecture Notes in Computer Science; Nr. 9399). https://doi.org/10.1007/978-3-319-25150-9_21