This HTML5 document contains 48 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dctermshttp://purl.org/dc/terms/
n14http://localhost/temp/predkladatel/
n11http://linked.opendata.cz/resource/domain/vavai/projekt/
n5http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n18http://linked.opendata.cz/ontology/domain/vavai/
n13http://linked.opendata.cz/resource/domain/vavai/zamer/
shttp://schema.org/
skoshttp://www.w3.org/2004/02/skos/core#
n3http://linked.opendata.cz/ontology/domain/vavai/riv/
n2http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n15http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n7http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n10http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216224%3A14330%2F06%3A00015451%21RIV08-AV0-14330___/
n16http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n12http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n19http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n4http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n17http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F06%3A00015451%21RIV08-AV0-14330___
rdf:type
skos:Concept n18:Vysledek
dcterms:description
Přehledová práce shrnující výzkum v oblasti paralelního a distribuovaného ověřování modelu formulemi lineární temporální logiky. Jednotlivé algoritmy jsou teoreticky ale i experimentálně porovnány. 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. 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.
dcterms:title
Cluster-Based LTL Model Checking of Large Systems LTL ověřování modelu rozsáhlých systémů s využitím počítačových klastrů Cluster-Based LTL Model Checking of Large Systems
skos:prefLabel
Cluster-Based LTL Model Checking of Large Systems LTL ověřování modelu rozsáhlých systémů s využitím počítačových klastrů Cluster-Based LTL Model Checking of Large Systems
skos:notation
RIV/00216224:14330/06:00015451!RIV08-AV0-14330___
n3:strany
259-279
n3:aktivita
n12:Z n12:P
n3:aktivity
P(1ET408050503), P(1M0545), P(GA201/06/1338), P(GD102/05/H050), Z(MSM0021622419)
n3:cisloPeriodika
4111
n3:dodaniDat
n17:2008
n3:domaciTvurceVysledku
n5:6500773 n5:5692792 n5:2361132
n3:druhVysledku
n4:J
n3:duvernostUdaju
n7:S
n3:entitaPredkladatele
n10:predkladatel
n3:idSjednocenehoVysledku
468921
n3:idVysledku
RIV/00216224:14330/06:00015451
n3:jazykVysledku
n16:eng
n3:klicovaSlova
distributed LTL model checking
n3:klicoveSlovo
n15:distributed%20LTL%20model%20checking
n3:kodStatuVydavatele
NL - Nizozemsko
n3:kontrolniKodProRIV
[FB4DFC4A821C]
n3:nazevZdroje
Lecture Notes in Computer Science
n3:obor
n19:IN
n3:pocetDomacichTvurcuVysledku
3
n3:pocetTvurcuVysledku
3
n3:projekt
n11:GD102%2F05%2FH050 n11:GA201%2F06%2F1338 n11:1M0545 n11:1ET408050503
n3:rokUplatneniVysledku
n17:2006
n3:svazekPeriodika
2006
n3:tvurceVysledku
Černá, Ivana Barnat, Jiří Brim, Luboš
n3:zamer
n13:MSM0021622419
s:issn
0302-9743
s:numberOfPages
21
n14:organizacniJednotka
14330