Characteristic Patterns for LTL

Varování

Publikace nespadá pod Ústav výpočetní techniky, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Název česky	Charakteristické vzorce pro LTL
Autoři	KUČERA Antonín STREJČEK Jan
Rok publikování	2005
Druh	Článek ve sborníku
Konference	SOFSEM 2005: Theory and Practice of Computer Science
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
Obor	Informatika
Klíčová slova	model-checking; linear temporal logic
Popis	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.
Související projekty:	Verifikace nekonečně stavových systémů Institut Teoretické Informatiky Vysoce paralelní a distribuované výpočetní systémy