scholarly journals Supporting domain-specific state space reductions through local partial-order reduction

2011 ◽  
Author(s):  
Peter Bokor ◽  
Johannes Kinder ◽  
Marco Serafini ◽  
Neeraj Suri
Keyword(s):  
State Space ◽  
Partial Order ◽  
Order Reduction ◽  
Partial Order Reduction ◽  
Domain Specific

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.

scholarly journals Model Checking $$\omega $$-Regular Properties with Decoupled Search

2021 ◽  
pp. 411-434
Author(s):  
Daniel Gnad ◽  
Jan Eisenhut ◽  
Alberto Lluch Lafuente ◽  
Jörg Hoffmann
Keyword(s):  
Model Checking ◽  
State Space ◽  
Partial Order ◽  
Order Reduction ◽  
Partial Order Reduction ◽  
Ai Planning ◽  
Symbolic Representations ◽  
State Space Search ◽  
Liveness Properties ◽  
Reduction Methods

AbstractDecoupled search is a state space search method originally introduced in AI Planning. Similar to partial-order reduction methods, decoupled search exploits the independence of components to tackle the state explosion problem. Similar to symbolic representations, it does not construct the explicit state space, but sets of states are represented in a compact manner, exploiting component independence. Given the success of both partial-order reduction and symbolic representations when model checking liveness properties, our goal is to add decoupled search to the toolset of liveness checking methods. Specifically, we show how decoupled search can be applied to liveness verification for composed Büchi automata by adapting, and showing correct, a standard algorithm for detecting lassos (i.e., infinite accepting runs), namely nested depth-first search. We evaluate our approach using a prototype implementation.

Dynamic partial order reduction for relaxed memory models

2015 ◽  
Vol 50 (6) ◽  
pp. 250-259 ◽  
Author(s):  
Naling Zhang ◽  
Markus Kusano ◽  
Chao Wang
Keyword(s):  
Partial Order ◽  
Order Reduction ◽  
Memory Models ◽  
Partial Order Reduction ◽  
Relaxed Memory
Sign in / Sign up

Export Citation Format

Share Document