applicative order reduction

Partial order reduction

In computer science, partial order reduction is a technique for reducing the size of the state-space to be searched by a model checking algorithm. It exploits the commutativity of concurrently executed transitions, which result in the same state when executed in different orders. Thus, this reduction technique is best suited for asynchronous systems.

C0 {ample(s)=empty} iff {enabled(s)=empty}

C1 If a transition alpha depends on some transition relation in ample(s), this transition cannot be invoked until some transition in the ample set executed.

C2 If enabled(s) neq ample(s) , each transition in the ample set is invisible

C3 A cycle is not allowed if it contains a state in which some transition alpha is enabled, but is never included in ample(s) for any states s on the cycle.

These conditions are sufficient for an ample set, but not necessary conditions . The premises of cutting a state out is that the state will not lead to some property-violate-states that cannot be uncovered by other states in the ample set. As those erroneous states cannot be known in advance, while exploring the state space, we use those conditions.

There are also other notations for partial order reduction. One of the commonly used is the persistent set/sleep set algorithm. Detailed information can be found in Patrice Godefroid's thesis .

In explicit model checking, partial order reduction can be achieved by discovering the independent transitions. In symbolic model checking, partial order reduction can be achieved by adding more constraints (guard strengthening).


Search another word or see applicative order reductionon Dictionary | Thesaurus |Spanish
Copyright © 2014, LLC. All rights reserved.
  • Please Login or Sign Up to use the Recent Searches feature