Probabilistic hyperlogics: extensions and efficient model checking

RWTH Publications (RWTH Aachen)

Abstract

Markov decision processes (MDPs) allow to model processes with both nondeterministic choices and randomness. Traditional verification tasks for MDPs are concerned with probabilities in a single execution of an MDP from a given state; the question is usually either whether some property holds for all schedulers or whether there exists some scheduler satisfying the desired property. In contrast, probabilistic hyperproperties allow to relate several executions of an MDP. This increased expressivity leads to an increased model-checking complexity: While model checking for temporal logics like PCTL is decidable, model checking for probabilistic hyperlogics like HyperPCTL or PHL is undecidable for schedulers with unbounded memory. This thesis studies model checking for probabilistic hyperproperties in two dimensions. Firstly, we explore the boundaries between tractability, decidability and undecidability for the HyperPCTL model-checking problem. To this end, we study the complexity of the HyperPCTL model-checking problem both for schedulers with bounded memory and for schedulers with unbounded memory, as well as a tractable class of probabilistic hyperproperties called relational properties. Secondly, we study formalisms for probabilistic hyperproperties going beyond (1) a lockstep evaluation of the considered executions and (2) single-player systems. More specifically, we propose (1) an asynchronous extension of HyperPCTL and (2) a probabilistic hyperlogic for strategies in turn-based stochastic games. For both logics, we investigate the complexity of the respective model-checking problems and propose model-checking algorithms for decidable fragments.

Authors 1

1. Carolina Gerlach corresponding Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen