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
n14http://linked.opendata.cz/ontology/domain/vavai/riv/typAkce/
dctermshttp://purl.org/dc/terms/
n22http://purl.org/net/nknouf/ns/bibtex#
n18http://localhost/temp/predkladatel/
n21http://linked.opendata.cz/resource/domain/vavai/projekt/
n10http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n17http://linked.opendata.cz/ontology/domain/vavai/
n13http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216224%3A14330%2F14%3A00073720%21RIV15-MSM-14330___/
n9https://schema.org/
shttp://schema.org/
n6http://linked.opendata.cz/ontology/domain/vavai/riv/
skoshttp://www.w3.org/2004/02/skos/core#
n4http://bibframe.org/vocab/
n2http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n7http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n8http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n19http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n16http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n20http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n15http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n11http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F14%3A00073720%21RIV15-MSM-14330___
rdf:type
skos:Concept n17:Vysledek
dcterms:description
We present a tool for translating LTL formulae into deterministic automata. It is the first tool that covers the whole LTL, while not using Safra's determinization or any of its variants, which leads to smaller automata. There are several outputs of the tool: firstly, deterministic Rabin automata, which are the standard input for probabilistic model checking, e.g. for the probabilistic model-checker PRISM; secondly, deterministic generalized Rabin automata, which can also be used for probabilistic model checking and are sometimes by orders of magnitude smaller. We also link our tool to PRISM and show that this leads to a significant speed-up of probabilistic LTL model checking, especially with the generalized Rabin automata. We present a tool for translating LTL formulae into deterministic automata. It is the first tool that covers the whole LTL, while not using Safra's determinization or any of its variants, which leads to smaller automata. There are several outputs of the tool: firstly, deterministic Rabin automata, which are the standard input for probabilistic model checking, e.g. for the probabilistic model-checker PRISM; secondly, deterministic generalized Rabin automata, which can also be used for probabilistic model checking and are sometimes by orders of magnitude smaller. We also link our tool to PRISM and show that this leads to a significant speed-up of probabilistic LTL model checking, especially with the generalized Rabin automata.
dcterms:title
Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata
skos:prefLabel
Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata
skos:notation
RIV/00216224:14330/14:00073720!RIV15-MSM-14330___
n6:aktivita
n19:S n19:P
n6:aktivity
P(GBP202/12/G061), S
n6:dodaniDat
n11:2015
n6:domaciTvurceVysledku
n10:4723260 n10:3503054
n6:druhVysledku
n15:D
n6:duvernostUdaju
n8:S
n6:entitaPredkladatele
n13:predkladatel
n6:idSjednocenehoVysledku
41164
n6:idVysledku
RIV/00216224:14330/14:00073720
n6:jazykVysledku
n16:eng
n6:klicovaSlova
linear temporal logic; automata; determinism; synthesis; probabilistic model checking
n6:klicoveSlovo
n7:automata n7:linear%20temporal%20logic n7:probabilistic%20model%20checking n7:synthesis n7:determinism
n6:kontrolniKodProRIV
[44E59CAC2336]
n6:mistoKonaniAkce
Heidelberg Dordrecht London New York
n6:mistoVydani
Heidelberg Dordrecht London New York
n6:nazevZdroje
Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014
n6:obor
n20:IN
n6:pocetDomacichTvurcuVysledku
2
n6:pocetTvurcuVysledku
2
n6:projekt
n21:GBP202%2F12%2FG061
n6:rokUplatneniVysledku
n11:2014
n6:tvurceVysledku
Křetínský, Jan Komárková, Zuzana
n6:typAkce
n14:WRD
n6:zahajeniAkce
2014-01-01+01:00
s:issn
0302-9743
s:numberOfPages
7
n4:doi
10.1007/978-3-319-11936-6_17
n22:hasPublisher
Springer-Verlag
n9:isbn
9783319119359
n18:organizacniJednotka
14330