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
dctermshttp://purl.org/dc/terms/
n7http://localhost/temp/predkladatel/
n16http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n4http://linked.opendata.cz/resource/domain/vavai/projekt/
n8http://linked.opendata.cz/ontology/domain/vavai/
n5http://linked.opendata.cz/resource/domain/vavai/zamer/
shttp://schema.org/
skoshttp://www.w3.org/2004/02/skos/core#
n3http://linked.opendata.cz/ontology/domain/vavai/riv/
n2http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n10http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n13http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n18http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n11http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n12http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n9http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n19http://reference.data.gov.uk/id/gregorian-year/
n17http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216224%3A14330%2F06%3A00015564%21RIV10-GA0-14330___/

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F06%3A00015564%21RIV10-GA0-14330___
rdf:type
n8:Vysledek skos:Concept
dcterms:description
Timed automata have an infinite semantics. For verification purposes, one usually uses zone based abstractions w.r.t. the maximal constants to which clocks of the timed automaton are compared. We show that by distinguishing maximal lower and upper bounds, significantly coarser abstractions can be obtained. We show soundness and completeness of the new abstractions w.r.t. reachability. We demonstrate how information about lower and upper bounds can be used to optimise the algorithm for bringing a difference bound matrix into normal form. Finally, we experimentally demonstrate that the new techniques dramatically increases the scalability of the real-time model checker Uppaal. Timed automata have an infinite semantics. For verification purposes, one usually uses zone based abstractions w.r.t. the maximal constants to which clocks of the timed automaton are compared. We show that by distinguishing maximal lower and upper bounds, significantly coarser abstractions can be obtained. We show soundness and completeness of the new abstractions w.r.t. reachability. We demonstrate how information about lower and upper bounds can be used to optimise the algorithm for bringing a difference bound matrix into normal form. Finally, we experimentally demonstrate that the new techniques dramatically increases the scalability of the real-time model checker Uppaal.
dcterms:title
Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata
skos:prefLabel
Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata
skos:notation
RIV/00216224:14330/06:00015564!RIV10-GA0-14330___
n3:aktivita
n11:P n11:Z
n3:aktivity
P(1M0545), P(GA201/03/0509), Z(MSM0021622419)
n3:cisloPeriodika
3
n3:dodaniDat
n19:2010
n3:domaciTvurceVysledku
n16:4686128
n3:druhVysledku
n12:J
n3:duvernostUdaju
n13:S
n3:entitaPredkladatele
n17:predkladatel
n3:idSjednocenehoVysledku
483684
n3:idVysledku
RIV/00216224:14330/06:00015564
n3:jazykVysledku
n18:eng
n3:klicovaSlova
model checking; timed automata; verification; abstraction; extrapolation
n3:klicoveSlovo
n10:verification n10:extrapolation n10:model%20checking n10:timed%20automata n10:abstraction
n3:kodStatuVydavatele
DE - Spolková republika Německo
n3:kontrolniKodProRIV
[31F6D699F06D]
n3:nazevZdroje
International Journal on Software Tools for Technology Transfer (STTT)
n3:obor
n9:IN
n3:pocetDomacichTvurcuVysledku
1
n3:pocetTvurcuVysledku
4
n3:projekt
n4:1M0545 n4:GA201%2F03%2F0509
n3:rokUplatneniVysledku
n19:2006
n3:svazekPeriodika
8
n3:tvurceVysledku
Larsen, Kim G. Behrmann, Gerd Pelánek, Radek Bouyer, Patricia
n3:zamer
n5:MSM0021622419
s:issn
1433-2779
s:numberOfPages
12
n7:organizacniJednotka
14330