Relaxed Cycle Condition Improves Partial Order Reduction

Investor logo
Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

MORAVEC Pavel ŠIMŠA Jiří

Year of publication 2007
Type Article in Proceedings
Conference 3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2007)
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords model checking; partial order reduction; proviso checking
Description 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:

You are running an old browser version. We recommend updating your browser to its latest version.