Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking.

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BRIM Luboš ČERNÁ Ivana MORAVEC Pavel ŠIMŠA Jiří

Year of publication 2004
Type Article in Proceedings
Conference Formal Methods in Computer-Aided Design (FMCAD)
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords distributed - memory LTL model checking; graph predecessors
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.