Converging from Branching to Linear Metrics on Markov Chains

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

16 Citationer (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.
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
Land/OmrådeColombia
ByCali
Periode29/10/201501/11/2015
NavnLecture Notes in Computer Science
Nummer9399
ISSN0302-9743

Fingeraftryk

Dyk ned i forskningsemnerne om 'Converging from Branching to Linear Metrics on Markov Chains'. Sammen danner de et unikt fingeraftryk.

Citationsformater