Oct 25, 2011: Tien-Loong Siaw: Saturation for state space generation in LTSmin

October 25, 2011Saturation for state space generation in LTSmin
Room: Zi 5126Tien-Loong Siaw

State space generation or reachability analysis plays an important role in model checking, but a disadvantage of current techniques lies in the fact that they require quite a lot of time and memory to come up with a result when using real-life system models. Symbolic state space generation using known traversal techniques as breadth-first search and search using chaining are quite common practice, but their performance on large real-life system models remains an issue to be tackled.
In the past decade a relatively new traversal technique has emerged, named Saturation. This traversal technique has proven itself to be a good competitor to traditional symbolic state space generation techniques for handling models with extremely large state spaces. It originates from the research group of professor Gianfranco Ciardo (University of California at Riverside, USA).
The main goal of this Master project is to design and assess the Saturation approach within the LTSmin toolset. This toolset has as main feature the clean interface for representing states in a model in a uniform way using PINS, allowing it to separate language-specific details from model checking algorithms.
In this presentation an introduction to the Saturation approach as state space generation technique is given, together with a short overview of the different variants of Saturation approaches. Furthermore aspects from the LTSmin toolset and the current status of the implementation of the Saturation approach into the toolset is highlighted.