Accepting predecessors are better than back edges in distributed LTL model-checking
Formal Methods in Computer-Aided Design: 5th International Conference, FMCAD …, 2004•Springer
We present a new distributed-memory algorithm for enumerative LTL model-checking that is
designed to be run on a cluster of workstations communicating via MPI. 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 ordering on the algorithm performance is discussed …
designed to be run on a cluster of workstations communicating via MPI. 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 ordering on the algorithm performance is discussed …
Abstract
We present a new distributed-memory algorithm for enumerative LTL model-checking that is designed to be run on a cluster of workstations communicating via MPI. 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 ordering on the algorithm performance is discussed. Experimental implementation of the algorithm shows promising results.
Springer
以上显示的是最相近的搜索结果。 查看全部搜索结果