This HTML5 document contains 46 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/
n10http://purl.org/net/nknouf/ns/bibtex#
n12http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216224%3A14330%2F04%3A00010726%21RIV09-GA0-14330___/
n7http://localhost/temp/predkladatel/
n14http://linked.opendata.cz/resource/domain/vavai/projekt/
n8http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n9http://linked.opendata.cz/ontology/domain/vavai/
n15http://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#
n11http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n13http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n20http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n17http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n18http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n4http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n6http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F04%3A00010726%21RIV09-GA0-14330___
rdf:type
n9:Vysledek skos:Concept
dcterms:description
We propose a parallel distributed memory on-the-fly algorithm for enumerative LTL model checking. The algorithm is designed for network of workstations communicating via MPI. The detection of cycles (faulty runs) effectively employs the so called back-level edges. In particular, a parallel level synchronized breadth first search of the graph is performed to discover all back-level edges and for each level the back-level edges are checked in parallel by a nested search procedure to confirm or refute the presence of a cycle. Several optimizations of the basic algorithm are presented and advantages and drawbacks of their application to distributed LTL model checking are discussed. Experimental evaluation of the algorithm is presented. Je navržen distribuovaný algoritmus pro ověřování modelu pro logiku LTL. Tento algoritmus je založen na prohledávání stavového prostoru do šířky a k detekci cyklů využívá zpětných hran. We propose a parallel distributed memory on-the-fly algorithm for enumerative LTL model checking. The algorithm is designed for network of workstations communicating via MPI. The detection of cycles (faulty runs) effectively employs the so called back-level edges. In particular, a parallel level synchronized breadth first search of the graph is performed to discover all back-level edges and for each level the back-level edges are checked in parallel by a nested search procedure to confirm or refute the presence of a cycle. Several optimizations of the basic algorithm are presented and advantages and drawbacks of their application to distributed LTL model checking are discussed. Experimental evaluation of the algorithm is presented.
dcterms:title
Distributed Memory LTL Model Checking Based on Breadth First Search Distributed Memory LTL Model Checking Based on Breadth First Search Distrubuované ovřování modelu pro LTL založené na prohledávání do šířky
skos:prefLabel
Distributed Memory LTL Model Checking Based on Breadth First Search Distrubuované ovřování modelu pro LTL založené na prohledávání do šířky Distributed Memory LTL Model Checking Based on Breadth First Search
skos:notation
RIV/00216224:14330/04:00010726!RIV09-GA0-14330___
n3:aktivita
n17:Z n17:P
n3:aktivity
P(GA201/03/0509), Z(MSM 143300001)
n3:dodaniDat
n6:2009
n3:domaciTvurceVysledku
n8:5376327 n8:5692792 n8:6500773
n3:druhVysledku
n4:B
n3:duvernostUdaju
n13:S
n3:entitaPredkladatele
n12:predkladatel
n3:idSjednocenehoVysledku
560844
n3:idVysledku
RIV/00216224:14330/04:00010726
n3:jazykVysledku
n20:eng
n3:klicovaSlova
Distributed memory LTL model checking; breadth first search; cycle detection
n3:klicoveSlovo
n11:cycle%20detection n11:Distributed%20memory%20LTL%20model%20checking n11:breadth%20first%20search
n3:kontrolniKodProRIV
[5F826F08A71D]
n3:mistoVydani
Brno
n3:nazevEdiceCisloSvazku
FIMU-RS-2004-07
n3:nazevZdroje
Distributed Memory LTL Model Checking Based on Breadth First Search
n3:obor
n18:IN
n3:pocetDomacichTvurcuVysledku
3
n3:pocetStranKnihy
57
n3:pocetTvurcuVysledku
3
n3:projekt
n14:GA201%2F03%2F0509
n3:rokUplatneniVysledku
n6:2004
n3:tvurceVysledku
Chaloupka, Jakub Barnat, Jiří Brim, Luboš
n3:zamer
n15:MSM%20143300001
s:numberOfPages
57
n10:hasPublisher
Masarykova univerzita. Fakulta informatiky
n7:organizacniJednotka
14330