Bakalářská práce

Výpočet charakteristických vzorců pro LTL

Computation of characteristic patterns for LTL

Tomáš Babiak, učo 143254
Anotace

Táto bakalárska práca sa zaoberá implementcáciu výpočtu charakteristických vzorcov pre LTL formule.

Abstract

This bachelor's thesis occupies at the implemantation of computation of characteristic patterns for LTL formula.

Klíčová slova
Model-checking lineárna temporálna logika (LTL) nekonečné slová charakteristické vzorce pre LTL
Zadání práce

Cílem práce je navrhnout a implementovat algoritmus pro výpočet charakteristických vzorců k zadané formuli Lineární temporální logiky (LTL). Tyto charakteristické vzorce odpovídají vzájemně se vylučujícím LTL formulím, jejichž disjunkce je ekvivalentní původní formuli. Naivní algoritmus pro výpočet vzorců byl naznačen v článku A. Kučera, J. Strejček: Characteristic patterns for LTL, kde je prezentována teorie charakteristických vzorců pro LTL.

Algoritmus může být přímočaře využit při vývoji nové paralelní a distribuované metody pro LTL model checking. Implementace zmíněné metody však již není součástí této bakalářské práce.

Administrativní informace
Práce zkontrolována:
11. 10. 2008 12:56, (IS automaticky)
Plný text práce
3,6 MB / soubor PDF
Jazyk práce
slovenština slovenština
Termín obhajoby
18. 6. 2007
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Jan Strejček, Ph.D., učo 3366
KTP FI MU

Oponent

Autor posudku dosud neidentifikován.

Literatura

  • 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.
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Aplikovaná informatika
Obor

Práce na příbuzné téma

Seznam prací, které mají shodná klíčová slova.

  • Přidání souboru

    Soubor nebo složku lze nahrát pomocí tlačítka Přidat.

  • Další operace se soubory

    Podrobnosti lze zjistit označením příslušného řádku.

  • Pohled pro experty

    Pro častou práci je možné zvolit režim Více možností.

  • Vyhledávání souborů

    Vyhledávaný výraz můžete zadat přímo do adresního řádku.

  • Rychlý přístup k souborům

    Pomocí funkce Nedávné je možné se rychle vrátit k právě prohlíženým souborům. Oblíbené soubory je také možné označit Hvězdičkou.