Converging from Branching to Linear Metrics on Markov Chains

Giorgio Bacci; Giovanni Bacci; Kim Guldstrand Larsen; Radu Iulian Mardare

doi:10.1007/978-3-319-25150-9_21

Converging from Branching to Linear Metrics on Markov Chains

Giorgio Bacci, Giovanni Bacci, Kim Guldstrand Larsen, Radu Iulian Mardare

Research output: Contribution to book/anthology/report/conference proceeding › Book chapter › Research › peer-review

16 Citations (Scopus)

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.

Original language	English
Title of host publication	Theoretical Aspects of Computing - ICTAC 2015 : 12th International Colloquium, Cali, Colombia, October 29-31, 2015, Proceedings
Editors	Martin Leucker, Camilo Rueda, Frank D. Valencia
Number of pages	18
Publisher	Springer
Publication date	2015
Pages	349-367
ISBN (Print)	978-3-319-25149-3
ISBN (Electronic)	978-3-319-25150-9
DOIs	https://doi.org/10.1007/978-3-319-25150-9_21
Publication status	Published - 2015
Event	12th International Colloquium on Theoretical Aspects of Computing - Cali, Colombia Duration: 29 Oct 2015 → 1 Nov 2015 Conference number: 12

Conference

Conference	12th International Colloquium on Theoretical Aspects of Computing
Number	12
Country/Territory	Colombia
City	Cali
Period	29/10/2015 → 01/11/2015

Series	Lecture Notes in Computer Science
Number	9399
ISSN	0302-9743

Access to Document

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

AUB Link

Search for the material in Aalborg University Library's search engine

CASSTING: Collective Adaptive System SynThesIs using Non-zero-sum Games
Larsen, K. G., Skou, A., David, A. & Srba, J.
FP7 STREP
01/04/2013 → 31/03/2016
Project: Research
SENSATION: Self Energy-Supporting Autonomous Computation
Larsen, K. G., Hansen, R. R., Koch, P., Nielsen, B. & Skou, A.
FP7 FET Proactive
01/10/2012 → 30/09/2015
Project: Research
IDEA4CPS: Foundations for Cyber-Physical Sytems
Larsen, K. G., Skou, A., Nielsen, B., Bulychev, P., Ravn, A. P. & Poulsen, D. B.
01/04/2011 → 30/04/2015
Project: Research

Cite this

Bacci, G., Bacci, G., Larsen, K. G., & Mardare, R. I. (2015). Converging from Branching to Linear Metrics on Markov Chains. In M. Leucker, C. Rueda, & F. D. Valencia (Eds.), Theoretical Aspects of Computing - ICTAC 2015: 12th International Colloquium, Cali, Colombia, October 29-31, 2015, Proceedings (pp. 349-367). Springer. https://doi.org/10.1007/978-3-319-25150-9_21

Bacci, Giorgio ; Bacci, Giovanni ; Larsen, Kim Guldstrand et al. / 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. editor / Martin Leucker ; Camilo Rueda ; Frank D. Valencia. Springer, 2015. pp. 349-367 (Lecture Notes in Computer Science; No. 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",

note = "12th International Colloquium on Theoretical Aspects of Computing , ICTAC'15 ; Conference date: 29-10-2015 Through 01-11-2015",

}

Bacci, G , Bacci, G , Larsen, KG & Mardare, RI 2015, Converging from Branching to Linear Metrics on Markov Chains. in M Leucker, C Rueda & FD Valencia (eds), Theoretical Aspects of Computing - ICTAC 2015: 12th International Colloquium, Cali, Colombia, October 29-31, 2015, Proceedings. Springer, Lecture Notes in Computer Science, no. 9399, pp. 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 et al.
Theoretical Aspects of Computing - ICTAC 2015: 12th International Colloquium, Cali, Colombia, October 29-31, 2015, Proceedings. ed. / Martin Leucker; Camilo Rueda; Frank D. Valencia. Springer, 2015. p. 349-367 (Lecture Notes in Computer Science; No. 9399).

Research output: Contribution to book/anthology/report/conference proceeding › Book chapter › Research › peer-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

N1 - Conference code: 12

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

T2 - 12th International Colloquium on Theoretical Aspects of Computing

Y2 - 29 October 2015 through 1 November 2015

ER -

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

Converging from Branching to Linear Metrics on Markov Chains

Abstract

Conference

Access to Document

AUB Link

Fingerprint

Projects

CASSTING: Collective Adaptive System SynThesIs using Non-zero-sum Games

SENSATION: Self Energy-Supporting Autonomous Computation

IDEA4CPS: Foundations for Cyber-Physical Sytems

Cite this