Znovu o principu periodických vzorů

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F05%3A00012554" target="_blank" >RIV/00216224:14330/05:00012554 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

The stuttering principle revisited

Popis výsledku v původním jazyce

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 both `next' and `until' operators. Thisallows 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. Further, we provide an effective characterization of languages definable by LTL formulae with a bounded nesting depth of the `next' operator.

Název v anglickém jazyce

The stuttering principle revisited

Popis výsledku anglicky

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 both `next' and `until' operators. Thisallows 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. Further, we provide an effective characterization of languages definable by LTL formulae with a bounded nesting depth of the `next' operator.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2005

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Acta informatica

ISSN

0001-5903

e-ISSN

—

Svazek periodika

41

Číslo periodika v rámci svazku

7/8

Stát vydavatele periodika

DE - Spolková republika Německo

Počet stran výsledku

20

Strana od-do

415-434

Kód UT WoS článku

—

EID výsledku v databázi Scopus

—