Characteristic Patterns for LTL

• 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
• 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