Jiri Barnat

Faculty of Informatics, Masaryk University in Brno, Czech Republic.

Time: Wednesday 2.3.2005, 14:30
Place: Room NJ 14 4-117, Niels Jernes Vej 14

Distributed Memory LTL Model Checking

The talk will give a survey on cycle detection algorithms designed to be used on clusters and NOWs. Need for distributed memory cycle detection algorithms come from LTL model checking, where cycle detection is used to check validity of an LTL formula. However, as soon as the graph to be checked cannot be completely kept in memory of a single computer, the algorithm is practically useless. Therefore, specialized algorithms were developed to perform cycle detection on distributed graphs. These will be presented in the talk.