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

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Bidrag til bog/antologi › Forskning › peer review

16 Citationer (Scopus)

Abstrakt

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.

Originalsprog	Engelsk
Titel	Theoretical Aspects of Computing - ICTAC 2015 : 12th International Colloquium, Cali, Colombia, October 29-31, 2015, Proceedings
Redaktører	Martin Leucker, Camilo Rueda, Frank D. Valencia
Antal sider	18
Forlag	Springer
Publikationsdato	2015
Sider	349-367
ISBN (Trykt)	978-3-319-25149-3
ISBN (Elektronisk)	978-3-319-25150-9
DOI	https://doi.org/10.1007/978-3-319-25150-9_21
Status	Udgivet - 2015
Begivenhed	12th International Colloquium on Theoretical Aspects of Computing - Cali, Colombia Varighed: 29 okt. 2015 → 1 nov. 2015 Konferencens nummer: 12

Konference

Konference	12th International Colloquium on Theoretical Aspects of Computing
Nummer	12
Land/Område	Colombia
By	Cali
Periode	29/10/2015 → 01/11/2015

Navn	Lecture Notes in Computer Science
Nummer	9399
ISSN	0302-9743

Adgang til dokumentet

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

3 Afsluttet

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
Projekter: Projekt › Forskning
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
Projekter: Projekt › Forskning
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
Projekter: Projekt › Forskning

Citationsformater

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 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. 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",

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. 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 et al.

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 proceeding › Bidrag til bog/antologi › Forskning › 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. 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). doi: 10.1007/978-3-319-25150-9_21

Converging from Branching to Linear Metrics on Markov Chains

Abstrakt

Konference

Adgang til dokumentet

Fingeraftryk

Projekter

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

SENSATION: Self Energy-Supporting Autonomous Computation

IDEA4CPS: Foundations for Cyber-Physical Sytems

Citationsformater