Searchs in graphs for Verification and Partial Order Reductions

Blaise Genest
Friday, 14 March, 2008 (All day)

The problem of state space search is one of the most basic building blocks of various application, as verification. Often, the state space is huge, so optimizing the search is crucial. Some of the actions may commute, i.e., they result in the same state for every order in which they are taken. After recalling briefly the basic search methods and their advantages, we will review different techniques using the commutation (Partial Order Reductions) to reduce the state space. In particular, the state space can be reduced either by deleting states (e.g. using persistent or ample sets), or by deleting transitions (e.g. with the sleep set method). We will present a new partial order method reducing the number of transitions, shading a new light on sleep set method. In particular, it brings tangible benefits regarding the stack size.