Partial-order methods for model checking: from linear time to branching time

2002 ◽  
Author(s):  
B. Willems ◽  
P. Wolper
Keyword(s):  
Model Checking ◽  
Partial Order ◽  
Linear Time ◽  
Branching Time

scholarly journals A Partial Order Approach to Branching Time Logic Model Checking

1999 ◽  
Vol 150 (2) ◽  
pp. 132-152 ◽  
Author(s):  
Rob Gerth ◽  
Ruurd Kuiper ◽  
Doron Peled ◽  
Wojciech Penczek
Keyword(s):  
Model Checking ◽  
Partial Order ◽  
Logic Model ◽  
Branching Time ◽  
Time Logic ◽  
Logic 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.

scholarly journals A Detailed Account of The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction

2021 ◽  
Vol Volume 17, Issue 3 ◽  
Author(s):  
Thomas Neele ◽  
Antti Valmari ◽  
Tim A. C. Willemse
Keyword(s):  
Model Checking ◽  
Partial Order ◽  
Linear Time ◽  
Order Reduction ◽  
Partial Order Reduction ◽  
Space Reduction ◽  
Reduction Techniques ◽  
Counter Example ◽  
The Impact ◽  
Trace Equivalence

One of the most popular state-space reduction techniques for model checking is partial-order reduction (POR). Of the many different POR implementations, stubborn sets are a very versatile variant and have thus seen many different applications over the past 32 years. One of the early stubborn sets works shows how the basic conditions for reduction can be augmented to preserve stutter-trace equivalence, making stubborn sets suitable for model checking of linear-time properties. In this paper, we identify a flaw in the reasoning and show with a counter-example that stutter-trace equivalence is not necessarily preserved. We propose a stronger reduction condition and provide extensive new correctness proofs to ensure the issue is resolved. Furthermore, we analyse in which formalisms the problem may occur. The impact on practical implementations is limited, since they all compute a correct approximation of the theory. Comment: arXiv admin note: substantial text overlap with arXiv:1910.09829

scholarly journals The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction

2020 ◽  
pp. 482-501 ◽  
Author(s):  
Thomas Neele ◽  
Antti Valmari ◽  
Tim A. C. Willemse
Keyword(s):  
Model Checking ◽  
State Space ◽  
Partial Order ◽  
Linear Time ◽  
Order Reduction ◽  
Partial Order Reduction ◽  
Correctness Proof ◽  
Counter Example ◽  
The Impact ◽  
Trace Equivalence

AbstractIn model checking, partial-order reduction (POR) is an effective technique to reduce the size of the state space. Stubborn sets are an established variant of POR and have seen many applications over the past 31 years. One of the early works on stubborn sets shows that a combination of several conditions on the reduction is sufficient to preserve stutter-trace equivalence, making stubborn sets suitable for model checking of linear-time properties. In this paper, we identify a flaw in the reasoning and show with a counter-example that stutter-trace equivalence is not necessarily preserved. We propose a solution together with an updated correctness proof. Furthermore, we analyse in which formalisms this problem may occur. The impact on practical implementations is limited, since they all compute a correct approximation of the theory.

Sign in / Sign up

Export Citation Format

Share Document