author: Jeroen Meijer
title: Improving Reachability Analysis in LTSmin
keywords: puzzles, games, hardware circuits, BDDs, symbolic model checking
topics: Algorithms and Data Structures
committee: Jaco van de Pol ,
Stefan Blom ,
Gijs Kant
started: September 2013
end: March 2014
type: Master in Computer Science (MTV or SE)


Boost symbolic model checking in LTSmin by revisiting the notion

of guards, exploit it in symbolic reachability strategies, and

apply it to mCRL2 models.


This research will boost our symbolic model checking capabilities,

and should allow us to solve interesting puzzles (Sokoban, Othello)

and games (Connect Four, Checkers) and verify synchronous hardware models.



  1. Kenneth McMillan, Symoblic Model Checking (Digital version available here)
  2. Elwin Pater, Partial Order Reduction for PINS (Digital version available here)
  3. Gianfranco Ciardo and Andy Jinqing Yu, Conjunctive and Disjunctive Partitioning (Digital version available here)

Additional Resources

  1. The paper