Mar 01, 2011: Elwin Pater: Partial Order Reduction for LTSmin

March 01, 2011Partial Order Reduction for LTSmin
Room: Zi 5126Elwin Pater

Partial Order Reduction is a well known technique to handle the state space explosion, caused by the (asynchronous) composition of multiple sub-components into one global system. It reduces that state space to a smaller state space in which properties of interest are preserved. For partial order reduction,  various algorithms are available in literature, but all of them rely on the notion of processes. This notion is not available in PINS, an Interface for a Partitioned Next State, used by the LTSmin model checking toolset ( In this talk i will show an adaptation of the 'stubborn set' algorithm (Valmari, Godefroid) that can be used in combination with an extended version of the PINS interface, without the notion of processes.