. "259-279" . "\u010Cern\u00E1, Ivana" . "4111" . . "P\u0159ehledov\u00E1 pr\u00E1ce shrnuj\u00EDc\u00ED v\u00FDzkum v oblasti paraleln\u00EDho a distribuovan\u00E9ho ov\u011B\u0159ov\u00E1n\u00ED modelu formulemi line\u00E1rn\u00ED tempor\u00E1ln\u00ED logiky. Jednotliv\u00E9 algoritmy jsou teoreticky ale i experiment\u00E1ln\u011B porovn\u00E1ny."@cs . . "0302-9743" . "NL - Nizozemsko" . "P(1ET408050503), P(1M0545), P(GA201/06/1338), P(GD102/05/H050), Z(MSM0021622419)" . . "Cluster-Based LTL Model Checking of Large Systems" . "Barnat, Ji\u0159\u00ED" . "Cluster-Based LTL Model Checking of Large Systems"@en . "RIV/00216224:14330/06:00015451!RIV08-AV0-14330___" . . "LTL ov\u011B\u0159ov\u00E1n\u00ED modelu rozs\u00E1hl\u00FDch syst\u00E9m\u016F s vyu\u017Eit\u00EDm po\u010D\u00EDta\u010Dov\u00FDch klastr\u016F"@cs . . "Lecture Notes in Computer Science" . "LTL ov\u011B\u0159ov\u00E1n\u00ED modelu rozs\u00E1hl\u00FDch syst\u00E9m\u016F s vyu\u017Eit\u00EDm po\u010D\u00EDta\u010Dov\u00FDch klastr\u016F"@cs . . . . . "Brim, Lubo\u0161" . "14330" . "468921" . . . "[FB4DFC4A821C]" . . "RIV/00216224:14330/06:00015451" . "Cluster-Based LTL Model Checking of Large Systems"@en . . "distributed LTL model checking"@en . "2006" . . "21"^^ . . "In recent years a bundle of parallel and distributed algorithms for verification of finite state systems has appeared. We survey distributed memory enumerative LTL model checking algorithms designed for networks of workstations communicating via MPI. The automata-based approach to LTL model checking reduces the model checking problem to the accepting cycle detection problem. Contrary to sequential algorithms, distributed algorithms cannot rely on depth-first search postorder which is essential for efficient cycle detection. Therefore, they have to employ diverse conditions that characterize the existence of cycles in a graph in order to come up with an efficient and practical solution. We compare these algorithms both theoretically and experimentally and determine cases where particular algorithms can be useful."@en . . "In recent years a bundle of parallel and distributed algorithms for verification of finite state systems has appeared. We survey distributed memory enumerative LTL model checking algorithms designed for networks of workstations communicating via MPI. The automata-based approach to LTL model checking reduces the model checking problem to the accepting cycle detection problem. Contrary to sequential algorithms, distributed algorithms cannot rely on depth-first search postorder which is essential for efficient cycle detection. Therefore, they have to employ diverse conditions that characterize the existence of cycles in a graph in order to come up with an efficient and practical solution. We compare these algorithms both theoretically and experimentally and determine cases where particular algorithms can be useful." . . "3"^^ . "Cluster-Based LTL Model Checking of Large Systems" . "3"^^ . . .