The Satisfiability Problem for Fragments of PCTL

VCLA hosting a talk by Alexej Rotar

ABSTRACT

The satisfiability of PCTL-formulae in general is a long standing open problem. Variations of the problem, such as the satisfiability of qualitative PCTL-formulae (Brázdil, Forejt, Kˇretínsk ` y, and Kucera, 2008), the bounded satisfiability (Bertrand, Fearnley, and Schewe, 2012), or the satisfiability for bounded PCTL-formulae (Chakraborty and Katoen, 2016) have been solved already. In this thesis, we tackle the satisfiability problem for various fragments of the quantitative PCTL. For this, we develop several techniques to reduce the size and complexity of models in order to obtain models of regular shape. Thereby, we show the small model property of the considered fragments. In particular, we prove that for those fragments, the general satisfiability problem and the finite satisfiability problem are equivalent. We also provide examples of obstacles for more general fragments. Besides the solutions presented in this thesis, the methods that we develop may serve as a framework to solve other fragments, as they are applicable to more general formulae.

This talk is a presentation of a master thesis, for which Alexej Rotar received the VCLA International Student Awards for Outstanding Undergraduate Thesis in 2019. More here

Magdalena Ortiz, Kurt Matyas (Vice-Rector for Academic Affairs), Alexej Rotar, Gerti Kappel.