Diplomová práce

Model Checking of promt-LTL properties

Bc. Ondřej Kuzník, učo 139894
Anotace

Logika LTL si, od chvíle, kdy byl poprvé publikován algoritmus pro její model-checking, získala mnoho uživatelů pro svou kombinaci množství popsatelných vlastností a jednoduchosti jejich popisu. Lidé jsou nicméně občas zlákáni v myšlenku, že splnění vlastnosti typu "živost" implikuje i "včasnost", že je délka čekání i nějak omezena. Pro tento účel rozšířili Vardi a kol. tuto logiku o operátor omezené …více

Abstract

Over the years since model checking has been introduced, LTL has gained a respectable position for striking a good compromise between simplicity and expressiveness. However, people often find themselves misled into thinking that satisfaction of a liveness property implies a bound on the wait time, promptness. For this very reason Vardi et al. proposed an extension of LTL, adding a prompt-future operator …více

Klíčová slova
model checking Prompt-LTL LTL tableau Buchi automata promptness liveness
Zadání práce
Cílem diplomové práce je prozkoumat možnosti ověřování LTL vlastností konečně-stavového modelu a to konkrétně z pohledu splnitelnosti vlastností v budoucnu. Dostupné algoritmy umožňují rozhodnout platnost LTL formule z pohledu omezené budoucnosti, tzv. prompt-LTL vlastností. Tyto algoritmy ale neumožňují efektivní hledání nejmenší hranice, pro kterou je formule splněná. Diplomová práce má analyzovat možnost hledání nejmenší hranice pomocí metody tabla a prozkoumat, zda metoda umožňuje efektivnější a přesnější určení nejmenší hranice než metoda založena na Buchiho automatech.
Administrativní informace
Práce zkontrolována:
27. 5. 2009 17:17, prof. RNDr. Ivana Černá, CSc., učo 1419
Plný text práce
314,1 KB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
29. 6. 2009
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Ivana Černá, CSc., učo 1419
KTP FI MU

Oponent

RNDr. Nikola Beneš, Ph.D., učo 72525
KPSK FI MU

Literatura

  • VARDI, Moshe; Orna KUPFERMAN a Nir PITERMAN. From Liveness to Promptness. In Lecture Notes in Computer Science Volume 4590. Springer Verlag, 2007.
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Informatika
Obor

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

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

Podobné práce
 
Název
Vložil
Vloženo
Práva
Archiv závěrečné práce Ondřej Kuzník FI N-IN IN, učo 139894 fpfgf/6
Kuzník, O.
24. 5. 2009
Složky
Soubory
Anotace anglicky annotation_english.txt
Kuzník, O.
24. 5. 2009
Anotace česky annotation.txt
Kuzník, O.
24. 5. 2009
Klíčová slova keywords.txt
Kuzník, O.
24. 5. 2009
Posudek oponenta posudek_oponenta.pdf
Beneš, N.
24. 6. 2009
thesis.pdf
Kuzník, O.
24. 5. 2009

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