Abstract:
In many systems, we have to deal with randomness. In case of communication between two computers for example, there may be a certain positive probability that a message is lost every time one is sent. To verify such systems we need to model these probabilities as well. Often, this is done using the Markov Decision Process (MDP), which models decision making under uncertainty. Furthermore, timing often plays an important role in lots of systems. The communication between two computers may time out if a message is not received after a certain amount of time. Therefore, the Probabilistic Timed Automaton has been introduced, which extends the MDP by adding clocks. We can already check if some MDP or PTA satisfies a certain specification, but for the MDP it is also possible to find probability distributions such that the specification is satisfied. This is called Parameter Synthesis. This raises the question whether this is also possible for the PTA.
In this talk, I, Bram Kohlen, will tell a little bit about myself as I only recently joined the team. I will then proceed to talk about my Master's Thesis, which was about Parameter Synthesis in PTAs. Last of all, I will introduce the main task during my PhD, which is the verification of the underlying algorithms to do this probabilistic verification, for which Isabelle/HOL will be used. In other words, it's about verifying the verifiers. We can then use Isabelle's Code Generator to generate algorithms that care correct by construction. Since the topic is quite theoretical, I aimed to visualize as much as possible and I decided skim over the parts that don't allow for good visualizations. So those who are having vacation should not feel disheartened to join if you are thinking about doing so, I have thought about you.
