author: Elwin Pater
title: Partial Order Reduction for PINS
keywords: model checking, state-space reduction, LTSmin
committee: Michael Weber ,
Jaco van de Pol ,
Dr. Dragan Bosnacki
started: July 2010
end: May 2011



There are a lot of different tools used for formal verification of hard- and software. Both for the scientific purpose of comparing methods and tools, as well as the industrial use cases which may require combining various methods, a uniform interface for state space generation would improve the applicability of model checkers. One such interface is the partitioned next state interface (PINS) which is an abstraction layer between the model and the algorithms used for state space generation. In this thesis we develop a partial order algorithm that works using a minimal extension of the PINS interface, and is developed in a modular fashion.

Summary of contributions

  1. A modular partial order reduction layer for an extension of PINS (i.e. language independent).
  2. Improvement on stubborn set algorithm.
  3. A modular LTL layer for PINS.
  4. Couvreur’s algorithm combined with General State Expanding Algorithms.
  5. A modular proviso implementation.


Additional Resources

  1. The paper