Characteristic Patterns for LTL

KUČERA, Antonín a Jan STREJČEK. Characteristic Patterns for LTL. P. Vojtas, M. Bielikova, B. Charron-Bost, O. Sykora (Eds.). In SOFSEM 2005: Theory and Practice of Computer Science. Berlin, Heidelberg: Springer-Verlag, 2005, s. 239-249. ISBN 3-540-24302-X.

Základní údaje

Originální název

Characteristic Patterns for LTL

Název česky

Charakteristické vzorce pro LTL

Autoři

KUČERA, Antonín (203 Česká republika, garant) a Jan STREJČEK (203 Česká republika)
P. Vojtas, M. Bielikova, B. Charron-Bost, O. Sykora (Eds.).

Vydání

Berlin, Heidelberg, SOFSEM 2005: Theory and Practice of Computer Science, od s. 239-249, 11 s. 2005

Nakladatel

Springer-Verlag

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Slovensko

Utajení

není předmětem státního či obchodního tajemství

Kód RIV

RIV/00216224:14330/05:00012348

Organizační jednotka

Fakulta informatiky

ISBN

3-540-24302-X

UT WoS

000228554400027

Klíčová slova anglicky

model-checking; linear temporal logic

Štítky

linear temporal logic, Model-Checking

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

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.

Česky

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.

---

Návaznosti

GA201/03/1161, projekt VaV	Název: Verifikace nekonečně stavových systémů Investor: Grantová agentura ČR, Verifikace nekonečně stavových systémů
MSM0021622419, záměr	Název: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky