Název: Generování protipříkladů při analýze Markovových modelů
Překlad názvu: Counter-Example Generation in the Analysis of Markov Models
Autoři: Molek, Martin ; Matyáš, Jiří (oponent) ; Češka, Milan (vedoucí práce)
Typ dokumentu: Bakalářské práce
Rok: 2018
Jazyk: cze
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [cze] [eng]
Tato práce se zabývá generováním protipříkladů v kontextu verifikace pravděpodobnostních systémů. Protipříklady jsou generovány nad Markovovými modely (přesněji DTMC). Specifikace vlastností modelu jsou zadávány pomocí logiky PCTL, která je v této práci popsána. Pro generování protipříkladů byly použity dva různé algoritmy (Best-first search a Recursive Enumration Algorithm). Práce obsahuje popis implementace algoritmů do verifikačního nástroje STORM. Výsledky experimentů ukazují, že REA je schopen pracovat s modely obsahující miliony stavů. This thesis deals with generating counterexamples in context of probabilistic models. Counterexamples are generated for Markov models (specifically DTMC). Definitions of model properties are given by logic PCTL. Two algorithms (Best-first search and Recursive Enumration Algorithm) are used to generate these counterexamples. Thesis describes implementation of algorithms into verification tool STORM. The results of experiments show that REA is capable of handling models containg millions of states.
Klíčová slova: DTMC; formální verifikace; k-nejkratších cest; Markovovy modely; pravděpodobnostní modely; pravděpodobnostní temporální logika; protipříklady; STORM; counterexamples; DTMC; formal verification; k-shortest paths; Markov chains; Probabilistic Computation Tree Logic; probabilistic models; STORM

Instituce: Vysoké učení technické v Brně (web)
Informace o dostupnosti dokumentu: Plný text je dostupný v Digitální knihovně VUT.
Původní záznam: http://hdl.handle.net/11012/85148

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-386165


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Vysoké učení technické v Brně
Vysokoškolské kvalifikační práce > Bakalářské práce