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

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

Namespace Prefixes

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

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F14%3A00076564%21RIV15-MSM-14330___
rdf:type
n13:Vysledek skos:Concept
dcterms:description
We introduce the Clock-Aware Linear Temporal Logic (CA-LTL) for expressing linear time properties of timed automata, and show how to apply the standard automata-based approach of Vardi and Wolper to check for the validity of a CA-LTL formula over the continuous-time semantics of a timed automaton. Our model checking procedure employs zone-based abstraction and a new concept of the so called ultraregions. We also show that the Timed Büchi Automaton Emptiness problem is not the problem that the intended automata-based approach to CA-LTL model checking is reduced to. Finally, we give the necessary proofs of correctness, some hints for an efficient implementation, and preliminary experimental evaluation of our technique. We introduce the Clock-Aware Linear Temporal Logic (CA-LTL) for expressing linear time properties of timed automata, and show how to apply the standard automata-based approach of Vardi and Wolper to check for the validity of a CA-LTL formula over the continuous-time semantics of a timed automaton. Our model checking procedure employs zone-based abstraction and a new concept of the so called ultraregions. We also show that the Timed Büchi Automaton Emptiness problem is not the problem that the intended automata-based approach to CA-LTL model checking is reduced to. Finally, we give the necessary proofs of correctness, some hints for an efficient implementation, and preliminary experimental evaluation of our technique.
dcterms:title
On Clock-Aware LTL Properties of Timed Automata On Clock-Aware LTL Properties of Timed Automata
skos:prefLabel
On Clock-Aware LTL Properties of Timed Automata On Clock-Aware LTL Properties of Timed Automata
skos:notation
RIV/00216224:14330/14:00076564!RIV15-MSM-14330___
n3:aktivita
n18:P
n3:aktivity
P(EE2.3.30.0009), P(LH11065)
n3:dodaniDat
n11:2015
n3:domaciTvurceVysledku
n6:4376447 n6:5692792 n6:3095673 n6:2050587 n6:2361132
n3:druhVysledku
n22:D
n3:duvernostUdaju
n15:S
n3:entitaPredkladatele
n16:predkladatel
n3:idSjednocenehoVysledku
34250
n3:idVysledku
RIV/00216224:14330/14:00076564
n3:jazykVysledku
n19:eng
n3:klicovaSlova
Linear Temporal Logic; Timed Automata; Automata-based Model Checking
n3:klicoveSlovo
n5:Linear%20Temporal%20Logic n5:Timed%20Automata n5:Automata-based%20Model%20Checking
n3:kontrolniKodProRIV
[AEE613D55B18]
n3:mistoKonaniAkce
Bucharest, Romania
n3:mistoVydani
Neuveden
n3:nazevZdroje
Theoretical Aspects of Computing – ICTAC 2014
n3:obor
n17:IN
n3:pocetDomacichTvurcuVysledku
5
n3:pocetTvurcuVysledku
5
n3:projekt
n10:EE2.3.30.0009 n10:LH11065
n3:rokUplatneniVysledku
n11:2014
n3:tvurceVysledku
Beneš, Nikola Bezděk, Peter Havel, Vojtěch Barnat, Jiří Černá, Ivana
n3:typAkce
n20:WRD
n3:zahajeniAkce
2014-01-01+01:00
s:issn
0302-9743
s:numberOfPages
18
n14:doi
10.1007/978-3-319-10882-7_4
n8:hasPublisher
Springer International Publishing
n21:isbn
9783319108810
n12:organizacniJednotka
14330