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

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

Namespace Prefixes

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

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F13%3A00066175%21RIV14-MSM-14330___
rdf:type
n10:Vysledek skos:Concept
dcterms:description
Some applications of linear temporal logic (LTL) require to translate formulae of the logic to deterministic omega-automata. There are currently two translators producing deterministic automata: ltl2dstar working for the whole LTL and Rabinizer applicable to the fragment LTL(F,G). We present a new translation to deterministic Rabin automata via alternating automata and deterministic transition-based generalized Rabin automata. Our translation applies to a fragment that is strictly larger than LTL(F,G). Experimental results show that our algorithm can produce significantly smaller automata compared to Rabinizer and ltl2dstar, especially for more complex LTL formulae. Some applications of linear temporal logic (LTL) require to translate formulae of the logic to deterministic omega-automata. There are currently two translators producing deterministic automata: ltl2dstar working for the whole LTL and Rabinizer applicable to the fragment LTL(F,G). We present a new translation to deterministic Rabin automata via alternating automata and deterministic transition-based generalized Rabin automata. Our translation applies to a fragment that is strictly larger than LTL(F,G). Experimental results show that our algorithm can produce significantly smaller automata compared to Rabinizer and ltl2dstar, especially for more complex LTL formulae.
dcterms:title
Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment
skos:prefLabel
Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment
skos:notation
RIV/00216224:14330/13:00066175!RIV14-MSM-14330___
n10:predkladatel
n18:orjk%3A14330
n3:aktivita
n21:S n21:P n21:I
n3:aktivity
I, P(GBP202/12/G061), S
n3:dodaniDat
n7:2014
n3:domaciTvurceVysledku
n9:3978915 n9:1425234 n9:9653023 n9:5598095
n3:druhVysledku
n19:D
n3:duvernostUdaju
n6:S
n3:entitaPredkladatele
n12:predkladatel
n3:idSjednocenehoVysledku
71879
n3:idVysledku
RIV/00216224:14330/13:00066175
n3:jazykVysledku
n15:eng
n3:klicovaSlova
linear temporal logic; deterministic omega-automata
n3:klicoveSlovo
n13:linear%20temporal%20logic n13:deterministic%20omega-automata
n3:kontrolniKodProRIV
[B43063C27353]
n3:mistoKonaniAkce
Hanoi, Vietnam
n3:mistoVydani
Berlin Heidelberg
n3:nazevZdroje
11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013
n3:obor
n22:IN
n3:pocetDomacichTvurcuVysledku
4
n3:pocetTvurcuVysledku
4
n3:projekt
n20:GBP202%2F12%2FG061
n3:rokUplatneniVysledku
n7:2013
n3:tvurceVysledku
Babiak, Tomáš Křetínský, Mojmír Strejček, Jan Blahoudek, František
n3:typAkce
n14:WRD
n3:zahajeniAkce
2013-01-01+01:00
s:issn
0302-9743
s:numberOfPages
15
n17:doi
10.1007/978-3-319-02444-8_4
n23:hasPublisher
Springer-Verlag
n5:isbn
9783319024431
n11:organizacniJednotka
14330