Thesis Details
Advanced Methods for Synthesis of Probabilistic Programs
Probabilistic programs play a crucial role in various engineering domains, including computer networks, embedded systems, power management policies, or software product lines. PAYNT is a tool for the automatic synthesis of probabilistic programs satisfying the given specifications. In this thesis, we extend this tool primarily to support optimal synthesis and synthesis for multi-property specifications. Further, we have proposed and implemented a new method that can efficiently synthesise continuous parameters affecting the transition probabilities alongside the synthesis of a program topology, i.e., support of both topology and parameter synthesis at the same time. We demonstrate the usefulness and performance of PAYNT on a wide range of real-world case studies from various application domains. For challenging synthesis problems, PAYNT can significantly decrease the run-time from days to minutes while ensuring the completeness of the synthesis process.
automated synthesis, probabilistic programs, Markov models, model checking
Češka Milan, doc. RNDr., Ph.D. (DITS FIT BUT), člen
Drábek Vladimír, doc. Ing., CSc. (DCSY FIT BUT), člen
Peringer Petr, Dr. Ing. (DITS FIT BUT), člen
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT), člen
Smrčka Aleš, Ing., Ph.D. (DITS FIT BUT), člen
@mastersthesis{FITMT24077, author = "\v{S}imon Stupinsk\'{y}", type = "Master's thesis", title = "Advanced Methods for Synthesis of Probabilistic Programs", school = "Brno University of Technology, Faculty of Information Technology", year = 2021, location = "Brno, CZ", language = "english", url = "https://www.fit.vut.cz/study/thesis/24077/" }