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. s. 239-249. ISBN 3-540-24302-X. 2005.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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
Změnil Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 29. 3. 2010 14:38.
Anotace
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.
Anotace č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 VaVNázev: Verifikace nekonečně stavových systémů
Investor: Grantová agentura ČR, Verifikace nekonečně stavových systémů
MSM0021622419, záměrNá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 VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky
VytisknoutZobrazeno: 29. 3. 2024 13:33