Original title:
Generování protipříkladů při analýze Markovových modelů
Translated title:
Counter-Example Generation in the Analysis of Markov Models
Authors:
Molek, Martin ; Matyáš, Jiří (referee) ; Češka, Milan (advisor) Document type: Bachelor's theses
Year:
2018
Language:
cze Publisher:
Vysoké učení technické v Brně. Fakulta informačních technologií Abstract:
[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.
Keywords:
counterexamples; DTMC; formal verification; k-shortest paths; Markov chains; Probabilistic Computation Tree Logic; probabilistic models; STORM; DTMC; formální verifikace; k-nejkratších cest; Markovovy modely; pravděpodobnostní modely; pravděpodobnostní temporální logika; protipříklady; STORM
Institution: Brno University of Technology
(web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library. Original record: http://hdl.handle.net/11012/85148