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

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

Namespace Prefixes

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

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F13%3A00066204%21RIV14-MSM-14330___
rdf:type
n15:Vysledek skos:Concept
dcterms:description
We present a tool that generates automata for LTL(X,F,G,U) where U does not occur in any G-formula (but F still can). The tool generates deterministic generalized Rabin automata (DGRA) significantly smaller than deterministic Rabin automata (DRA) generated by state-of-the-art tools. For complex properties such as fairness constraints, the difference is in orders of magnitude. DGRA have been recently shown to be as useful in probabilistic model checking as DRA, hence the difference in size directly translates to a speed up of the model checking procedures. We present a tool that generates automata for LTL(X,F,G,U) where U does not occur in any G-formula (but F still can). The tool generates deterministic generalized Rabin automata (DGRA) significantly smaller than deterministic Rabin automata (DRA) generated by state-of-the-art tools. For complex properties such as fairness constraints, the difference is in orders of magnitude. DGRA have been recently shown to be as useful in probabilistic model checking as DRA, hence the difference in size directly translates to a speed up of the model checking procedures.
dcterms:title
Rabinizer 2: Small Deterministic Automata for LTL\GU Rabinizer 2: Small Deterministic Automata for LTL\GU
skos:prefLabel
Rabinizer 2: Small Deterministic Automata for LTL\GU Rabinizer 2: Small Deterministic Automata for LTL\GU
skos:notation
RIV/00216224:14330/13:00066204!RIV14-MSM-14330___
n15:predkladatel
n16:orjk%3A14330
n4:aktivita
n10:S n10:P
n4:aktivity
P(GBP202/12/G061), S
n4:dodaniDat
n20:2014
n4:domaciTvurceVysledku
n18:3503054
n4:druhVysledku
n21:D
n4:duvernostUdaju
n17:S
n4:entitaPredkladatele
n9:predkladatel
n4:idSjednocenehoVysledku
101291
n4:idVysledku
RIV/00216224:14330/13:00066204
n4:jazykVysledku
n23:eng
n4:klicovaSlova
linear temporal logic; automata; determinism; synthesis; probabilistic model checking
n4:klicoveSlovo
n5:synthesis n5:determinism n5:automata n5:probabilistic%20model%20checking n5:linear%20temporal%20logic
n4:kontrolniKodProRIV
[9DEFF2F0BBBD]
n4:mistoKonaniAkce
Heidelberg Dordrecht London New York
n4:mistoVydani
Heidelberg Dordrecht London New York
n4:nazevZdroje
Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013
n4:obor
n22:IN
n4:pocetDomacichTvurcuVysledku
1
n4:pocetTvurcuVysledku
2
n4:projekt
n13:GBP202%2F12%2FG061
n4:rokUplatneniVysledku
n20:2013
n4:tvurceVysledku
Křetínský, Jan Ledesma Garza, Ruslan
n4:typAkce
n8:WRD
n4:zahajeniAkce
2013-01-01+01:00
s:issn
0302-9743
s:numberOfPages
5
n7:doi
10.1007/978-3-319-02444-8_32
n11:hasPublisher
Springer-Verlag
n14:isbn
9783319024431
n12:organizacniJednotka
14330