scholarly journals Distributed disk-based algorithms for model checking very large Markov chains

2006 ◽  
Vol 29 (2) ◽  
pp. 177-196 ◽  
Author(s):  
Alexander Bell ◽  
Boudewijn R. Haverkort
Keyword(s):  
Model Checking ◽  
Markov Chains

Model Checking Markov Chains with Actions and State Labels

2007 ◽  
Vol 33 (4) ◽  
pp. 209-224 ◽  
Author(s):  
Christel Baier ◽  
Lucia Cloth ◽  
Boudewijn R. Haverkort ◽  
Matthias Kuntz ◽  
Markus Siegle
Keyword(s):  
Model Checking ◽  
Markov Chains

Counterexample Generation for Markov Chains Using SMT-Based Bounded Model Checking

2011 ◽  
pp. 75-89 ◽  
Author(s):  
Bettina Braitling ◽  
Ralf Wimmer ◽  
Bernd Becker ◽  
Nils Jansen ◽  
Erika Ábrahám
Keyword(s):  
Model Checking ◽  
Markov Chains ◽  
Bounded Model Checking

scholarly journals Converging from branching to linear metrics on Markov chains

2017 ◽  
Vol 29 (1) ◽  
pp. 3-37 ◽  
Author(s):  
GIORGIO BACCI ◽  
GIOVANNI BACCI ◽  
KIM G. LARSEN ◽  
RADU MARDARE
Keyword(s):  
Model Checking ◽  
Markov Chains ◽  
Temporal Logic ◽  
Polynomial Time ◽  
Linear Time ◽  
Linear Temporal Logic ◽  
Np Hard ◽  
Branching Time ◽  
Threshold Problem ◽  
Ltl Model Checking

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 linear temporal logic (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 non-trivial relation between branching and linear-time metric-based semantics that does not hold in equivalence-based semantics.

Sign in / Sign up

Export Citation Format

Share Document