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
dctermshttp://purl.org/dc/terms/
n12http://localhost/temp/predkladatel/
n16http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n6http://linked.opendata.cz/resource/domain/vavai/projekt/
n8http://linked.opendata.cz/ontology/domain/vavai/
n14http://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/resource/domain/vavai/vysledek/RIV%2F00216224%3A14330%2F06%3A00015453%21RIV10-GA0-14330___/
n4http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n17http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n19http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n13http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n18http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n5http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n9http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F06%3A00015453%21RIV10-GA0-14330___
rdf:type
n8:Vysledek skos:Concept
dcterms:description
The distributed automata-based LTL model-checking relies on algorithms for finding accepting cycles in a B\"{u}chi automaton. One approach to distributed accepting cycle detection is based on maximal accepting predecessors. The ordering of accepting states (hence the maximality) is one of the main factors affecting the overall complexity of model-checking as imperfect ordering can enforce numerous re-explorations of the automaton. This paper addresses the problem of finding an optimal ordering, proves its hardness, and gives several heuristics for finding an optimal ordering in the distributed environment. We compare the heuristics both theoretically and experimentally, and find out which of these work well. The distributed automata-based LTL model-checking relies on algorithms for finding accepting cycles in a B\"{u}chi automaton. One approach to distributed accepting cycle detection is based on maximal accepting predecessors. The ordering of accepting states (hence the maximality) is one of the main factors affecting the overall complexity of model-checking as imperfect ordering can enforce numerous re-explorations of the automaton. This paper addresses the problem of finding an optimal ordering, proves its hardness, and gives several heuristics for finding an optimal ordering in the distributed environment. We compare the heuristics both theoretically and experimentally, and find out which of these work well.
dcterms:title
How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors
skos:prefLabel
How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors
skos:notation
RIV/00216224:14330/06:00015453!RIV10-GA0-14330___
n3:aktivita
n13:Z n13:P
n3:aktivity
P(1ET408050503), P(1M0545), P(GA201/03/0509), P(GD102/05/H050), Z(MSM0021622419)
n3:cisloPeriodika
2
n3:dodaniDat
n9:2010
n3:domaciTvurceVysledku
n16:2361132 n16:6500773 n16:6656536 n16:9654674
n3:druhVysledku
n18:J
n3:duvernostUdaju
n17:S
n3:entitaPredkladatele
n15:predkladatel
n3:idSjednocenehoVysledku
478302
n3:idVysledku
RIV/00216224:14330/06:00015453
n3:jazykVysledku
n19:eng
n3:klicovaSlova
accepting predecessors; LTL model checking
n3:klicoveSlovo
n4:accepting%20predecessors n4:LTL%20model%20checking
n3:kodStatuVydavatele
PT - Portugalská republika
n3:kontrolniKodProRIV
[18083FC1EC79]
n3:nazevZdroje
Electronic Notes in Theoretical Computer Science
n3:obor
n5:IN
n3:pocetDomacichTvurcuVysledku
4
n3:pocetTvurcuVysledku
4
n3:projekt
n6:1ET408050503 n6:GD102%2F05%2FH050 n6:1M0545 n6:GA201%2F03%2F0509
n3:rokUplatneniVysledku
n9:2006
n3:svazekPeriodika
135
n3:tvurceVysledku
Černá, Ivana Brim, Luboš Šimša, Jiří Moravec, Pavel
n3:zamer
n14:MSM0021622419
s:issn
1571-0661
s:numberOfPages
15
n12:organizacniJednotka
14330