Probabilistic Hyperproperties of Markov Decision Processes

Abstract

Hyperproperties are properties that describe the correctness of a system as a relation between multiple executions. Hyperproperties generalize trace properties and include information-flow security requirements, like noninterference, as well as requirements like symmetry, partial observation, robustness, and fault tolerance. We initiate the study of the specification and verification of hyperproperties of Markov decision processes (MDPs). We introduce the temporal logic PHL (Probabilistic Hyper Logic), which extends classic probabilistic logics with quantification over schedulers and traces. PHL can express a wide range of hyperproperties for probabilistic systems, including both classical applications, such as probabilistic noninterference, and novel applications in areas such as robotics and planning. While the model checking problem for PHL is in general undecidable, we provide methods both for proving and for refuting formulas from a fragment of the logic. The fragment includes many probabilistic hyperproperties of interest.

This work was partially supported by the Collaborative Research Center “Foundations of Perspicuous Software Systems” (TRR 248, 389792660), the European Research Council (ERC) Grant OSARES (No. 683300), the DARPA Assured Autonomy program, the iCyPhy center, and by Berkeley Deep Drive.

1 Introduction

Ten years ago, Clarkson and Schneider coined the term hyperproperties [10] for the class of properties that describe the correctness of a system as a relation between multiple executions. Hyperproperties include information-flow security requirements, like noninterference [17], as well as many other types of system requirements that cannot be expressed as trace properties, including symmetry, partial observation, robustness, and fault tolerance. Over the past decade, a rich set of tools for the specification and verification of hyperproperties have been developed. HyperLTL and ${\textsc {HyperCTL}}^*$ [9] are extensions to LTL and CTL$^*$ that can express a wide range of hyperproperties. There are a number of algorithms and tools for hardware model checking [11, 16], satisfiability checking [15], and reactive synthesis [14] for hyperproperties.

The natural next step is to consider probabilistic systems. Randomization plays a key role in the design of security-critical and distributed systems. In fact, randomization is often added specifically to implement a certain hyperproperty. For example, randomized mutual exclusion protocols use a coin flip to decide which process gets access to the critical resource in order to avoid breaking the symmetry based on the process id [4]. Databases employ privacy mechanisms based on randomizaton in order to guarantee (differential) privacy [13].

Previous work on probabilistic hyperproperties [2] has focussed on the specification and verification of probabilistic hyperproperties for Markov chains. The logic HyperPCTL [2] extends the standard probabilistic logic PCTL with quantification over states. For example, the HyperPCTL formula

specifies that the probability that the system terminates is the same from all initial states. If the initial state encodes some secret, then the property guarantees that this secret is not revealed through the probability of termination.

Because Markov chains lack nondeterministic choice, they are a limited modeling tool. In an open system, the secret would likely be provided by an external environment, whose decisions would need to be represented by nondeterminism. In every step of the computation, such an environment would typically set the values of some low-security and some high-security input variables. In such a case, we would like to specify that the publicly observable behavior of our system does not depend on the infinite sequence of the values of the high-security input variables. Similarly, nondeterminism is needed to model the possible strategic decisions in autonomous systems, such as robots, or the content of the database in a privacy-critical system.

In this paper, we initiate the study of hyperproperties for Markov decision processes (MDPs). To formalize hyperproperties in this setting, we introduce PHL, a general temporal logic for probabilistic hyperproperties. The nondeterministic choices of an MDP are resolved by a scheduler¹; correspondingly, our logic quantifies over schedulers. For example, in the PHL formula

the variables $\sigma$ and $\sigma '$ refer to schedulers. The formula specifies that the probability of termination is the same for all of the possible (infinite) combinations of the nondeterministic choices. If we wish to distinguish different types of inputs, for example those that are provided through a high-security variable h vs. those provided through a low-security variable l, then the quantification can be restricted to those schedulers that make the same low-security choices:

The path quantifier $\forall \pi :\sigma$ works analogously to the quantifiers in ${\textsc {HyperCTL}}^*$, here restricted to the paths of the Markov chain induced by the scheduler assigned to variable $\sigma$. The formula thus states that all schedulers that agree on the low-security inputs induce the same probability of termination.

As we show in the paper, PHL is a very expressive logic, thanks to the combination of scheduler quantifiers, path quantifiers and a probabilistic operator. PHL has both classical applications, such as differential privacy, as well as novel applications in areas such as robotics and planning. For example, we can quantify the interference of the plans of different agents in a multi-agent system, such as the robots in a warehouse, or we can specify the existence of an approximately optimal policy that meets given constraints. A consequence of the generality of the logic is that it is impossible to simply reduce the model checking problem to that of a simpler temporal logic in the style of the reduction of HyperPCTL to PCTL [2]. In fact, we show that the emptiness problem for probabilistic Büchi automata (PBA) can be encoded in PHL, which implies that the model checking problem for PHL is, in general, undecidable.

We present two verification procedures that approximate the model checking problem from two sides. The first algorithm overapproximates the model checking problem by quantifying over a combined monolithic scheduler rather than a tuple of independent schedulers. Combined schedulers have access to more information than individual ones, meaning that the set of allowed schedulers is overapproximated. This means that if a universal formula is true for all combined schedulers it is also true for all tuples of independent schedulers. The second procedure is a bounded model checking algorithm that underapproximates the model checking problem by bounding the number of states of the schedulers. This algorithm is obtained as a combination of a bounded synthesis algorithm for hyperproperties, which generates the schedulers, and a model checking algorithm for Markov chains, which computes the probabilities on the Markov chains induced by the schedulers. Together, the two algorithms thus provide methods both for proving and for refuting a class of probabilistic hyperproperties for MDPs.

Related Work. Probabilistic noninterference originated in information-flow security [18, 21] and is a security policy that requires that the probability of every low trace should be the same for every low equivalent initial state. Volpano and Smith [24] presented a type system for checking probabilistic noninterference of concurrent programs with probabilistic schedulers. Sabelfeld and Sands [23] defined a secure type system for multi-threaded programs with dynamic thread creation which improves on that of Volpano and Smith. None of these works is concerned with models combining probabilistic choice with nondeterminism, nor with general temporal logics for probabilistic hyperproperties.

The specification and verification of probabilistic hyperproperties have recently attracted significant attention. Abraham and Bonakdarpour [2] are the first to study a temporal logic for probabilistic hyperproperties, called HyperPCTL. The logic allows for explicit quantification over the states of a Markov chain, and is capable of expressing information-flow properties like probabilistic noninterference. The authors present a model checking algorithm for verifying HyperPCTL on finite-state Markov chains. HyperPCTL was extended to a logic called HyperPCTL* [25] that allows nesting of temporal and probabilistic operators, and a statistical model checking method for HyperPCTL* was proposed. Our present work, on the other hand is concerned with the specification and model checking of probabilistic hyperproperties for system models featuring both probabilistic choice and nondeterminism, which are beyond the scope of all previous temporal logics for probabilistic hyperproperties. Probabilistic logics with quantification over schedulers have been studied in [6] and [3]. However, these logics do not include quantifiers over paths.

Independently and concurrently to our work, probabilistic hyperproperties for MDPs were also studied in [1] (also presented at ATVA’20). The authors extend HyperPCTL with quantifiers over schedulers, while our new logic PHL extends ${\textsc {HyperCTL}}^*$ with the probabilistic operator and quantifiers over schedulers. Thus, HyperPCTL quantifies over states (i.e., the computation trees that start from the states), while PHL quantifies over paths. Both papers show that the model checking problem is undecidable for the respective logics. The difference is in how the approaches deal with the undecidability result. For both logics, the problem is decidable when quantifiers are restricted to non-probabilistic memoryless schedulers. [1] provides an SMT-based verification procedure for HyperPCTL for this class of schedulers. We consider general memoryful schedulers and present two methods for proving and for refuting formulas from a fragment of PHL.

Due to lack of space we have omitted the proofs of our results and details of the presented model checking procedures, which can be found in [12].

2 Preliminaries

Definition 1

(Markov Decision Process (MDP)). A Markov Decision Process (MDP) is a tuple $M = (S, Act ,\mathbf {P},\iota ,\mathsf {AP},L)$ where S is a finite set of states, $Act$ is a finite set of actions, $\mathbf {P}: S \times Act \times S \rightarrow [0,1]$ is the transition probability function such that $\sum _{s'\in S}\mathbf {P}(s,a,s') \in \{0,1\}$ for every $s \in S$ and $a \in Act$, $\iota : S \rightarrow [0,1]$ is the initial distribution such that $\sum _{s \in S} \iota (s) = 1$, $\mathsf {AP}$ is a finite set of atomic propositions and $L: S \rightarrow 2^{\mathsf {AP}}$ is a labelling function.

A finite path in an MDP $M = (S, Act ,\mathbf {P},\iota ,\mathsf {AP},L)$ is a sequence $s_0s_1\ldots s_n$ where for every $0 \le i < n$ there exists $a_i \in Act$ such that $\mathbf {P}(s_i,a_i,s_{i+1})>0$. Infinite paths in M are defined analogously. We denote with $Paths _ fin (M)$ and $Paths _ inf (M)$ the sets of finite and infinite paths in M. For an infinite path $\rho = s_0s_1\ldots$ and $i \in \mathbb {N}$ we denote with $\rho [i,\infty )$ the infinite suffix $s_i s_{i+1}\ldots$. Given $s \in S$, define $Paths _ fin (M,s) = \{s_0s_1\ldots s_n \in Paths _ fin (M)\mid s_0=s\}$, and similarly $Paths _ inf (M,s)$. We denote with $M_s = (S, Act ,\mathbf {P},\iota _s,\mathsf {AP},L)$ the MDP obtained from M by making s the single initial state, i.e., $\iota _s(s) = 1$ and $\iota _s(t) = 0$ for $t \ne s$.

For a set A we denote with $\mathcal {D}(A)$ the set of probability distributions on A.

Definition 2

(Scheduler). A scheduler for an MDP $M = (S, Act ,\mathbf {P},\iota ,\mathsf {AP},L)$ is a function $\mathfrak {S}: (S\cdot Act )^* S \rightarrow \mathcal {D}( Act )$ such that for all sequences $s_0 a_0 \ldots a_{n-1}s_n \in (S\cdot Act )^* S$ it holds that if $\mathfrak {S}(s_0 a_0 \ldots a_{n-1}s_n)(a) > 0$ then $\sum _{t\in S}\mathbf {P}(s_n,a,t) > 0$, that is, each action in the support of $\mathfrak {S}(s_0 a_0 \ldots a_{n-1}s_n)$ is enabled in $s_n$. We define $Sched (M)$ to be the set consisting of all schedulers for an MDP M.

Given an MDP $M = (S, Act ,\mathbf {P},\iota ,\mathsf {AP},L)$ and a scheduler $\mathfrak {S}$ for M, we denote with $M_{\mathfrak {S}}$ the Markov chain of M induced by $\mathfrak {S}$, which is defined as the tuple $M_{\mathfrak {S}} = ((S\cdot Act )^* S,\mathbf {P}_\mathfrak {S},\iota ,AP,L_\mathfrak {S})$ where for every sequence $h = s_0 a_0 \ldots a_{n-1}s_n \in (S\cdot Act )^* S$ it holds that $\mathbf {P}_\mathfrak {S}(h,h \cdot s_{n+1}) = \sum _{a \in Act }\mathfrak {S}(h)(a)\cdot \mathbf {P}(s_n,a, s_{n+1})$ and $L_\mathfrak {S}(h) = L(s_n)$. Note that $M_{\mathfrak {S}}$ is infinite even when M is finite. The different types of paths in a Markov chain are defined as for MDPs.

Of specific interest are finite-memory schedulers, which are schedulers that can be represented as finite-state machines. Formally, a finite-memory scheduler for M is represented as a tuple $\mathcal {T}_\mathfrak {S}= (Q,\delta ,q_0, act )$, where Q is a finite set of states, representing the memory of the scheduler, $\delta : Q \times S \times Act \rightarrow Q$ is a memory update function, $q_0$ is the initial state of the memory, and $act : Q \times S \rightarrow \mathcal {D}( Act )$ is a function that based on the current memory state and the state of the MDP returns a distribution over actions. Such a representation defines a function $\mathfrak {S}: (S\cdot Act )^* S \rightarrow \mathcal {D}( Act )$ as follows. First, let us define the function $\delta ^* : Q \times (S\cdot Act )^* \rightarrow Q$ as follows: $\delta ^*(q,\epsilon ) = q$ for all $q \in Q$, and $\delta ^*(q,s_0 a_0 \ldots s_na_ns_{n+1}a_{n+1}) = \delta (\delta ^*(q,s_0 a_0 \ldots s_na_n),s_{n+1},a_{n+1})$ for all $q \in Q$ and all $s_0 a_0 \ldots s_na_ns_{n+1}a_{n+1} \in (S\cdot Act )^*$. Now, we define the scheduler function represented by $\mathcal {T}_\mathfrak {S}$ by $\mathfrak {S}(s_0 a_0 \ldots s_na_ns_{n+1}) = act (\delta ^*(s_0 a_0 \ldots s_na_n),s_{n+1})$.

Finite-memory schedulers induce finite Markov chains with simpler representation. A finite memory scheduler $\mathfrak {S}$ represented by $\mathcal {T}_\mathfrak {S}= (Q,\delta ,q_0, act )$ induces the Markov chain $M_{\mathfrak {S}} = (S\times Q,\mathbf {P}_\mathfrak {S},\iota _\mathfrak {S},AP,L_\mathfrak {S})$ where $\mathbf {P}_\mathfrak {S}((s,q),(s',q'))=\sum _{a \in Act } act (q,s)(a)\cdot \mathbf {P}(s,a,s')$ if $q' = \delta (q,s)$, otherwise $\mathbf {P}_\mathfrak {S}((s,q),(s',q'))= 0$, and $\iota _\mathfrak {S}(s,q) = \iota (s)$ if $q = q_0$ and $\iota _\mathfrak {S}(s,q) = 0$ otherwise.

A scheduler $\mathfrak {S}$ is deterministic if for every $h \in (S\cdot Act )^* S$ it holds that $\mathfrak {S}(h)(a) = 1$ for exactly one $a \in Act$. By abuse of notation, a deterministic scheduler can be represented as a function $\mathfrak {S}: S^+ \rightarrow Act$, that maps a finite sequence of states to the single action in the support of the corresponding distribution. Note that for deterministic schedulers we omit the actions from the history as they are uniquely determined by the sequence of states. We write $DetSched (M)$ for the set of deterministic schedulers for the MDP M.

A probability space is a triple $(\varOmega ,\mathcal {F}, Prob )$, where $\varOmega$ is a sample space, $\mathcal {F} \subseteq 2^{\varOmega }$ is a $\sigma$-algebra and $Prob : \mathcal {F} \rightarrow [0,1]$ is a probability measure.

Given a Markov chain $C = (S,\mathbf {P},\iota ,AP,L)$, it is well known how to associate a probability space $(\varOmega ^C,\,\mathcal {F}^C, Prob ^C)$ with C. The sample space $\varOmega ^C = Paths _ inf (C)$ is the set of infinite paths in C, where the sets of finite and infinite paths for a Markov chain are defined in the same way as for MDP. The $\sigma$-algebra $\mathcal {F}^C$ is the smallest $\sigma$-algebra that for each $\pi \in Paths _ fin (C)$ contains the set $Cyl _C(\pi ) = \{\rho \in Paths _ inf (C) \mid \exists \rho ' \in Paths _ inf (C) : \rho = \pi \cdot \rho '\}$ called the cylinder set of the finite path $\pi$. $Prob ^C$ is the unique probability measure such that for each $\pi = s_0\ldots s_n \in Paths _ fin (C)$ it holds that $Prob ^C( Cyl (\pi )) = \iota (s_0) \cdot \prod _{i=0}^{n-1} \mathbf {P}(s_i,s_{i+1})$.

Analogously, given any state $s \in S$ we denote with $(\varOmega ^C,\mathcal {F}^C, Prob ^C_s)$ the probability space for paths in C originating in the state s, i.e., the probability space associated with the Markov chain $C_s$ (where $C_s$ is defined as for MDPs).

When considering a Markov chain $M_\mathfrak {S}$ induced by an MDP M and a scheduler $\mathfrak {S}$, we write $Prob _{M,\mathfrak {S}}$ and $Prob _{M,\mathfrak {S},s}$ for the sake of readability.

3 The Logic PHL

In this section we define the syntax and semantics of PHL, the logic which we introduce and study in this work. PHL allows for quantification over schedulers and integrates features of temporal logics for hyper properties, such as HyperLTL and ${\textsc {HyperCTL}}^*$ [9], and probabilistic temporal logics such as PCTL*.

3.1 Examples of PHL Specifications

We illustrate the expressiveness of PHL with two applications beyond information-flow security, from the domains of robotics and planning.

Example 1

(Action Cause). Consider the question whether a car on a highway that enters the opposite lane (action b) when there is a car approaching from the opposite direction (condition p) increases the probability of an accident (effect e). This can be formalized as the property stating that there exist two deterministic schedulers $\sigma _1$ and $\sigma _2$ such that (i) in $\sigma _1$ the action b is never taken when p is satisfied, (ii) the only differences between $\sigma _1$ and $\sigma _2$ can happen when $\sigma _2$ takes action b when p is satisfied, and (iii) the probability of e being true eventually is higher in the Markov chain induced by $\sigma _2$ than in the one for $\sigma _1$. To express this property in our logic, we will use scheduler quantifiers quantifying over the schedulers for the MDP. To capture the condition on the way the schedulers differ, we will use path quantifiers quantifying over the paths in the Markov chain induced by each scheduler. The atomic propositions in a PHL formula are indexed with path variables when they are interpreted on a given path, and with scheduler variables when they are interpreted in the Markov chain induced by that scheduler. Formally, we can express the property with the PHL formula

where .

The two conjuncts of capture conditions (i) and (ii) above respectively, and formalizes (iii). Here we assume that actions are represented in $\mathsf {AP}$, i.e., $Act \subseteq \mathsf {AP}$    $\square$

Example 2

(Plan Non-interference). Consider two robots in a warehouse, possibly attempting to reach the same location. Our goal is to determine whether all plans for the first robot to move towards the goal are robust against interferences from arbitrary plans of the other robot. That is, we want to check whether for every plan of robot 1 the probability that it reaches the goal under an arbitrary plan of robot 2 is close to that of the same plan for robot 1 executed under any other plan for robot 2. We can express this property in PHL by using quantifiers over schedulers to quantify over the joint deterministic plans of the robots, and using path quantifiers to express the condition that in both joint plans robot 1 behaves the same. Formally, we can express the property with the PHL formula

where $\sigma _1$ and $\sigma _2$ are scheduler variables, $\pi _1$ is a path variable associated with the scheduler for $\sigma _1$, and $\pi _2$ is a path variable associated with the scheduler for $\sigma _2$. The condition states that in both joint plans robot 1 executes the same moves, where the proposition $move1$ corresponds to robot 1 making a move towards the goal. The formula states that the difference in the probability of robot 1 reaching the goal under scheduler $\sigma _1$ and the probability of it reaching the goal under scheduler $\sigma _2$ does not exceed $\varepsilon$.    $\square$

3.2 Syntax

As we are concerned with hyperproperties interpreted over MDPs, our logic allows for quantification over schedulers and quantification over paths.

To this end, let $\mathcal {V}_{sched}$ be a countably infinite set of scheduler variables and let $\mathcal {V}_{path}$ be a countably infinite set of path variables. According to the semantics of our logic, quantification over path variables ranges over the paths in a Markov chain associated with the scheduler represented by a given scheduler variable. To express this dependency we will associate path variables with the corresponding scheduler variable, writing $\pi :\sigma$ for a path variable $\pi$ associated with a scheduler variable $\sigma$. The precise use and meaning of this notation will become clear below, once we define the syntax and semantics of the logic.

Given a set $\mathsf {AP}$ of atomic propositions, PHL formulas over $\mathsf {AP}$ will use atomic propositions indexed with scheduler variables or with path variables. We define the sets of propositions indexed with scheduler variables as $\mathsf {AP}_{\mathcal {V}_{sched}} = \{ a_\sigma \mid a \in \mathsf {AP},\sigma \in \mathcal {V}_{sched}\}$ and with path variables as $\mathsf {AP}_{\mathcal {V}_{path}} = \{ a_\pi \mid a \in \mathsf {AP},\pi \in \mathcal {V}_{path}\}$.

PHL (Probabilistic Hyper Logic) formulas are defined by the grammar

where $\sigma \in \mathcal {V}_{sched}$ is a scheduler variable, $\chi$ is a ${\textsc {HyperCTL}}^*$ formula, $P$ is a probabilistic expression defined below, $\bowtie \, \in \, \{\le ,\le ,\ge ,\ge \}$, and $c \in \mathbb {Q}$.

Formulas in ${\textsc {HyperCTL}}^*$, introduced in [9], are constructed by the grammar

where $\pi$ is a path variable associated with a scheduler variable $\sigma$, and $a\in \mathsf {AP}$.

Probability expressions are defined by the grammar

where $\mathbb {P}$ is the probabilistic operator, $c \in \mathbb {Q}$, and $\varphi$ is an LTL formula [22] defined by the grammar below, where $a \in \mathsf {AP}$ and $\sigma$ is a scheduler variable.

We call formulas of the form $P\bowtie c$ probabilistic predicates.

A PHL formula $\varPhi$ is well-formed if each path quantifier for $\pi :\sigma$ that appears in $\varPhi$ is in the scope of a scheduler quantifier with the scheduler variable $\sigma$.

A PHL formula is closed if all occurrences of scheduler and path variables are bound by scheduler and path quantifiers respectively.

In the following we consider only closed and well-formed PHL formulas.

Discussion. Intuitively, a PHL formula is a Boolean combination of formulas consisting of a scheduler quantifier prefix followed by a formula without scheduler quantifiers constructed from probabilistic predicates and ${\textsc {HyperCTL}}^*$ formulas via propositional operators. Thus, interleaving path quantifiers and probabilistic predicates is not allowed in PHL. This design decision is in line with the fact that probabilistic temporal logics like PCTL$^*$ replace the path quantifiers with the probabilistic operator that can be seen as their quantitative counterpart. We further chose to not allow nesting of probabilistic predicates and temporal operators, as in all the examples that we considered we never encountered the need for nested $\mathbb {P}$ operators. Moreover, allowing arbitrary nesting of probabilistic and temporal operators would immediately make the model checking problem for the resulting logic undecidable, following from the results in [8].

3.3 Self-composition for MDPs

In order to define the semantics of PHL we first introduce the self-composition operation for MDPs, which lifts to MDPs the well-known self-composition of transition systems that is often used in the model checking of hyperproperties.

Let us fix, for the reminder of the section, an MDP $M = (S, Act ,\mathbf {P},\iota ,\mathsf {AP},L)$.

Definition 3

(n-Self-composition of MDP). Let $M = (S, Act ,\mathbf {P},\iota ,\mathsf {AP},L)$ be an MDP and $n \in \mathbb {N}_{>0}$ be a constant. The n-self-composition of M is the MDP $M^n = (S^n, Act ^n,\widehat{\mathbf {P}},\widehat{\iota },\mathsf {AP},\widehat{L})$ with the following components. $S^n = \{(s_1,\ldots ,s_n) \mid s_i \in S \text { for all } 1\le i \le n\}$ is the set of states. $Act ^n = \{(a_1,\ldots ,a_n) \mid a_i \in Act \text { for all } 1\le i \le n\}$ is the set of actions. The transition probability function $\widehat{\mathbf {P}}$ is such that for every $(s_1,\ldots ,s_n),(s_1',\ldots ,s_n')\in S^n$ and $(a_1,\ldots ,a_n) \in Act ^n$ we have $\widehat{\mathbf {P}}((s_1,\ldots ,s_n),(a_1,\ldots ,a_n),(s_1',\ldots ,s_n')) = \prod _{i=1}^n\mathbf {P}(s_i,a_i,s'_i).$ The initial distribution such that $\widehat{\iota }((s_1,\ldots , s_n)) = \iota (s_1)$ if $s_1 = \ldots = s_n = s$ and $\widehat{\iota }((s_1,\ldots , s_n)) = 0$ otherwise. The labelling function $\widehat{L} : S^n \rightarrow (2^\mathsf {AP})^n$ maps states to n-tuples of subsets of $\mathsf {AP}$ (in contrast to Definition 1 where states are mapped to subsets of $\mathsf {AP}$) and is given by $\widehat{L}((s_1,\ldots ,s_n)) = (L(s_1),\ldots ,L(s_n))$.

Naturally, a scheduler $\widehat{\mathfrak {S}} \in Sched (M^n)$ induces a Markov chain $M^n_{\widehat{\mathfrak {S}}}$.

Given schedulers $\mathfrak {S}_1,\ldots ,\mathfrak {S}_n \in Sched (M)$, their composition, a scheduler $\overline{\mathfrak {S}}: (S^n\cdot Act ^n)^* S^n \rightarrow \mathcal {D}( Act ^n)$ for $M^n$, is denoted $\overline{\mathfrak {S}}= \mathfrak {S}_1\parallel \ldots \parallel \mathfrak {S}_n$ and such that for every $\overline{h} = (s_{1,1},\ldots ,s_{1,n})(a_{1,1},\ldots ,a_{1,n})\ldots (s_{k,1},\ldots ,s_{k,n}) \in (S^n\cdot Act ^n)^* S^n$ and $\overline{a} = (a_{k+1,1},\ldots ,a_{k+1,n}) \in Act ^n$, $\overline{\mathfrak {S}}(\overline{h})(\overline{a}) = \prod _{i=1}^n \mathfrak {S}_i(s_{1,i}a_{1,i}\ldots s_{k,i})(a_{k+1,i}).$

3.4 Scheduler and Path Assignments

Let $\mathcal {V}_{sched}$ and $\mathcal {V}_{path}$ be the sets of scheduler and path variables respectively.

A scheduler assignment is a vector of pairs $\varSigma \in \bigcup _{n \in \mathbb {N}}(\mathcal {V}_{sched}\times Sched (M))^n$ that assigns schedulers to some of the scheduler variables. Given a scheduler assignment $\varSigma = ((\sigma _1,\mathfrak {S}_1),\ldots ,(\sigma _n,\mathfrak {S}_n))$, we denote by $|\varSigma |$ the length (number of pairs) of the vector. For a scheduler variable $\sigma \in \mathcal {V}_{sched}$ we define $\varSigma (\sigma ) = \mathfrak {S}_i$ where i is the maximal index such that $\sigma _i = \sigma$. If such an index i does not exits, $\varSigma (\sigma )$ is undefined. For a scheduler assignment $\varSigma = ((\sigma _1,\mathfrak {S}_1),\ldots ,(\sigma _n,\mathfrak {S}_n))$, a scheduler variable $\sigma \in \mathcal {V}_{sched}$, and a scheduler $\mathfrak {S}\in Sched (M)$ we define the scheduler assignment $\varSigma [\sigma \mapsto \mathfrak {S}] = ((\sigma _1,\mathfrak {S}_1),\ldots ,(\sigma _n,\mathfrak {S}_n),(\sigma ,\mathfrak {S}))$ obtained by adding the pair $(\sigma ,\mathfrak {S})$ to the end of the vector $\varSigma$.

Given the MDP M, let $\varSigma = ((\sigma _1,\mathfrak {S}_1),\ldots ,(\sigma _n,\mathfrak {S}_n))$ be a scheduler assignment, and consider $M^{|\varSigma |}$, the $|\varSigma |$-self composition of M. $\varSigma$ defines a scheduler for $M^{|\varSigma |}$, which is the product of the schedulers in $\varSigma$, i.e., $\overline{\mathfrak {S}} = \mathfrak {S}_1 \parallel \ldots \parallel \mathfrak {S}_n$. Let $M_{\varSigma }$ be the Markov chain induced by $\overline{\mathfrak {S}}$. If $\widehat{s}$ is a state in $M_{\varSigma }$, we denote by $M_{\varSigma ,\widehat{s}}$ the Markov chain obtained from $M_{\varSigma }$ by making $\widehat{s}$ the single initial state.

Note that the labeling function $\widehat{L}$ in $M^{|\varSigma |}$ maps the states in $S^{|\varSigma |}$ to $|\varSigma |$-tuples of sets of atomic predicates, that is $\widehat{L}(\widehat{s}) = (L_{1},\ldots ,L_{|\varSigma |})$. Given a scheduler variable $\sigma$ for which $\varSigma (\sigma )$ is defined, we write $\widehat{L}(\widehat{s})(\sigma )$ for the set of atomic predicates $L_i$, where i is the maximal position in $\varSigma$ in which $\sigma$ appears.

We define path assignments similarly to scheduler assignments. A path assignment is a vector of pairs of path variables and paths in $Paths _ inf (M)$. More precisely, a path assignment $\varPi$ is an element of $\bigcup _{m \in \mathbb {N}}(\mathcal {V}_{path}\times Paths _ inf (M))^m$. Analogously to scheduler assignments, for a path variable $\pi$ and a path $\rho \in Paths _ inf (M)$, we define $\varPi (\pi )$ and $\varPi [\pi \mapsto \rho ]$. For $\varPi = ((\pi _1,\rho _1),\ldots ,(\pi _n,\rho _n))$ and $j \in \mathbb {N}$, we define $\varPi [j,\infty ] = ((\pi _1,\rho _1[j,\infty ]),\ldots ,(\pi _n,\rho _n[j,\infty ]))$ to be the path assignment that assigns to each $\pi _i$ the suffix $\rho _i[j,\infty ]$ of the path $\rho _i$.

3.5 Semantics of PHL

We are now ready to define the semantics of PHL formulas. Recall that we consider only closed and well-formed PHL formulas. PHL formulas are interpreted over an MDP and a scheduler assignment. The interpretation of ${\textsc {HyperCTL}}^*$ formulas requires additionally a path assignment. Probabilistic expressions and LTL formulas are evaluated in the Markov chain for an MDP induced by a scheduler assignment. As usual, the satisfaction relations are denoted by $\models$.

For an MDP M and a scheduler assignment $\varSigma$ we define

$$ \begin{array}{lcl} M,\varSigma \,\models \, \forall \sigma . \varPhi &{} \quad \text {iff} &{} \quad \text {for all } \mathfrak {S}\in Sched (M):\; M,\varSigma [\sigma \mapsto \mathfrak {S}] \,\models \, \varPhi ; \\ M,\varSigma \,\models \, \varPhi _1 \wedge \varPhi _2 &{} \quad \text {iff} &{} \quad M,\varSigma \,\models \, \varPhi _1 \text { and } M,\varSigma \,\models \, \varPhi _2; \\ M,\varSigma \,\models \, \lnot \varPhi &{} \quad \text {iff} &{} \quad M,\varSigma \,\not \models \, \varPhi ;\\ M,\varSigma \,\models \, \chi &{} \quad \text {iff} &{} \quad M,\varSigma ,\varPi _\emptyset \,\models \, \chi , \text {where } \varPi _\emptyset \text { is the empty path assignment};\\ M,\varSigma \,\models \, P\bowtie c &{} \quad \text {iff} &{} \quad [\![P]\!]_{{M}_{\varSigma }} \bowtie c. \\ \end{array} $$

For an MDP M, scheduler assignment $\varSigma$, and path assignment $\varPi$ we define

where in the last item C is the Markov chain $M_{\varSigma (\sigma )}$ when $\varPi$ is the empty path assignment, and otherwise the Markov chain $M_{\varSigma (\sigma ),\varPi (\pi ')[0]}$ where $\pi '$ is the path variable associated with scheduler variable $\sigma$ that was most recently added to $\varPi$.

For Markov chain C of the form $M_{\varSigma }$ or $M_{\varSigma ,\widehat{s}}$, where $\varSigma$ is a scheduler assignment and $\widehat{s}$ is a state in $M_\varSigma$ the semantics $[\![\cdot ]\!]_C$ of probabilistic expressions is:

where the semantics of path formulas (i.e., LTL formulas) is defined by

Note that $Prob ^C(\{\rho \in Paths _ inf (C) \mid C,\rho \,\models \, \varphi \})$ is well-defined as it is a known fact [7] that the set $\{\rho \in Paths _ inf (C) \mid C,\rho \,\models \, \varphi \}$ is measurable.

We say that an MDP M satisfies a closed well-formed PHL formula $\varPhi$, denoted $M \,\models \, \varPhi$ iff $M,\varSigma _{\emptyset }\,\models \, \varPhi$, where $\varSigma _{\emptyset }$ is the empty scheduler assignment.

Since PHL includes both scheduler and path quantification, the sets of deterministic and randomized schedulers are not interchangeable with respect to the PHL semantics. That is, there exists an MDP M and formula $\varPhi$ such that if quantifiers are interpreted over $Sched (M)$, then $M \,\models \, \varPhi$, and if quantifiers are interpreted over $DetSched (M)$ then $M \,\not \models \, \varPhi$. See [12] for an example.

3.6 Undecidability of PHL Model Checking

Due to the fact that PHL allows quantification over both schedulers and paths, the model checking problem for PHL is undecidable. The proof is based on a reduction from the emptiness problem for probabilistic Büchi automata (PBA), which is known to be undecidable [5].

Theorem 1

The model checking problem for PHL is undecidable.

We saw in the previous section an example of a probabilistic hyperproperty expressed as a PHL formulas of the form $\forall \sigma _1\ldots \forall \sigma _n.\ \big ((\forall \pi _1:{\sigma _1}\ldots \forall \pi _n:{\sigma _n}. \;\psi ) \rightarrow P\bowtie c\big )$. Analogously to Theorem 1, we can show that the model checking problem for PHL formulas of the form $\exists \sigma _1\ldots \exists \sigma _n.\ (\forall \pi _1:{\sigma _1}\ldots \forall \pi _n:{\sigma _n}.\;\psi \wedge P\bowtie c)$ is undecidable. The undecidability for formulas of the form $\forall \sigma _1\ldots \forall \sigma _n.\ \big ((\forall \pi _1:{\sigma _1}\ldots \forall \pi _n:{\sigma _n}. \;\psi ) \rightarrow P\bowtie c\big )$ then follows by duality. In the next two sections, we present an approximate model checking procedure and a bounded model checking procedure for PHL formulas in these two classes.

However, since there are finitely many deterministic schedulers with a given fixed number of states, the result stated in the next theorem is easily established.

Theorem 2

For any constant $b \in \mathbb {N}$, the model checking problem for PHL restricted to deterministic finite-memory schedulers with b states is decidable.

Fig. 1.

Approximate model checking of PHL formulas of the form (1).

4 Approximate Model Checking

In this section we provide a sound but incomplete procedure for model checking a fragment of PHL. The fragment we consider consists of those PHL formulas that are positive Boolean combinations of formulas of the form

$$\begin{aligned} \varPhi = \forall \sigma _1\ldots \forall \sigma _n.\ \big (\chi \rightarrow c_1 \cdot \mathbb {P}(\varphi _1) + \ldots + c_k \cdot \mathbb {P}(\varphi _k) \bowtie c \big ) \end{aligned}$$

(1)

where $\chi = \forall \pi _1:{\sigma _1}\ldots \forall \pi _n:{\sigma _n}.\;\psi$ and the formula $\psi$ does not contain path quantifiers and describes an n-safety property (i.e., a safety property on $M^n$ [10]). The PHL formula in Example 2 falls into this class.

The formula $\psi$ contains at most one path variable associated with each scheduler variable in $\{\sigma _1,\ldots \sigma _n\}$. This allows us to use the classical self-composition approach to obtain an automaton for $\chi$. Requiring that $\psi$ describes an n-safety property enables us to consider a deterministic safety automaton for $\chi$ which, intuitively, represents the most general scheduler in $M^n$, such that every scheduler that refines it results in a Markov chain in which all paths satisfy $\psi$.

Since for every Markov chain C we have $Prob ^C(\{\pi \in Paths _ inf (C) \mid \pi \,\models \, \varphi \}) = 1 - Prob ^C(\{\pi \in Paths _ inf (C) \mid \pi \,\models \, \lnot \varphi \})$, it suffices to consider the case when $\bowtie$ is $\le$ (or <) and $c_i \ge 0$ for each $i = 1,\ldots ,k$.

We now describe a procedure for checking whether a given MDP $M = (S, Act ,\mathbf {P},\iota ,\mathsf {AP},L)$ satisfies a PHL formula $\varPhi$ of the form (1). If the answer is positive, then we are guaranteed that $M\,\models \, \varPhi$, but otherwise the result is inconclusive. The method, outlined in Fig. 1, proceeds as follows.

We first compute a deterministic safety automaton $\mathcal {D}_\psi$ for the n-hypersafety property $\psi$. The language of $\mathcal {D}_\psi$ is defined over words in $(S^n)^\omega$. It holds that $w \in \mathcal {L}(\mathcal {D}_\psi )$ if and only if for an arbitrary scheduler assignment $\varSigma$ it holds that $M,\varSigma ,\varPi _w \,\models \, \psi$, where $\varPi _w$ is the path assignment corresponding to the word w. As a second step we construct the n-self-composition MDP $M^n$, and then build the product of $M^n$ with the deterministic safety automaton $\mathcal {D}_\psi$. The language of the resulting automaton $\widehat{M}_\chi$ consists of the n-tuples of infinite paths in M such that each such tuple satisfies the n-hypersafety property $\psi$.

After constructing the MDP $\widehat{M}_\chi$, our goal is to check that for every scheduler assignment $\varSigma = ((\sigma _1,\mathfrak {S}_1),\ldots ,(\sigma _n,\mathfrak {S}_n))$ for M such that $\overline{\mathfrak {S}}= \mathfrak {S}_1 \parallel \ldots \parallel \mathfrak {S}_n\in Sched (\widehat{M}_\chi )$ the inequality $\sum _{i=1}^k(c_i \cdot Prob _{\widehat{M}_\chi ,\overline{\mathfrak {S}}}(\varphi _i)) \le c$ is satisfied. That would mean, intuitively, that every scheduler assignment that satisfies $\chi$ also satisfies the above inequality, which is the property stated by $\varPhi$. Note that, if we establish that $\max _{\overline{\mathfrak {S}}= \mathfrak {S}_1 \parallel \ldots \parallel \mathfrak {S}_n} \sum _{i=1}^k(c_i \cdot Prob _{\widehat{M}_\chi ,\overline{\mathfrak {S}}}(\varphi _i))\le c$, then we have established the above property. Computing exactly the value $\max _{\overline{\mathfrak {S}}= \mathfrak {S}_1 \parallel \ldots \parallel \mathfrak {S}_n} \sum _{i=1}^k(c_i \cdot Prob _{\widehat{M}_\chi ,\overline{\mathfrak {S}}}(\varphi _i))$, however, is not algorithmically possible in light of the undecidability results in the previous section. Therefore, we will overapproximate this value by computing a value $c^* \ge \max _{\overline{\mathfrak {S}}= \mathfrak {S}_1 \parallel \ldots \parallel \mathfrak {S}_n} \sum _{i=1}^k(c_i \cdot Prob _{\widehat{M}_\chi ,\overline{\mathfrak {S}}}(\varphi _i))$ and if $c^* \le c$, then we can conclude that the property holds. The value $c^*$ is computed as $c^* = \max _{\widehat{\mathfrak {S}} \in Sched (\widehat{M}_\chi )} \sum _{i=1}^k(c_i \cdot Prob _{\widehat{M}_\chi ,\widehat{\mathfrak {S}}}(\varphi _i))$. For the schedulers $\widehat{\mathfrak {S}}$ considered in this maximization, it is not in general possible to decompose $\widehat{\mathfrak {S}}$ into schedulers $\mathfrak {S}_1,\ldots ,\mathfrak {S}_n \in Sched (M)$. Therefore we have that

$$ \max _{\widehat{\mathfrak {S}} \in Sched (\widehat{M}_\chi )} \sum _{i=1}^k(c_i \cdot Prob _{\widehat{M}_\chi ,\widehat{\mathfrak {S}}}(\varphi _i)) \ge \ \max _{\overline{\mathfrak {S}}= \mathfrak {S}_1 \parallel \ldots \parallel \mathfrak {S}_n} \sum _{i=1}^k(c_i \cdot Prob _{\widehat{M}_\chi ,\overline{\mathfrak {S}}}(\varphi _i)), $$

which implies that $c^*$ has the desired property. We compute $c^*$ as follows.

We construct deterministic Rabin automata $\mathcal {A}_1,\dots ,\mathcal {A}_k$ for the formulas $\varphi _1,\dots ,\varphi _k$. We compute the product $\widetilde{M}$ of the MDP $\widehat{M}_{\chi }$ constructed earlier and $\mathcal {A}_1,\ldots ,\mathcal {A}_k$. Let $\widetilde{S}$ be the set of states of $\widetilde{M}$. We consider each combination of formulas in $\{\varphi _1,\ldots ,\varphi _k\}$, i.e., each subset $I \subseteq \{1,\ldots , k\}$ such that $I \ne \emptyset$. For each I, we take the conjunction of the accepting conditions of the deterministic Rabin automata $\mathcal {A}_i$ for $i \in I$ and apply the methods in [7] to compute the so called success set $U_I\subseteq \widetilde{S}$ for this conjunction. Intuitively, in the states in $U_I$ there exists a scheduler that can enforce the conjunction of the properties in I.

Finally, we solve the linear program that asks to minimize $\sum _{\widetilde{s} \in \widetilde{S}} x_{\widetilde{s}}$ subject to (i) $x_{\widetilde{s}} \ge 0 ~ \text {for all ~} \widetilde{s} \in \widetilde{S}$, (ii) $x_{\widetilde{s}} \ge \sum _{i \in I} c_i \text { for all } I \subseteq \{1,\ldots , k\}\text { and } \widetilde{s} \in U_I$ and (iii) $x_{\widetilde{s}} \ge \sum _{\widetilde{t} \in \widetilde{S}} \mathbf {P}(\widetilde{s},a,\widetilde{t}) \cdot x_{\widetilde{t}} \text { for all } \widetilde{s} \in \widetilde{S} \text { and } a \in Act ^n.$ If $(x_{\widetilde{s}}^*)_{s\in \widetilde{S}}$ is the optimal solution of the linear program, let $c^* = \sum _{\widetilde{s} \in \widetilde{S}} \widetilde{\iota }(\widetilde{s}) \cdot x_{\widetilde{s}}^*.$

If $c^* \le c$, then for all tuples of schedulers $\mathfrak {S}_1,\ldots ,\mathfrak {S}_n$ we have that if $M_{\mathfrak {S}_1 \parallel \ldots \parallel \mathfrak {S}_n} \,\models \,\chi$, then for their product $\overline{\mathfrak {S}}= \mathfrak {S}_1 \parallel \ldots \parallel \mathfrak {S}_n$ it holds that $\sum _{i=1}^k (c_i \cdot Prob _{M^n,\overline{\mathfrak {S}}}(\varphi _i))\le c$, and we conclude that $M \,\models \, \varPhi$. If, on the other hand, we have $c^* > c$, then the result is inconclusive. When this is the case, we can use bounded model checking to search for counterexamples to formulas of the form (1). For the procedure above, we establish the following result.

Theorem 3

(Complexity). Given an MDP $M = (S, Act ,\mathbf {P},\iota ,\mathsf {AP},L)$ and a PHL formula $\varPhi$ of the form (1) the model checking procedure above runs in time polynomial in the size of M and doubly exponential in the size of $\varPhi$.

Fig. 2.

Bounded model checking of MDPs against PHL formulas for the form (2).

5 Bounded Model Checking

We present a bounded model-checking procedure for PHL formulas of the form

$$\begin{aligned} \varPhi = \exists \sigma _1\ldots \exists \sigma _n.\ \big (\chi \wedge c_1 \cdot \mathbb {P}(\varphi _1) + \ldots + c_k \cdot \mathbb {P}(\varphi _k) \bowtie c \big ) \end{aligned}$$

(2)

where $\chi = \forall \pi _1:{\sigma _1}\ldots \forall \pi _n:{\sigma _n}.\;\psi$ is in the $\forall ^*$ fragment of HyperLTL [14]. An example of a formula in this fragment is the formula in Example 1. By finding a scheduler assignment that is a witness for a PHL formula of the form (2) we can find counterexamples to PHL formulas of the form (1).

Given an MDP $M = (S, Act ,\mathbf {P},\iota ,\mathsf {AP},L)$, a bound $b \in \mathbb {N}$, and a PHL formula $\varPhi = \exists \sigma _1\ldots \exists \sigma _n.\ \big (\chi \,\wedge \, c_1 \cdot \mathbb {P}(\varphi _1)\, + \ldots + \,c_k \cdot \mathbb {P}(\varphi _k)\, \bowtie \, c\big )$, the bounded model checking problem for M, b and $\varPhi$ is to determine whether there exists a deterministic finite-memory scheduler $\widetilde{\mathfrak {S}} = \mathfrak {S}_1||\dots ||\mathfrak {S}_n$ for $M^n$ composed of deterministic finite-memory schedulers $\mathfrak {S}_i = ( Q^i, \delta ^i, q^i_0, act _i)$ for M for $i\in \{1,\dots ,n\}$, with $|\mathfrak {S}| = b$ such that $M^n_{\widetilde{\mathfrak {S}}} \,\models \, \chi \,\wedge \, \sum _{i=1}^k (c_i \cdot \mathbb {P}(\varphi _i)) \,\bowtie \, c$.

Our bounded model checking procedure employs bounded synthesis for the logic HyperLTL [14] and model checking of Markov chains [19]. The flow of our procedure is depicted in Fig. 2. The procedure starts by checking whether there is a scheduler $\widetilde{\mathfrak {S}}$ for $M^n$ composed of schedulers $\mathfrak {S}_1,\dots , \mathfrak {S}_n$ for M that satisfies the constraint given by the hyperproperty $\chi$. This is done by synthesizing a scheduler of size b for the HyperLTL formula $\varphi _M^{\chi }$ composed of the formula $\chi$, an encoding of M, which ensures that the schedulers $\mathfrak {S}_1,\dots , \mathfrak {S}_n$ defining $\widetilde{\mathfrak {S}}$ follow the structure of M, and an additional consistency constraint that requires $\widetilde{\mathfrak {S}}$ to be a composition of n schedulers $\mathfrak {S}_1,\dots , \mathfrak {S}_n$ for M.

If $\varphi _M^\chi$ is realizable, then the procedure proceeds by applying the synthesized scheduler $\widetilde{\mathfrak {S}}$ to the n-self-composition of the MDP M, which results in a Markov chain $\widetilde{C}= M^n_{\widetilde{\mathfrak {S}}}$. To check whether the synthesized scheduler also satisfies the probabilistic constraint $P\bowtie c$, we apply a probabilistic model checker to the Markov chain $\widetilde{C}$ to compute for each $\varphi _i$ the probability $Prob _{\widetilde{C}}(\varphi _i)$, and then we evaluate the probabilistic predicate $P \bowtie c$. If $\widetilde{C}$ satisfies $P \bowtie c$, then $M^n_{\widetilde{\mathfrak {S}}} \,\models \, \chi \wedge \sum _{i=1}^k (c_i \cdot \mathbb {P}(\varphi _i)) \bowtie c$, implying that $M\,\models \,\varPhi$. If not, we return back to the synthesizer to construct a new scheduler. In order to exclude the scheduler $\widetilde{\mathfrak {S}}$ from the subsequent search, a new constraint $\overline{\varphi }_{\widetilde{\mathfrak {S}}}$ is added to $\varphi _M^\chi$. The formula $\varphi _{\widetilde{\mathfrak {S}}}$ imposes the requirement that the synthesized scheduler should be different from $\widetilde{\mathfrak {S}}$. This process is iterated until a scheduler that is a witness for $\varPhi$ is found, or all schedulers within the given bound b have been checked. The complexity of the procedure is given in the next theorem and follows from complexity of probabilistic model checking [19] and that of synthesis for HyperLTL [14].

Theorem 4

(Complexity). Given an MDP $M = (S, Act ,\mathbf {P},\iota ,\mathsf {AP},L)$, a bound $b \in \mathbb {N}$, and a PHL formula $\varPhi = \exists \sigma _1\ldots \exists \sigma _n. \chi ~\wedge ~ c_1 \cdot \mathbb {P}(\varphi _1) \,+ \ldots + \,c_k \cdot \mathbb {P}(\varphi _k) \bowtie c$, the bounded model checking problem for M, b and $\varPhi$ can be solved in time polynomial in the size of M, exponential in b, and exponential in the size of $\varPhi$.

5.1 Evaluation

Table 1. Experimental results from model checking plan non-interference.

We developed a proof-of-concept implementation of the approach in Fig. 2. We used the tool BoSyHyper [14] for the scheduler synthesis and the tool PRISM [20] to model check the Markov chains resulting from applying the synthesized scheduler to the self-composition of the input MDP. For our experiments, we used a machine with 3.3 GHz dual-core Intel Core i5 and 16 GB of memory.

Table 1 shows the results of model checking the “plan non-interference” specification introduced in Sect. 3.1 against MDP’s representing two robots that try to reach a designated cell on grid arenas of different sizes ranging from 3-grid to a 9-grid arena. In the last instance, we increased the number of robots to three to raise the number of possible schedulers. The specification thus checks whether the probability for a robot to reach the designated area changes with the movements the other robots in the arena. In the initial state, every robot is positioned on a different end of the grid, i.e., the farthest point from the designated cell.

Table 2. Detailed experimental results for the 3-Robots Arena 4 benchmark.

In all instances in Table 1, the specification with $\varepsilon = 0.25$ is violated. We give the number of iterations, i.e., the number of schedulers synthesized, until a counterexample was found. The synthesis and model checking time represent the total time for synthesizing and model checking all schedulers. Table 1 shows the feasibility of approach, however, it also demonstrates the inherent difficulty of the synthesis problem for hyperproperties.

Table 2 shows that the time needed for the overall model checking approach is dominated by the time needed for synthesis: The time for synthesizing a scheduler quickly increases in the last iterations, while the time for model checking the resulting Markov chains remains stable for each scheduler. Despite recent advances on the synthesis from hyperproperties [14], synthesis tools for hyperproperties are still in their infancy. PHL model checking will directly profit from future progress on this problem.

6 Conclusion

We presented a new logic, called PHL, for the specification of probabilistic temporal hyperproperties. The novel and distinguishing feature of our logic is the combination of quantification over both schedulers and paths, and a probabilistic operator. This makes PHL uniquely capable of specifying hyperproperties of MDPs. PHL is capable of expressing interesting properties both from the realm of security and from the planning and synthesis domains. While, unfortunately, the expressiveness of PHL comes at a price as the model checking problem for PHL is undecidable, we show how to approximate the model checking problem from two sides by providing sound but incomplete procedures for proving and for refuting universally quantified PHL formulas. We developed a proof-of-concept implementation of the refutation procedure and demonstrated its principle feasibility on an example from planning.

We believe that this work opens up a line of research on the verification of MDPs against probabilistic hyperproperties. One direction of future work is identifying fragments of the logic or classes of models that are practically amenable to verification. Furthermore, investigating the connections between PHL and simulation notions for MDPs, as well studying the different synthesis questions expressible in PHL are both interesting avenues for future work.