"Od distribuovane detekce cyklu k paralelnimu LTL overovani modelu"@cs . "From Distributed Memory Cycle Detection to Parallel LTL Model Checking"@en . . . "LTL model checking; breadth first search; distributed memory"@en . . "14330" . "Proceedings of the Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2004)" . . . . "RIV/00216224:14330/04:00010725!RIV08-MSM-14330___" . "We propose a parallel graph algorithm for detecting cycles in very large directed graphs distributed over a network of workstations. The algorithm employs back-level edges as computed by the breadth first search. In this paper we describe how to turn the algorithm into an explicit state distributed memory LTL model checker by extending it with detection of accepting cycles, counterexample generation and partial order reduction. We discuss these extensions and show experimental results."@en . . . "From Distributed Memory Cycle Detection to Parallel LTL Model Checking" . "From Distributed Memory Cycle Detection to Parallel LTL Model Checking"@en . "P(GA201/03/0509), Z(MSM 143300001)" . "Brim, Lubo\u0161" . "3"^^ . . . "3"^^ . . . . . . "17-34" . "564936" . "Chaloupka, Jakub" . "2004-01-01+01:00"^^ . "Linz, Austria" . "Institute for Systems Engineering & Automation, Kepler university Linz" . "Linz, Austria" . . "We propose a parallel graph algorithm for detecting cycles in very large directed graphs distributed over a network of workstations. The algorithm employs back-level edges as computed by the breadth first search. In this paper we describe how to turn the algorithm into an explicit state distributed memory LTL model checker by extending it with detection of accepting cycles, counterexample generation and partial order reduction. We discuss these extensions and show experimental results." . . "[A7CCC139A24C]" . . "RIV/00216224:14330/04:00010725" . "Barnat, Ji\u0159\u00ED" . . . "Od distribuovane detekce cyklu k paralelnimu LTL overovani modelu"@cs . "18"^^ . "From Distributed Memory Cycle Detection to Parallel LTL Model Checking" . "3-902457-03-1" . "V \u010Dl\u00E1nku je pops\u00E1n paraleln\u00ED a distribuovan\u00FD algoritmus pro detekci cyklu v rozs\u00E1hl\u00FDch distribuovan\u00FDch grafech. Algoritmus vyu\u017E\u00EDv\u00E1 tzv. back-level hrany, je\u017E lze spo\u010D\u00EDtat s vyu\u017Eit\u00EDm distribuovan\u00E9ho prohled\u00E1v\u00E1n\u00ED grafu do \u0161\u00ED\u0159ky. D\u00E1le \u010Dl\u00E1nek popisuje jak lze tento algoritmus upravit za \u00FA\u010Delem pou\u017Eit\u00ED pro ov\u011B\u0159ov\u00E1n\u00ED modelu LTL. Konkr\u00E9tn\u011B je navr\u017Eeno roz\u0161\u00ED\u0159en\u00ED algoritmu o detekci akceptuj\u00EDc\u00EDch cykl\u016F, generov\u00E1n\u00ED protip\u0159\u00EDklad\u016F a redukci stavov\u00E9ho prostoru s vyu\u017Eit\u00EDm redukce \u010D\u00E1ste\u010Dn\u00FDm uspo\u0159\u00E1d\u00E1n\u00EDm. \u010Cl\u00E1nek tak\u00E9 pod\u00E1v\u00E1 nezbytn\u00E9 experiment\u00E1ln\u00ED vyhodnocen\u00ED algoritmu."@cs .