Jeroen Meijer - Improving Reachability Analysis in LTSmin

author:Jeroen Meijer
title:Improving Reachability Analysis in LTSmin
keywords:puzzles, games, hardware circuits, BDDs, symbolic model checking
topics:Algorithms and Data Structures
committee:prof.dr. J.C. van de Pol (1st supervisor)
dr. S.C.C. Blom
G. Kant MSc
graduation date:27 March 2014 (mark: 9)

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)