Janina Torbecke - Symbolic Model Checking on Supercomputers

author:Janina Torbecke
title:Symbolic Model Checking on Supercomputers
keywords:large search spaces, distributed model checking, binary decision diagrams, supercomputers
topics:Algorithms and Data Structures
committee:prof.dr. J.C. van de Pol
W.H.M. Oortwijn MSc
started:1 December 2015

Research topics

Description

In practice, model checking frequently fails due to state space explosions, since state spaces tend to grow exponentially with the size of the input model. Several strategies exist to fight state space explosions. An example is symbolic model checking, in which the state space is represented symbolically to reduce space requirements. Another example is employing additional hardware resources, in combination with parallel and/or distributed algorithms for model checking. By employing more memory, larger state spaces can be stored, and by increasing the number of CPUs, state spaces can be processed faster.


This research project attempts to combine both strategies by implementing symbolic model checking algorithms targeting high-performance networks of many-core machines. Earlier work on distributed verification show that very large state spaces can be handled, but maintaining time-efficiency is still an active challenge. Recently, we implemented BDD-based distributed reachability analysis on many-core clusters, and thereby improve on time-efficiency compared to earlier work. 


The research project has two main goals: (1) providing support for distributed cluster-based verification techniques into LTSmin, and (2) using the implementation to solve some very challenging problems that require a supercomputer, like solving Chess. To achieve (2), techniques have to be developed to improve load-balancing and to better exploit data-locality. Furthermore, alternative decision diagrams can be tried to store states more efficiently.


TASKS:

  • Developing techniques for improved load-balancing and better exploitation of data-locality, compared to [1,2].
  • Experimenting with alternative decision diagrams, e.g. MDDs, LDDs, and ZDDs.
  • Implementing support for CTL model checking.
  • Integrating the distributed algorithms into LTSmin.- Evaluating the performance by performing model checking on challenging examples, for example solving Chess.

 

References

  1. Wytse Oortwijn, Distributed Symbolic Reachability Analysis (Master's Thesis).
  2. Gijs Kant, LTSmin: High-Performance Language-Independent Model Checking. (Digital version available here)
  3. Gianfranco Ciardo, Parallel symbolic state-space exploration is difficult, but what is the alternative?