User: Guest  Login
Original title:
Verification of Discrete-Time Markov Decision Processes 
Translated title:
Verifikation von Markov Entscheidungsprozessen in Diskreter Zeit 
Year:
2021 
Document type:
Dissertation 
Institution:
Fakultät für Informatik 
Advisor:
Křetínský, Jan (Prof. Dr.) 
Referee:
Křetínský, Jan (Prof. Dr.); Baier, Christel (Prof. Dr.) 
Language:
en 
Subject group:
DAT Datenverarbeitung, Informatik 
Keywords:
Verification, Markov Decision Process 
Translated keywords:
Verifikation, Markov Entscheidungsprozess 
TUM classification:
DAT 500 
Abstract:
In this thesis, we discuss the verification of discrete-time Markov decision processes (MDP). First, we present two novel algorithms to efficiently compute mean-payoff queries on MDP. Then, we provide efficient practical implementations of LTL-to-automata translation algorithms, which play a central role in probabilistic LTL model checking. We introduce the novel notion of cores in an MDP, which provide a framework to speed up many approximation-based tasks by automatically removing irrelevant s...    »
 
Translated abstract:
Diese Arbeit beschäftigt sich mit der Verifikation von Markov Entscheidungsprozessen in diskreter Zeit. Wir definieren zwei neue Algorithmen um mean-payoff Probleme effizient zu lösen. Dann geben wir eine Überblick über eine effiziente Implementierung von LTL-zu-Automaten Übersetzungsalgorithmen, welche insbesondere im Kontext der probabilistischen Verifikation von LTL Formeln eine zentrale Rolle spielen. Danach beschreiben wir das neue Konzept eines Kerns, welches uns erlaubt automatisch unwich...    »
 
Oral examination:
26.02.2021 
File size:
3471158 bytes 
Pages:
170 
Last change:
26.07.2021