The satisfiability problem for temporal logics such as LTL and CTL is well-investigated. These logics possess the finite model property and the complexity of fragments of CTL/CTL* has been fully explored. For probabilistic branching-time logics such as PCTL and PCTL*, that are used to express quantitative properties of Markov chains (MCs) and MDPs, the satisfiability problem is almost unexplored. These logics are quite popular in the field of probabilistic model checking. Model checking of the more expressive probabilistic μ-calculus is decidable too. In contrast, the satisfiability problem for these logics turns out to be a much more difficult endeavour. This is in particular true for quantitative fragments where probabilistic reasoning is required.

Satisfiability for qualitative PCTL—a fragment of PCTL in which all probability bounds are =1 or >0—is decidable and is EXPTIME-complete. Qualitative PCTL and CTL have incomparable expressiveness and the former does (in contrast to CTL) not have the finite model property. The question whether a probabilistic logic admits a rational model, i.e., a Markov model with only rational transition probabilities, plays an important role. PCTL formulas may have only models with irrational probabilities if the model size is bounded. The decision problem whether a PCTL-formula has a rational Markov chain model of a certain size is NP-complete and can be checked using SMT techniques. Initial results on the complexity and finite/rational model property for simple fragments of PCTL and a simple variant of the probabilistic μ-calculus have recently been reported. These logics only contain probabilistically quantified next-modalities and probabilistically quantified bounded until-modalities.

The aim of this dissertation project is to identify richer fragments of PCTL and study their satisfiability, complexity, and finite/rational model property. A promising direction is to start from the characterisation in safety and liveness fragments of this logic. In addition, a systematic study of variants of the probabilistic μ-calculus needs to be carried out. The challenging issue is that there is a plethora of probabilistic variants of the μ-calculus, all with their benefits and deficits. The recently proposed logic μPCTL seems to be at the right balance between expressiveness and decidability. It is planned to investigate several fragments of this logic and to study their satisfiability.