Time: Wednesday 12.10.2005, 14:30
Place: Room A4-108, Fr. Bajersvej 7
We present a distributed-memory algorithm for enumerative LTL model-checking that is designed to be run on a cluster of workstations. The detection of accepting cycles is based on computing maximal accepting predecessors and the subsequent decomposition of the graph into independent predecessor subgraphs induced by maximal accepting predecessors. Several optimizations of the basic algorithm are presented and the influence of the vertex ordering on the algorithm performance is discussed.