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

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

Namespace Prefixes

PrefixIRI
n10http://linked.opendata.cz/ontology/domain/vavai/riv/typAkce/
dctermshttp://purl.org/dc/terms/
n22http://purl.org/net/nknouf/ns/bibtex#
n14http://localhost/temp/predkladatel/
n12http://linked.opendata.cz/resource/domain/vavai/projekt/
n6http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n17http://linked.opendata.cz/ontology/domain/vavai/
n21http://linked.opendata.cz/resource/domain/vavai/zamer/
n5https://schema.org/
shttp://schema.org/
skoshttp://www.w3.org/2004/02/skos/core#
n3http://linked.opendata.cz/ontology/domain/vavai/riv/
n20http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216224%3A14330%2F04%3A00010529%21RIV09-GA0-14330___/
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/
n18http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n15http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n4http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n13http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n7http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n16http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F04%3A00010529%21RIV09-GA0-14330___
rdf:type
skos:Concept n17:Vysledek
dcterms:description
We present a new distributed-memory algorithm for enumerative LTL model-checking that is designed to be run on a cluster of workstations communicating via MPI. The detection of accepting cycles is based on computing maximal accepting predecessors and the subsequent decomposition of the graph into independent predecessor subgraphs induced by maximal accepting predecessors. Several optimizations of the basic algorithm are presented and the influence of the ordering on the algorithm performance is discussed. Experimental implementation of the algorithm shows promising results. We present a new distributed-memory algorithm for enumerative LTL model-checking that is designed to be run on a cluster of workstations communicating via MPI. The detection of accepting cycles is based on computing maximal accepting predecessors and the subsequent decomposition of the graph into independent predecessor subgraphs induced by maximal accepting predecessors. Several optimizations of the basic algorithm are presented and the influence of the ordering on the algorithm performance is discussed. Experimental implementation of the algorithm shows promising results. Článek prezentuje nový distribuovaný algoritmus pro ověřování LTL vlastností založený na akceptujících předchůdcích. Je prezentováné několik optimalizací a experimentální výsledky
dcterms:title
Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking. Akceptující předchůdci v distrubuovaném LTL ověřování modelů Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking.
skos:prefLabel
Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking. Akceptující předchůdci v distrubuovaném LTL ověřování modelů Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking.
skos:notation
RIV/00216224:14330/04:00010529!RIV09-GA0-14330___
n3:aktivita
n15:Z n15:P
n3:aktivity
P(GA201/03/0509), Z(MSM 143300001)
n3:dodaniDat
n16:2009
n3:domaciTvurceVysledku
n6:6656536 n6:2361132 n6:6500773 n6:9654674
n3:druhVysledku
n7:D
n3:duvernostUdaju
n18:S
n3:entitaPredkladatele
n20:predkladatel
n3:idSjednocenehoVysledku
553348
n3:idVysledku
RIV/00216224:14330/04:00010529
n3:jazykVysledku
n4:eng
n3:klicovaSlova
distributed - memory LTL model checking; graph predecessors
n3:klicoveSlovo
n11:distributed n11:graph%20predecessors
n3:kontrolniKodProRIV
[4DF18BA696C8]
n3:mistoKonaniAkce
Austin, USA
n3:mistoVydani
Neuveden
n3:nazevZdroje
Formal Methods in Computer-Aided Design (FMCAD)
n3:obor
n13:IN
n3:pocetDomacichTvurcuVysledku
4
n3:pocetTvurcuVysledku
4
n3:projekt
n12:GA201%2F03%2F0509
n3:rokUplatneniVysledku
n16:2004
n3:tvurceVysledku
Moravec, Pavel Brim, Luboš Černá, Ivana Šimša, Jiří
n3:typAkce
n10:WRD
n3:wos
000226785300025
n3:zahajeniAkce
2004-01-01+01:00
n3:zamer
n21:MSM%20143300001
s:numberOfPages
24
n22:hasPublisher
Springer-Verlag. LNCS
n5:isbn
3-540-23738-0
n14:organizacniJednotka
14330