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-Verlag 2004.
Cite
CITATION STYLE
Brim, L., Černá, I., Moravcc, P., & Šimša, J. (2004). Accepting predecessors are better than back edges in distributed LTL model-checking. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3312, 352–366. https://doi.org/10.1007/978-3-540-30494-4_25
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
