This HTML5 document contains 51 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/
n19http://localhost/temp/predkladatel/
n14http://linked.opendata.cz/resource/domain/vavai/projekt/
n6http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n20http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216305%3A26230%2F11%3APU96118%21RIV12-MSM-26230___/
n8http://linked.opendata.cz/resource/domain/vavai/subjekt/
n7http://linked.opendata.cz/ontology/domain/vavai/
n18http://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#
n12http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n9http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n17http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n13http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n16http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n15http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n11http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216305%3A26230%2F11%3APU96118%21RIV12-MSM-26230___
rdf:type
skos:Concept n7:Vysledek
dcterms:description
The paper considers several issues related to efficient use of tree automata in formal verification. First, a new efficient algorithm for inclusion checking on non-deterministic tree automata is proposed. The algorithm traverses the automaton downward, utilizing antichains and simulations to optimize its run. Results of a set of experiments are provided, showing that such an approach often very significantly outperforms the so far common upward inclusion checking. Next, a new semi-symbolic representation of non-deterministic tree automata, suitable for automata with huge alphabets, is proposed together with algorithms for upward as well as downward inclusion checking over this representation of tree automata. Results of a set of experiments comparing the performance of these algorithms are provided, again showing that the newly proposed downward inclusion is very often better than upward inclusion checking. The paper considers several issues related to efficient use of tree automata in formal verification. First, a new efficient algorithm for inclusion checking on non-deterministic tree automata is proposed. The algorithm traverses the automaton downward, utilizing antichains and simulations to optimize its run. Results of a set of experiments are provided, showing that such an approach often very significantly outperforms the so far common upward inclusion checking. Next, a new semi-symbolic representation of non-deterministic tree automata, suitable for automata with huge alphabets, is proposed together with algorithms for upward as well as downward inclusion checking over this representation of tree automata. Results of a set of experiments comparing the performance of these algorithms are provided, again showing that the newly proposed downward inclusion is very often better than upward inclusion checking.
dcterms:title
Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata
skos:prefLabel
Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata
skos:notation
RIV/00216305:26230/11:PU96118!RIV12-MSM-26230___
n7:predkladatel
n8:orjk%3A26230
n3:aktivita
n13:Z n13:S n13:P
n3:aktivity
P(GAP103/10/0306), P(GD102/09/H042), P(OC10009), S, Z(MSM0021630528)
n3:cisloPeriodika
6996
n3:dodaniDat
n11:2012
n3:domaciTvurceVysledku
n6:7182430 n6:1258486 n6:1316850 n6:9761985
n3:druhVysledku
n16:J
n3:duvernostUdaju
n9:S
n3:entitaPredkladatele
n20:predkladatel
n3:idSjednocenehoVysledku
196752
n3:idVysledku
RIV/00216305:26230/11:PU96118
n3:jazykVysledku
n17:eng
n3:klicovaSlova
tree automata, binary decision diagrams, language inclusion, downward inclusion checking, symbolic encoding
n3:klicoveSlovo
n12:symbolic%20encoding n12:tree%20automata n12:binary%20decision%20diagrams n12:downward%20inclusion%20checking n12:language%20inclusion
n3:kodStatuVydavatele
DE - Spolková republika Německo
n3:kontrolniKodProRIV
[EDB7919E21CF]
n3:nazevZdroje
Lecture Notes in Computer Science (IF 0,513)
n3:obor
n15:IN
n3:pocetDomacichTvurcuVysledku
4
n3:pocetTvurcuVysledku
4
n3:projekt
n14:GD102%2F09%2FH042 n14:GAP103%2F10%2F0306 n14:OC10009
n3:rokUplatneniVysledku
n11:2011
n3:svazekPeriodika
2011
n3:tvurceVysledku
Šimáček, Jiří Lengál, Ondřej Holík, Lukáš Vojnar, Tomáš
n3:zamer
n18:MSM0021630528
s:issn
0302-9743
s:numberOfPages
16
n19:organizacniJednotka
26230