Diplomová práce
Získaná ocenění: Cena děkana FI za vynikající závěrečnou práci

Problém splnitelnosti pro pravděpodobnostní temporální logiky

The satisfiability problem for probabilistic temporal logics

Bc. Miroslav Chodil
Anotace

Táto práca sa zaoberá problémom splnitelnosti pre pravdepodobnostnú logiku PCTL. PCTL je populárny formalizmus pre špecifikáciu vlastností stochastických systémov. Problém splnitelnosti pre PCTL je dlhodobo otvorený problém zaujímavý z teoretickej stránky, jeho riešenie by ale malo aj praktické využitie, ako napríklad overovanie konzistencie špecifikácií. Najprv práca podáva prehľad známych výsledkov …více

Abstract

In this thesis, we study the satisfiability problem for PCTL. PCTL is a popular formalism for specifying properties of stochastic systems. The satisfiability problem for PCTL is a longstanding open problem interesting from a theoretical perspective, although its solution would also have various practical applications, such as consistency checking for specifications. We give an overview of known results …více

Klíčová slova
pctl probabilistic ctl satisfiability probabilistic temporal logics
Zadání práce

Standardní temporální logiky větvícího se času umožňují kvantifikovat formule cest pomocí existenčního a univerzálního kvantifikátoru. Pravděpodobnostní varianty těchto logik pak nahrazují uvedené kvantifikátory pravděpodobnostním operátorem, s jehož pomocí lze explicitně omezit pravděpodobnost cest splňujících danou formuli. Pravděpodobnostní temporální logiky představují základní specifikační jazyk pro vlastnosti stochastických systémů.

Základním tématem práce je rozhodnutelnost a výpočetní složitost problému splnitelnosti pro pravděpodobnostní logiku PCTL a její fragmenty. Rozhodnutelnost problému splnitelnosti pro PCTL je dlouhodobě otevřený problém, existují však pozitivní výsledky pro některé fragmenty PCTL. Řešení je dále komplikováno tím, že PCTL nemá (na rozdíl od CTL) vlastnost malého modelu, a některé PCTL formule mají pouze nekonečný model. Cílem práce je podat úplný přehled a kvalifikované srovnání stávajících výsledků a důkazových technik, v ideálním případě pak přispět původními vědeckými výsledky v této oblasti.

Administrativní informace
Práce zkontrolována:
21. 5. 2019 10:49, prof. RNDr. Antonín Kučera, Ph.D., učo 2508
Plný text práce
607,2 KB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
20. 6. 2019
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Antonín Kučera, Ph.D., učo 2508
KTP FI MU

Oponent

doc. RNDr. Tomáš Brázdil, Ph.D., MBA, učo 4074
KSUZD FI MU
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

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