Back to University of Twente portal
| 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) |
Abstract
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.
References
- Kenneth McMillan, Symoblic Model Checking (Digital version available here)
- Elwin Pater, Partial Order Reduction for PINS (Digital version available here)
- Gianfranco Ciardo and Andy Jinqing Yu, Conjunctive and Disjunctive Partitioning (Digital version available here)