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

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F14%3A00073709%21RIV15-MSM-14330___
rdf:type
skos:Concept n22:Vysledek
dcterms:description
We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula phi. The automaton is the product of a master automaton and an array of slave automata, one for each G-subformula of phi. The slave automaton for G(psi) is in charge of recognizing whether FG(psi) holds. As opposed to standard determinization procedures, the states of all our automata have a clear logical structure, which allows for various optimizations. Our construction subsumes former algorithms for fragments of LTL. Experimental results show improvement in the sizes of the resulting automata compared to existing methods. We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula phi. The automaton is the product of a master automaton and an array of slave automata, one for each G-subformula of phi. The slave automaton for G(psi) is in charge of recognizing whether FG(psi) holds. As opposed to standard determinization procedures, the states of all our automata have a clear logical structure, which allows for various optimizations. Our construction subsumes former algorithms for fragments of LTL. Experimental results show improvement in the sizes of the resulting automata compared to existing methods.
dcterms:title
From LTL to Deterministic Automata: A Safraless Compositional Approach From LTL to Deterministic Automata: A Safraless Compositional Approach
skos:prefLabel
From LTL to Deterministic Automata: A Safraless Compositional Approach From LTL to Deterministic Automata: A Safraless Compositional Approach
skos:notation
RIV/00216224:14330/14:00073709!RIV15-MSM-14330___
n4:aktivita
n10:S n10:P
n4:aktivity
P(GBP202/12/G061), S
n4:dodaniDat
n5:2015
n4:domaciTvurceVysledku
n20:3503054
n4:druhVysledku
n16:D
n4:duvernostUdaju
n8:S
n4:entitaPredkladatele
n15:predkladatel
n4:idSjednocenehoVysledku
17559
n4:idVysledku
RIV/00216224:14330/14:00073709
n4:jazykVysledku
n13:eng
n4:klicovaSlova
linear temporal logic; automata; determinism; synthesis; probabilistic model checking
n4:klicoveSlovo
n7:probabilistic%20model%20checking n7:automata n7:determinism n7:linear%20temporal%20logic n7:synthesis
n4:kontrolniKodProRIV
[55BB8D641D20]
n4:mistoKonaniAkce
Heidelberg Dordrecht London New York
n4:mistoVydani
Heidelberg Dordrecht London New York
n4:nazevZdroje
Computer Aided Verification - 26th International Conference, CAV 2014
n4:obor
n18:IN
n4:pocetDomacichTvurcuVysledku
1
n4:pocetTvurcuVysledku
2
n4:projekt
n11:GBP202%2F12%2FG061
n4:rokUplatneniVysledku
n5:2014
n4:tvurceVysledku
Esparza, Javier Křetínský, Jan
n4:typAkce
n14:WRD
n4:zahajeniAkce
2014-01-01+01:00
s:issn
0302-9743
s:numberOfPages
17
n9:doi
10.1007/978-3-319-08867-9_13
n19:hasPublisher
Springer-Verlag
n21:isbn
9783319088662
n17:organizacniJednotka
14330