Thesis Details

Computer-Aided Synthesis of Probabilistic Models

Master's Thesis Student: Andriushchenko Roman Academic Year: 2019/2020 Supervisor: Češka Milan, doc. RNDr., Ph.D.
Czech title
Computer-Aided Synthesis of Probabilistic Models
Language
English
Abstract

This thesis considers the problem of automated synthesis of probabilistic systems: having a family of Markov chains, how can one efficiently identify a chain satisfying a given specification? Such families often arise in various domains of engineering when modeling systems under uncertainty, and deciding even the simplest problems shows to be NP-hard. To tackle this problem, we adopt the principles of counterexample-guided inductive synthesis (CEGIS) and abstraction refinement (CEGAR) and develop a novel integrated technique for probabilistic synthesis. Experiments on practically relevant case studies demonstrate that the designed technique is not only comparable to state-of-the-art synthesis approaches, in most cases it manages to significantly outperform existing methods, sometimes by a margin of orders of magnitude.

Keywords

Markov models, probabilistic model checking, synthesis of probabilistic models

Department
Degree Programme
Information Technology, Field of Study Mathematical Methods in Information Technology
Files
Status
defended, grade A
Date
17 July 2020
Reviewer
Committee
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT), předseda
Grégr Matěj, Ing., Ph.D. (DIFS FIT BUT), člen
Hrubý Martin, Ing., Ph.D. (DITS FIT BUT), člen
Kekely Lukáš, Ing., Ph.D. (DCSY FIT BUT), člen
Kořenek Jan, doc. Ing., Ph.D. (DCSY FIT BUT), člen
Ryšavý Ondřej, doc. Ing., Ph.D. (DIFS FIT BUT), člen
Citation
ANDRIUSHCHENKO, Roman. Computer-Aided Synthesis of Probabilistic Models. Brno, 2020. Master's Thesis. Brno University of Technology, Faculty of Information Technology. 2020-07-17. Supervised by Češka Milan. Available from: https://www.fit.vut.cz/study/thesis/22997/
BibTeX
@mastersthesis{FITMT22997,
    author = "Roman Andriushchenko",
    type = "Master's thesis",
    title = "Computer-Aided Synthesis of Probabilistic Models",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2020,
    location = "Brno, CZ",
    language = "english",
    url = "https://www.fit.vut.cz/study/thesis/22997/"
}
Back to top