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

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

Namespace Prefixes

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

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F04%3A00010725%21RIV08-MSM-14330___
rdf:type
skos:Concept n20:Vysledek
dcterms:description
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. 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. V článku je popsán paralelní a distribuovaný algoritmus pro detekci cyklu v rozsáhlých distribuovaných grafech. Algoritmus využívá tzv. back-level hrany, jež lze spočítat s využitím distribuovaného prohledávání grafu do šířky. Dále článek popisuje jak lze tento algoritmus upravit za účelem použití pro ověřování modelu LTL. Konkrétně je navrženo rozšíření algoritmu o detekci akceptujících cyklů, generování protipříkladů a redukci stavového prostoru s využitím redukce částečným uspořádáním. Článek také podává nezbytné experimentální vyhodnocení algoritmu.
dcterms:title
Od distribuovane detekce cyklu k paralelnimu LTL overovani modelu From Distributed Memory Cycle Detection to Parallel LTL Model Checking From Distributed Memory Cycle Detection to Parallel LTL Model Checking
skos:prefLabel
From Distributed Memory Cycle Detection to Parallel LTL Model Checking Od distribuovane detekce cyklu k paralelnimu LTL overovani modelu From Distributed Memory Cycle Detection to Parallel LTL Model Checking
skos:notation
RIV/00216224:14330/04:00010725!RIV08-MSM-14330___
n5:strany
17-34
n5:aktivita
n14:P n14:Z
n5:aktivity
P(GA201/03/0509), Z(MSM 143300001)
n5:dodaniDat
n10:2008
n5:domaciTvurceVysledku
n12:5376327 n12:5692792 n12:6500773
n5:druhVysledku
n8:D
n5:duvernostUdaju
n18:S
n5:entitaPredkladatele
n19:predkladatel
n5:idSjednocenehoVysledku
564936
n5:idVysledku
RIV/00216224:14330/04:00010725
n5:jazykVysledku
n11:eng
n5:klicovaSlova
LTL model checking; breadth first search; distributed memory
n5:klicoveSlovo
n7:breadth%20first%20search n7:LTL%20model%20checking n7:distributed%20memory
n5:kontrolniKodProRIV
[A7CCC139A24C]
n5:mistoKonaniAkce
Linz, Austria
n5:mistoVydani
Linz, Austria
n5:nazevZdroje
Proceedings of the Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2004)
n5:obor
n16:IN
n5:pocetDomacichTvurcuVysledku
3
n5:pocetTvurcuVysledku
3
n5:projekt
n6:GA201%2F03%2F0509
n5:rokUplatneniVysledku
n10:2004
n5:tvurceVysledku
Brim, Luboš Chaloupka, Jakub Barnat, Jiří
n5:typAkce
n13:WRD
n5:zahajeniAkce
2004-01-01+01:00
n5:zamer
n15:MSM%20143300001
s:numberOfPages
18
n17:hasPublisher
Institute for Systems Engineering & Automation, Kepler university Linz
n22:isbn
3-902457-03-1
n9:organizacniJednotka
14330