Quantitative Probabilistic Fixed Point Logic and the Problem of Satisfiability

Abstract

The analysis of time-dependent systems in a probabilistic setting has greatly benefited from the application of temporal logic. This thesis focuses on a specific probabilistic modal fixed point logic setup, which offers a higher level of expressiveness compared to conventional probabilistic logics by incorporating quantitative semantics. Additionally, the logic has the capability of encoding proba- bilistic computation tree logic, one of the most widely used logics in probabilistic model checking. The decidability of the satisfiability problem for this logic however, remains a significant open prob- lem. In this thesis we propose a tableau system for the quantitative probabilistic fixed point logic that is intended to characterise satisfiability. Drawing inspiration from related work, the tableau con- struction we propose has novel rules that syntactically capture the quantitive aspect of the logic. Our objective is to demonstrate that the proposed structure is suitable for further exploration while offering a deeper understanding of the complexity associated with solving the satisfiability problem for this logic.