In
computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to Applied science, practical discipli ...
, partial order reduction is a technique for reducing the size of the
state-space
A state space is the set of all possible configurations of a system. It is a useful abstraction for reasoning about the behavior of a given system and is widely used in the fields of artificial intelligence and game theory.
For instance, the toy ...
to be searched by a
model checking
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems ...
or
automated planning and scheduling
Automation describes a wide range of technologies that reduce human intervention in processes, namely by predetermining decision criteria, subprocess relationships, and related actions, as well as embodying those predeterminations in machines ...
algorithm
In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algorithms are used as specificat ...
. It exploits the commutativity of concurrently executed
transitions that result in the same state when executed in different orders.
In explicit state space exploration, partial order reduction usually refers to the specific technique of expanding a representative subset of all enabled transitions. This technique has also been described as model checking with representatives.
There are various versions of the method, the so-called stubborn set method, ample set method,
and persistent set method.
Ample sets
Ample sets are an example of model checking with representatives. Their formulation relies on a separate notion of ''dependency''. Two transitions are considered independent only if whenever they are mutually enabled, they cannot disable another and the execution of both results in a unique state regardless of the order in which they are executed. Transitions that are not independent, are dependent. In practice dependency is approximated using
static analysis
Static analysis, static projection, or static scoring is a simplified analysis wherein the effect of an immediate change to a system is calculated without regard to the longer-term response of the system to that change. If the short-term effect i ...
.
Ample sets for different purposes can be defined by giving conditions as to when a set of transitions is "ample" in a given state.
C0
C1 If a transition
depends on some transition relation in
, this transition cannot be invoked until some transition in the ample set is executed.
Conditions C0 and C1 are sufficient for preserving all the deadlocks in the state space. Further restrictions are needed in order to preserve more nuanced properties. For instance, in order to preserve properties of
linear temporal logic In logic, linear temporal logic or linear-time temporal logic (LTL) is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths, e.g., a condition will eventually be true, a condition will ...
, the following two conditions are needed:
C2 If
, each transition in the ample set is invisible.
C3 A
cycle is not allowed if it contains a state in which some transition
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.
Stubborn sets
Stubborn sets make no use of an explicit independence relation. Instead they are defined solely through commutativity over sequences of actions. A set
is (weakly) stubborn at s, if the following hold.
D0
, if execution of the sequence
is possible and leads to the state
, then execution of the sequence
is possible and will lead to state
.
D1 Either
is a deadlock, or
such that
, the execution of
is possible.
These conditions are sufficient for preserving all
deadlocks
In concurrent computing, deadlock is any situation in which no member of some group of entities can proceed because each waits for another member, including itself, to take action, such as sending a message or, more commonly, releasing a lo ...
, just like C0 and C1 are in the ample set method. They are, however, somewhat weaker, and as such may lead to smaller sets. The conditions C2 and C3 can also be further weakened from what they are in the ample set method, but the stubborn set method is compatible with C2 and C3.
Others
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 symbolic model checking, partial order reduction can be achieved by adding more constraints (guard strengthening). Further applications of partial order reduction involve automated planning.
Citations
References
*
*
*
*
*
* {{Cite conference , first=Antti , last=Valmari , title=Stubborn sets for reduced state space generation , book-title=Advances in Petri Nets 1990, LNCS 483, Springer 1991 , year=1990, pages=491–515, doi=10.1007/3-540-53863-1_36
Model checking