. "3-540-23738-0" . . . "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."@en . "Moravec, Pavel" . "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." . "[4DF18BA696C8]" . "RIV/00216224:14330/04:00010529" . . "Brim, Lubo\u0161" . "Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking."@en . . . . "000226785300025" . "2004-01-01+01:00"^^ . "Austin, USA" . "4"^^ . . "14330" . "P(GA201/03/0509), Z(MSM 143300001)" . . . "Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking." . . . "4"^^ . "Akceptuj\u00EDc\u00ED p\u0159edch\u016Fdci v distrubuovan\u00E9m LTL ov\u011B\u0159ov\u00E1n\u00ED model\u016F"@cs . "Akceptuj\u00EDc\u00ED p\u0159edch\u016Fdci v distrubuovan\u00E9m LTL ov\u011B\u0159ov\u00E1n\u00ED model\u016F"@cs . "Neuveden" . . "RIV/00216224:14330/04:00010529!RIV09-GA0-14330___" . "Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking." . "Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking."@en . "24"^^ . . . "distributed - memory LTL model checking; graph predecessors"@en . "\u010Cern\u00E1, Ivana" . . . "\u010Cl\u00E1nek prezentuje nov\u00FD distribuovan\u00FD algoritmus pro ov\u011B\u0159ov\u00E1n\u00ED LTL vlastnost\u00ED zalo\u017Een\u00FD na akceptuj\u00EDc\u00EDch p\u0159edch\u016Fdc\u00EDch. Je prezentov\u00E1n\u00E9 n\u011Bkolik optimalizac\u00ED a experiment\u00E1ln\u00ED v\u00FDsledky"@cs . . "553348" . "Formal Methods in Computer-Aided Design (FMCAD)" . . "\u0160im\u0161a, Ji\u0159\u00ED" . . "Springer-Verlag. LNCS" .