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

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

Namespace Prefixes

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

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F02%3A00006381%21RIV08-MSM-14330___
rdf:type
skos:Concept n22:Vysledek
dcterms:description
It is known that LTL formulae without the `next' operator are invariant under the so-called stutter-equivalence of words. In this paper we extend this principle to general LTL formulae with given nesting depths of the `next' and `until' operators. This allows us to prove the semantical strictness of three natural hierarchies of LTL formulae, which are parametrized either by the nesting depth of just one of the two operators, or by both of them. As another interesting corollary we obtain an alternative characterization of LTL languages, which are exactly the regular languages closed under the generalized form of stutter equivalence. We also indicate how to tackle the state-space explosion problem with the help of presented results. It is known that LTL formulae without the `next' operator are invariant under the so-called stutter-equivalence of words. In this paper we extend this principle to general LTL formulae with given nesting depths of the `next' and `until' operators. This allows us to prove the semantical strictness of three natural hierarchies of LTL formulae, which are parametrized either by the nesting depth of just one of the two operators, or by both of them. As another interesting corollary we obtain an alternative characterization of LTL languages, which are exactly the regular languages closed under the generalized form of stutter equivalence. We also indicate how to tackle the state-space explosion problem with the help of presented results. It is known that LTL formulae without the `next' operator are invariant under the so-called stutter-equivalence of words. In this paper we extend this principle to general LTL formulae with given nesting depths of the `next' and `until' operators. This allows us to prove the semantical strictness of three natural hierarchies of LTL formulae, which are parametrized either by the nesting depth of just one of the two operators, or by both of them. As another interesting corollary we obtain an alternative characterization of LTL languages, which are exactly the regular languages closed under the generalized form of stutter equivalence. We also indicate how to tackle the state-space explosion problem with the help of presented results.
dcterms:title
The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL
skos:prefLabel
The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL
skos:notation
RIV/00216224:14330/02:00006381!RIV08-MSM-14330___
n4:strany
276
n4:aktivita
n16:P n16:Z
n4:aktivity
P(GA201/00/0400), P(GA201/00/1023), Z(MSM 143300001)
n4:dodaniDat
n18:2008
n4:domaciTvurceVysledku
n14:3978915 n14:9872655
n4:druhVysledku
n10:D
n4:duvernostUdaju
n20:S
n4:entitaPredkladatele
n15:predkladatel
n4:idSjednocenehoVysledku
665827
n4:idVysledku
RIV/00216224:14330/02:00006381
n4:jazykVysledku
n6:eng
n4:klicovaSlova
verification; concurrency; weak bisimilarity; infinite-state systems
n4:klicoveSlovo
n7:infinite-state%20systems n7:concurrency n7:weak%20bisimilarity n7:verification
n4:kontrolniKodProRIV
[08B89A45EAA7]
n4:mistoKonaniAkce
September 22-25, 2002, Edinburgh, Scotland
n4:mistoVydani
Berlin
n4:nazevZdroje
Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL'02)
n4:obor
n13:JC
n4:pocetDomacichTvurcuVysledku
2
n4:pocetTvurcuVysledku
2
n4:projekt
n12:GA201%2F00%2F1023 n12:GA201%2F00%2F0400
n4:rokUplatneniVysledku
n18:2002
n4:tvurceVysledku
Strejček, Jan Kučera, Antonín
n4:typAkce
n9:WRD
n4:zahajeniAkce
2002-01-01+01:00
n4:zamer
n21:MSM%20143300001
s:numberOfPages
16
n11:hasPublisher
Springer-Verlag
n19:isbn
3-540-44240-5
n17:organizacniJednotka
14330