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/
n16http://localhost/temp/predkladatel/
n14http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n5http://linked.opendata.cz/resource/domain/vavai/projekt/
n18http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216224%3A14330%2F05%3A00012348%21RIV08-MSM-14330___/
n10http://linked.opendata.cz/ontology/domain/vavai/
n12http://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#
n11http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n9http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n19http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n13http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n15http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n8http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n4http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F05%3A00012348%21RIV08-MSM-14330___
rdf:type
skos:Concept n10:Vysledek
dcterms:description
We give a new characterization of those languages that are definable in fragments of LTL where the nesting depths of X and U modalities are bounded by given constants. This brings further results about various LTL fragments. We also propose a generic method for decomposing LTL formulae into an equivalent disjunction of "semantically refined" LTL formulae, and indicate how this result can be used to improve the functionality of existing LTL model-checkers. We give a new characterization of those languages that are definable in fragments of LTL where the nesting depths of X and U modalities are bounded by given constants. This brings further results about various LTL fragments. We also propose a generic method for decomposing LTL formulae into an equivalent disjunction of "semantically refined" LTL formulae, and indicate how this result can be used to improve the functionality of existing LTL model-checkers. Popisujeme nové charakterizace jazyků, které jsou definovatelné pomocí fragmentů LTL s danou hloubkou zanoření operátorů X a U. Tyto charakterizace využívá nově navržená obecná metoda rozkladu LTL formule na ekvivalentní disjunkci "sémanticky jemnějších" formulí. Dále ukazujeme, jak může být tento rozklad použit k vylepšení existujících nástrojů pro LTL model checking.
dcterms:title
Characteristic Patterns for LTL Characteristic Patterns for LTL Charakteristické vzorce pro LTL
skos:prefLabel
Charakteristické vzorce pro LTL Characteristic Patterns for LTL Characteristic Patterns for LTL
skos:notation
RIV/00216224:14330/05:00012348!RIV08-MSM-14330___
n3:strany
239-249
n3:aktivita
n13:Z n13:P
n3:aktivity
P(1M0545), P(GA201/03/1161), Z(MSM0021622419)
n3:cisloPeriodika
3381
n3:dodaniDat
n4:2008
n3:domaciTvurceVysledku
n14:3978915 n14:9872655
n3:druhVysledku
n15:J
n3:duvernostUdaju
n9:S
n3:entitaPredkladatele
n18:predkladatel
n3:idSjednocenehoVysledku
514985
n3:idVysledku
RIV/00216224:14330/05:00012348
n3:jazykVysledku
n19:eng
n3:klicovaSlova
model-checking; linear temporal logic
n3:klicoveSlovo
n11:linear%20temporal%20logic n11:model-checking
n3:kodStatuVydavatele
SK - Slovenská republika
n3:kontrolniKodProRIV
[C330CD5B5296]
n3:nazevZdroje
Lecture Notes in Computer Science
n3:obor
n8:IN
n3:pocetDomacichTvurcuVysledku
2
n3:pocetTvurcuVysledku
2
n3:projekt
n5:GA201%2F03%2F1161 n5:1M0545
n3:rokUplatneniVysledku
n4:2005
n3:svazekPeriodika
2005
n3:tvurceVysledku
Kučera, Antonín Strejček, Jan
n3:zamer
n12:MSM0021622419
s:issn
0302-9743
s:numberOfPages
11
n16:organizacniJednotka
14330