HyperQPTL and HyperQPTL + are expressive specification languages for hyperproperties, properties that relate multiple executions of a system. Tight complexity bounds are known for HyperQPTL finite-state satisfiability and model-checking. Here, we settle the complexity of satisfiability for HyperQPTL as well as satisfiability, finite-state satisfiability, and model-checking for HyperQPTL + : the former is Σ 1 2 -complete, the latter are all equivalent to truth in third-order arithmetic, i.e., all four are very undecidable.

We robustify PCTL and PCTL⁎, the most important specification languages for probabilistic systems, and show that robustness does not increase the complexity of their model-checking problems.