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

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

Namespace Prefixes

PrefixIRI
n19http://linked.opendata.cz/ontology/domain/vavai/riv/typAkce/
dctermshttp://purl.org/dc/terms/
n22http://purl.org/net/nknouf/ns/bibtex#
n18http://localhost/temp/predkladatel/
n13http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n6http://linked.opendata.cz/resource/domain/vavai/projekt/
n14http://linked.opendata.cz/ontology/domain/vavai/
n20https://schema.org/
n4http://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/
n7http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216224%3A14330%2F06%3A00015451%21RIV10-GA0-14330___/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n16http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n21http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n9http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n5http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n17http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n10http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n8http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F06%3A00015451%21RIV10-GA0-14330___
rdf:type
n14:Vysledek skos:Concept
dcterms:description
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 Cluster-Based LTL Model Checking of Large Systems
skos:prefLabel
Cluster-Based LTL Model Checking of Large Systems Cluster-Based LTL Model Checking of Large Systems
skos:notation
RIV/00216224:14330/06:00015451!RIV10-GA0-14330___
n3:aktivita
n5:Z n5:P
n3:aktivity
P(1ET408050503), P(1M0545), P(GA201/06/1338), P(GD102/05/H050), Z(MSM0021622419)
n3:dodaniDat
n8:2010
n3:domaciTvurceVysledku
n13:6500773 n13:2361132 n13:5692792
n3:druhVysledku
n10:D
n3:duvernostUdaju
n21:S
n3:entitaPredkladatele
n7:predkladatel
n3:idSjednocenehoVysledku
468920
n3:idVysledku
RIV/00216224:14330/06:00015451
n3:jazykVysledku
n9:eng
n3:klicovaSlova
distributed LTL model checking
n3:klicoveSlovo
n16:distributed%20LTL%20model%20checking
n3:kontrolniKodProRIV
[AD6952B3136B]
n3:mistoKonaniAkce
Amsterdam
n3:mistoVydani
Berlin
n3:nazevZdroje
Formal Methods for Components and Objects
n3:obor
n17:IN
n3:pocetDomacichTvurcuVysledku
3
n3:pocetTvurcuVysledku
3
n3:projekt
n6:GD102%2F05%2FH050 n6:1M0545 n6:1ET408050503 n6:GA201%2F06%2F1338
n3:rokUplatneniVysledku
n8:2006
n3:tvurceVysledku
Brim, Luboš Černá, Ivana Barnat, Jiří
n3:typAkce
n19:WRD
n3:wos
00240360000013
n3:zahajeniAkce
2006-01-01+01:00
n3:zamer
n4:MSM0021622419
s:numberOfPages
21
n22:hasPublisher
Springer-Verlag
n20:isbn
978-3-540-36749-9
n18:organizacniJednotka
14330