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

Statements

Subject Item
n2:RIV%2F00216305%3A26230%2F11%3APU96126%21RIV12-MSM-26230___
rdf:type
skos:Concept n14:Vysledek
dcterms:description
Checking language inclusion between two nondeterministic Büchi automata A and B is computationally hard (PSPACE-complete). However, several approaches which are efficient in many practical cases have been proposed. We build on one of these, which is known as the Ramsey-based approach. It has recently been shown that the basic Ramsey-based approach can be drastically optimized by using powerful subsumption techniques, which allow one to prune the search-space when looking for counterexamples to inclusion. While previous works only used subsumption based on set inclusion or forward simulation on A and B, we propose the following new techniques: (1) A larger subsumption relation based on a combination of backward and forward simulations on A and B. (2) A method to additionally use forward simulation between A and B. (3) Abstraction techniques that can speed up the computation and lead to early detection of counterexamples. The new algorithm was implemented and tested on automata derived from Checking language inclusion between two nondeterministic Büchi automata A and B is computationally hard (PSPACE-complete). However, several approaches which are efficient in many practical cases have been proposed. We build on one of these, which is known as the Ramsey-based approach. It has recently been shown that the basic Ramsey-based approach can be drastically optimized by using powerful subsumption techniques, which allow one to prune the search-space when looking for counterexamples to inclusion. While previous works only used subsumption based on set inclusion or forward simulation on A and B, we propose the following new techniques: (1) A larger subsumption relation based on a combination of backward and forward simulations on A and B. (2) A method to additionally use forward simulation between A and B. (3) Abstraction techniques that can speed up the computation and lead to early detection of counterexamples. The new algorithm was implemented and tested on automata derived from
dcterms:title
Advanced Ramsey-based Büchi Automata Inclusion Testing Advanced Ramsey-based Büchi Automata Inclusion Testing
skos:prefLabel
Advanced Ramsey-based Büchi Automata Inclusion Testing Advanced Ramsey-based Büchi Automata Inclusion Testing
skos:notation
RIV/00216305:26230/11:PU96126!RIV12-MSM-26230___
n14:predkladatel
n15:orjk%3A26230
n3:aktivita
n7:Z n7:S n7:P
n3:aktivity
P(GAP103/10/0306), P(GD102/09/H042), P(OC10009), S, Z(MSM0021630528)
n3:cisloPeriodika
6901
n3:dodaniDat
n4:2012
n3:domaciTvurceVysledku
n17:1258486 n17:9761985
n3:druhVysledku
n16:J
n3:duvernostUdaju
n19:S
n3:entitaPredkladatele
n8:predkladatel
n3:idSjednocenehoVysledku
184741
n3:idVysledku
RIV/00216305:26230/11:PU96126
n3:jazykVysledku
n12:eng
n3:klicovaSlova
Büchi automata, inclusion checking, Ramsey theorem, simulation relations
n3:klicoveSlovo
n13:B%C3%BCchi%20automata n13:inclusion%20checking n13:simulation%20relations n13:Ramsey%20theorem
n3:kodStatuVydavatele
DE - Spolková republika Německo
n3:kontrolniKodProRIV
[06A777AF9607]
n3:nazevZdroje
Lecture Notes in Computer Science (IF 0,513)
n3:obor
n9:IN
n3:pocetDomacichTvurcuVysledku
2
n3:pocetTvurcuVysledku
7
n3:projekt
n5:GAP103%2F10%2F0306 n5:GD102%2F09%2FH042 n5:OC10009
n3:rokUplatneniVysledku
n4:2011
n3:svazekPeriodika
2011
n3:tvurceVysledku
Abdulla, Parosh Holík, Lukáš Mayr, Richard Clemente, Lorenzo Hong, Chih-Duo Vojnar, Tomáš Chen, Yu-Fang
n3:zamer
n18:MSM0021630528
s:issn
0302-9743
s:numberOfPages
16
n20:organizacniJednotka
26230