Publication details

<< back
 

Relaxed Cycle Condition Improves Partial Order Reduction

Basic information
Original title:Relaxed Cycle Condition Improves Partial Order Reduction
Authors:Pavel Moravec, Jiří Šimša
Further information
Citation:MORAVEC, Pavel - ŠIMŠA, Jiří. Relaxed Cycle Condition Improves Partial Order Reduction. In 3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2007). Znojmo, Czech Republic : FI MU, FIT VUT, 2007. ISBN 978-80-7355-077-6, pp. 140-147. 2007, Znojmo, Czech Republic.
Original language:English
Field:Informatika
Type:Article in Proceedings
Keywords:model checking; partial order reduction; proviso checking

Partial order reduction is a method widely used for tackling the state space explosion problem. In this paper we focus on a theoretical refinement of a particular instance of the partial order reduction which is nowadays an inherent part of most tools for explicit state model checking of Linear Temporal Logic. This particular instance is represented as a set of conditions C0 through C3 which describe valid reductions of a state space. We propose a hierarchy of alternatives to the cycle condition C3. In this hierarchy we point out which alternatives guarantee a valid reduction with respect to LTL_X properties.

Related projects:

 
 
top