User:Aronisstav/sandbox/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 or automated planning and scheduling algorithm. It exploits the commutativity of transitions, which result in the same state when executed in different orders.

Formalization

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 (Peled 1993). There are various versions of selecting the subset, such as the ample set method (Peled 1993) (Clarke 1999), persistent set method (Godefroid 1994), source set method (Abdulla 2017), and stubborn set method (Valmari 1990).

Dependency relations

The formalization of partial order reduction techniques often relies on a notion of dependency between transitions of the state transition system. Two transitions are considered independent 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.

Dependency can be approximated by static analysis, or determined dynamic analysis, by 'executing' the transition system (e.g. running the program) and collecting data about the executed transitions.

Soundness

In order to be useful, a partial order reduction algorithm must ensure that it will inspect states that are partial-order-equivalent with all relevant reachable states in the given state-space. This is called a soundness or correctness argument. A method to prove soundness, is to show that the subset of transitions that the algorithm explores at every inspected state satisfies some particular property and also show that the property leads to soundness. The aforementioned ample, persistent, source, and stubborn properties describe subsets that lead to soundness. The algorithms for constructing such subsets out of all the enabled transitions at each state are also described in the referenced papers.

Effectiveness

The premise of partial order reduction techniques is that exploring the entire (i.e., not reduced) state-space is too costly. The effectiveness of a It is therefore important to determine how effective a particular partial order reduction technique is.

Subset selection

Sleep Sets

Optimality

Wakeup Trees

Tools

• CHESS
• Concuerror
• Nidhugg
• Java PathFinder
• SPIN
• VERISOFT

Other techniques

Abstract interpretation Bounded model checking Formal analysis

References

• Clarke, Edmund M.; Grumberg, Orna; Peled, Doron A. (1999). Model Checking. MIT Press.
• Flanagan, Cormac; Godefroid, Patrice (2005). "Dynamic partial-order reduction for model checking software". Proceedings of POPL ’05, 32th ACM Symp. on Principles of Programming Languages. pp. 110–121.
• Godefroid, Patrice (1994). Partial-Order Methods for the Verification of Concurrent Systems -- An Approach to the State-Explosion Problem (PostScript) (PhD). University of Liege, Computer Science Department.
• Holzmann, Gerard J (1993). The Spin Model Checker: Primer and Reference Manual. Addison-Wesley. ISBN 0-321-22862-6.
• Peled, Doron A. (1993). "All from One, One for All: Model Checking Using Representatives". Proceedings of CAV'93, LNCS 697, Springer 1993. pp. 409–423. doi:10.1007/3-540-56922-7_34.
• Valmari, Antti (1990). "Stubborn sets for reduced state space generation". Advances in Petri Nets 1990, LNCS 483, Springer 1991. pp. 491–515. doi:10.1007/3-540-53863-1_36.

External links

• www.example.com