Relaxed Cycle Condition Improves Partial Order Reduction
| Authors | |
|---|---|
| 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 | |
| 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: |
|