Partial 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) eq 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 ref_harvard|ClarkeEtAl1999|Clarke "et al." 1999|_. 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 ref_harvard|Godefroid1994|Godefroid 1994|_.

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).

References

* Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, "Model Checking", MIT Press, 1999.
* Patrice Godefroid, "Partial-Order Methods for the Verification of Concurrent Systems -- An Approach to the State-Explosion Problem", PhD. thesis, University of Liege, Computer Science Department, 1994, [http://cm.bell-labs.com/who/god/public_psfiles/thesis.ps download thesis as PostScript] .
* [http://spinroot.com/spin/Doc/Book_extras/ "The Spin Model Checker: Primer and Reference Manual"] , Gerard J. Holzmann, Addison-Wesley, ISBN 0-321-22862-6.


Wikimedia Foundation. 2010.

Игры ⚽ Поможем написать курсовую

Look at other dictionaries:

  • Reduction — Reduction, reduced, or reduce may refer to:cienceChemistry*Reduction – chemical reaction in which atoms have their oxidation number (oxidation state) changed. **Reduced gas – a gas with a low oxidation number **Ore reduction: see… …   Wikipedia

  • Order of Saint Augustine — Abbreviation OSA Formation March, 1256 Type Catholic religious ord …   Wikipedia

  • Partial fraction — In algebra, the partial fraction decomposition or partial fraction expansion is a procedure used to reduce the degree of either the numerator or the denominator of a rational function (also known as a rational algebraic fraction). In symbols, one …   Wikipedia

  • Order of integration (calculus) — For the summary statistic in time series, see Order of integration. Topics in Calculus Fundamental theorem Limits of functions Continuity Mean value theorem Differential calculus  Derivative Change of variables Implicit differentiati …   Wikipedia

  • Reduction criterion — In quantum information theory, the reduction criterion is a necessary condition a mixed state must satisfy in order for it to be separable. In other words, the reduction criterion is a separability criterion . Details Let H 1 and H 2 be Hilbert… …   Wikipedia

  • Glossary of order theory — This is a glossary of some terms used in various branches of mathematics that are related to the fields of order, lattice, and domain theory. Note that there is a structured list of order topics available as well. Other helpful resources might be …   Wikipedia

  • Turing reduction — In computability theory, a Turing reduction from a problem A to a problem B, named after Alan Turing, is a reduction which solves A, assuming B is already known (Rogers 1967, Soare 1987). It can be understood as an algorithm that could be used to …   Wikipedia

  • Noise reduction — For sound proofing, see soundproofing. For scientific aspects of noise reduction of machinery and products, see noise control. Noise reduction is the process of removing noise from a signal. All recording devices, both analogue or digital, have… …   Wikipedia

  • United States Congress Joint Select Committee on Deficit Reduction — The Joint Select Committee on Deficit Reduction,[1] colloquially referred to as the Supercommittee, is a joint select committee of the United States Congress, created by the Budget Control Act of 2011 on August 2, 2011. The act was intended to… …   Wikipedia

  • Lithic reduction — The Levallois technique of flint knapping Lithic reduction involves the use of a hard hammer precursor, such as a hammerstone, a soft hammer fabricator (made of wood, bone or antler), or a wood or antler punch to detach lithic flakes from a lump… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”