{'fraction_non_alphanumeric': 0.042767140210006174, 'fraction_numerical': 0.008004941321803582, 'mean_word_length': 4.209936928819668, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 5, 'https://': 1, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 8, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Probabilistic Hyperproperties with Nondeterminism

We study the problem of formalizing and checking probabilistic hyperproperties for models that allow nondeterminism in actions. We extend the temporal logic HyperPCTL, which has been previously introduced for discrete-time Markov chains, to enable the specification of hyperproperties also for Markov decision processes. We generalize HyperPCTL by allowing explicit and simultaneous quantification over schedulers and probabilistic computation trees and show that it can express important quantitative requirements in security and privacy. We show that HyperPCTL model checking over MDPs is in general undecidable for quantification over probabilistic schedulers with memory, but restricting the domain to memoryless non-probabilistic schedulers turns the model checking problem NP-complete. Subsequently, we propose an SMT-based encoding for model checking this language and evaluate its performance.


Introduction
Hyperproperties [1] extend the conventional notion of trace properties [2] from a set of traces to a set of sets of traces. In other words, a hyperproperty stipulates a system property and not the property of just individual traces. It has been shown that many interesting requirements in computing systems are hyperproperties and cannot be expressed by trace properties. Examples include (1) a wide range of information-flow security policies such as noninterference [3] and observational determinism [4], (2) sensitivity and robustness requirements in cyber-physical systems [5], and consistency conditions such as linearizability in concurrent data structures [6]. Hyperproperties can describe the requirements of probabilistic systems as well. They generally express probabilistic relations between multiple executions of a system. For example, in informationflow security, adding probabilities is motivated by establishing a connection between information theory and information flow across multiple traces. A prominent example is probabilistic schedulers that open up an opportunity for an attacker to set up a probabilistic covert channel. Or, probabilistic causation compares the probability of occurrence of an effect between scenarios where the cause is or is not present.
The state of the art on probabilistic hyperproperties has exclusively been studied in the context of discrete-time Markov chains (DTMCs). In [7], we proposed the temporal logic HyperPCTL, which extends PCTL by allowing explicit and simultaneous quantification over computation trees. For example, the DTMC in Fig. 1 satisfies the following HyperPCTL formula: ψ = ∀ŝ.∀ŝ ′ . initŝ ∧ initŝ′ ⇒ P( aŝ) = P( aŝ′ ) (1) which means, that the probability of reaching proposition a from any pair of statesŝ andŝ ′ labeled by init should be equal . Other works on probabilistic hyperproperties for DTMCs include parameter synthesis [8] and statistical model checking [5]. An important gap in the spectrum is verification of probabilistic hyperproperties with regard to models that allow nondeterminism, in particular, Markov decision processes (MDP). Nondeterminism plays a crucial role in many probabilistic systems. For instance, nondeterministic queries can be exploited in order to make targeted attacks to databases with private information [9]. To motivate the idea, consider the MDP in Fig. 2, where h is a high secret and l is a low publicly observable variable. To protect secret, there should be no probabilistic dependencies between observations on the low variable l and the value of h. However, an attacker that chooses a scheduler that always takes action α from states s 0 and s 1 can learn whether or not h ≤ 0 by observing the probability of obtaining l = 1 (or l = 2). On the other hand, a scheduler that always chooses action β, does not leak any information about the value of h. Thus, a natural question to ask is whether a certain property holds for all or some schedulers. With the above motivation, in this paper, we focus on probabilistic hyperproperties in the context of MDPs. Such hyperproperties inherently need to consider different nondeterministic choices in different executions, and naturally call for quantification over schedulers. There are several challenges to achieve this. In general, there are schedulers whose reachability probabilities cannot be achieved by any memoryless non-probabilistic scheduler, and, hence finding a scheduler is not reducible to checking non-probabilistic memoryless schedulers, as it is done in PCTL mode checking for MDPs. Consider for example the MDP in Fig. 3, for which we want to know whether there is a scheduler such that the probability to reach s 1 from s 0 equals 0.5. There are two non-probabilistic memoryless schedulers, one choosing action α and the other, action β in s 0 . The first one is the maximal scheduler for which s 1 is reached with probability 1, and the second one is the minimal scheduler leading to probability 0. However, the probability 0.5 cannot be achieved by any non-probabilistic scheduler. Memoryless probabilistic schedulers can neither achieve probability 0.5: if a memoryless scheduler would take action α with any positive probability, then the probability to reach s 1 is always 1. The only way to achieve the reachability probability 0.5 (or any value strictly between 0 and 1) is by a probabilistic scheduler with memory, e.g., taking α and β in s 0 with probabilities 0.5 each when this is the first step on a path, and β with probability 1 otherwise.
Our contributions in this paper are as follows. We first extend the temporal logic HyperPCTL [7] to the context of MDPs. To this end, we augment the syntax and semantics of HyperPCTL to quantify over schedulers and relate probabilistic computation trees for different schedulers. For example, the following formula generalizes (1) by requiring that the respective property should hold for all computation trees starting in any statesŝ andŝ ′ of the DMTC induced by any schedulerσ: On the negative side, we show that the problem to check HyperPCTL properties for MDPs is in general undecidable. On the positive side, we show that the problem becomes decidable when we restrict the scheduler quantification domain to memoryless non-probabilistic schedulers. We also show that this restricted problem is already NP-complete (respectively, coNP-complete) in the size of the given MDP for HyperPCTL formulas with a single existential (respectively, universal) scheduler quantifier. Subsequently, we propose an SMT-based encoding to solve the restricted model checking problem. We have implemented our method and analyze it experimentally on three case studies: probabilistic scheduling attacks, side-channel timing attacks, and probabilistic conformance (available at https://github.com/oreohere/HyperOnMDP).
Organization. Preliminary concepts are discussed in Section 2. We present the syntax and semantics of HyperPCTL for MDPs and discuss its expressive power in Section 3. Section 4 is dedicated to the applications of HyperPCTL. Sections 5 and 6 present our results on memoryless non-probabilistic schedulers and their evaluation before concluding in Section 7. All proofs appear in the appendix. -S is a nonempty finite set of states; -P : S×S → [0, 1] is a transition probability function with s ′ ∈S P(s, s ′ ) = 1, for all s ∈ S; -AP is a finite set of atomic propositions, and -L : S → 2 AP is a labeling function. . . ∈ S ω of states with P(s i , s i+1 ) > 0, for all i ≥ 0; we write π[i] for s i . Let Paths D s denote the set of all (infinite) paths of D starting in s, and fPaths D s denote the set of all non-empty finite prefixes of paths from Paths D s , which we call finite paths. For a finite path π = s 0 . . . s k ∈ fPaths D s0 , k ≥ 0, we define |π| = k. We will also use the notations Paths D = ∪ s∈S Paths D s and fPaths D = ∪ s∈S fPaths D s . A state t ∈ S is reachable from a state s ∈ S in D if there exists a finite path in fPaths D s with last state t; we use fPaths D s,T to denote the set of all finite paths from fPaths D s with last state in T ⊆ S. A state s ∈ S is absorbing if P(s, s) = 1.

Preliminaries
The cylinder set Cyl D (π) of a finite path π ∈ fPaths D s is the set of all infinite paths of D with prefix π. The probability space for D and state s ∈ S is (Paths . Note that the cylinder sets of two finite paths starting in the same state are either disjoint or one is contained in the other. According to the definition of the probability spaces, the total probability for a set of cylinder sets defined by the finite paths R ⊆ fPaths D s is Pr To improve readability, we sometimes omit the DTMC index D in the notations when it is clear from the context.
Simultaneous runs in different DTMCs can be formalized by parallel compositions.

Definition 2. The parallel composition of two DTMCs
with the following components: Markov decision processes extend DTMCs with non-deterministic choices. -S is a nonempty finite set of states; -Act is a nonempty finite set of actions; -P : S × Act × S → [0, 1] is a transition probability function such that for all s ∈ S the set of in s enabled actions Act(s) = {α ∈ Act | s ′ ∈S P(s, α, s ′ ) = 1} is not empty and s ′ ∈S P(s, α, s ′ ) = 0 for all α ∈ Act \ Act(s); -AP is a finite set of atomic propositions; -L : S → 2 AP is a labeling function.  and α∈Act\Act(s) act (q, s, α) = 0 for all s ∈ S and q ∈ Q; -mode : Q × S → Q is a mode transition function, and init : S → Q is a function selecting a starting mode for each state of M.
Let Σ M denote the set of all schedulers for the MDP M. A scheduler is finitememory if Q is finite, memoryless if |Q| = 1, and non-probabilistic if act (q, s, α) ∈ {0, 1} for all q ∈ Q, s ∈ S and α ∈ Act.
Definition 5. Assume an MDP M = (S, Act, P, AP, L) and a scheduler σ = (Q, act , mode, init) ∈ Σ M for M. The DTMC induced by M and σ is defined and L σ (q, s) = L(s) for all s, s ′ ∈ S and all q, q ′ ∈ Q.
A state s ′ is reachable from s ∈ S in MDP M is there exists a scheduler σ for M such that s ′ is reachable from s in M σ . A state s ∈ S is absorbing in M if s is absorbing in M σ for all schedulers σ for M. We sometimes omit the MDP index M in the notations when it is clear from the context.

HyperPCTL for MDPs
In this section we extend HyperPCTL from [7] for DTMCs, to argue also about non-determinism in MDPs.

HyperPCTL Syntax
HyperPCTL (quantified) state formulas ϕ q are inductively defined a follows: quantified formula ϕ q ::= ∀σ.ϕ q | ∃σ.ϕ q | ∀ŝ(σ).ϕ q | ∃ŝ(σ).ϕ q | ϕ nq non-quantified formula ϕ nq ::= true | aŝ | ϕ nq ∧ ϕ nq | ¬ϕ nq | ϕ pr < ϕ pr probability expression ϕ pr ::= P(ϕ path ) | f (ϕ pr 1 , . . . , ϕ pr k ) path formula whereσ is a scheduler variable 1 from an infinite setΣ ,ŝ is a state variable from an infinite setŜ, ϕ nq is a quantifier-free state formula, a ∈ AP is an atomic proposition, ϕ pr is a probability expression, f : [0, 1] k → R are k-ary elementary functions to express operations over probabilities, where constants are viewed as 0-ary functions, and ϕ path is a path formula, such that k 1 ≤ k 2 ∈ N ≥0 . The probability operator P allows the usage of probabilities in arithmetic constraints and relations. A HyperPCTL construct ϕ (probability expression ϕ pr , state formula ϕ q , ϕ nq or path formula ϕ path ) is well-formed if each occurrence of any aŝ with a ∈ AP andŝ ∈Ŝ is in the scope of a state quantifier forŝ(σ) for someσ ∈Σ , and any quantifier forŝ(σ) is in the scope of a scheduler quantifier forσ. We restrict ourselves to quantifying first the schedulers then the states, i.e., different state variables can share the same scheduler. One can consider also local schedulers when different players cannot explicitly share the same scheduler, or in other words, each scheduler quantifier belongs to exactly one of the quantified states.

HyperPCTL Semantics
The semantics of HyperPCTL is based on the n-ary self-composition of an MDP.
HyperPCTL state formulas are evaluated in the context of an MDP M = (S, Act, P, AP, L), a sequence σ = (σ 1 , . . . , σ n ) ∈ (Σ M ) n of schedulers, and a sequence r = ((q 1 , s 1 ), . . . , (q n , s n )) of M σ states; we use () to denote the empty sequence (of any type) and • for concatenation. Intuitively, these sequences store instantiations for scheduler and state variables. The satisfaction of a HyperPCTL quantified formula by M is defined by The semantics evaluates HyperPCTL formulas by structural recursion. Let in the following Q, Q ′ , . . . denote quantifiers from Q ∈ {∀, ∃}. When instantiating Qσ.ϕ by a scheduler σ ∈ Σ M , we replace in ϕ each subformula Q ′ŝ (σ).ϕ ′ , that is not in the scope of a quantifier forσ by Qŝ(σ).ϕ ′ , and denote the result by ϕ[σ σ]. For instantiating a state quantifier Qŝ(σ).ϕ by a state s, we append σ = (Q, act , mode, init ) and (init (s), s) at the end of the respective sequences, and replace each aŝ in the scope of the given quantifier by a s , resulting in a formula that we denote by ϕ[ŝ s n+1 ]. To evaluate probability expressions, we use the n-ary self-composition of the MDP.

The Expressiveness Power of HyperPCTL
For MDPs with |Act(s)| = 1 for each of its states s, the HyperPCTL semantics reduces to the one proposed in [7] for DTMCs. For MDPs with non-determinism, the standard PCTL semantics defines that in order to satisfy a PCTL formula P ∼c (ψ) in a given MDP state s, all schedulers should induce a DTMC that satisfies P ∼c (ψ) in s. Though it should hold for all schedulers, it is known that there exist minimal and maximal schedulers that are non-probabilistic and memoryless, therefore it is sufficient to restrict the reasoning to such schedulers. Since for MDPs with finite state and action spaces, the number of such schedulers is finite, PCTL model checking for MDPs is decidable. Given this analogy, one would expect that HyperPCTL model checking should be decidable, but it is not.

Theorem 1. HyperPCTL model checking for MDPs is in general undecidable.
What is the source of increased expressiveness that makes HyperPCTL undecidable? State quantification cannot be the source, as the state space is finite and thus there are finitely many possible state quantifier instantiations.
Assume an MDP M = (S, Act, P, AP, L) with a state s ∈ S that is uniquely labelled by the proposition init ∈ L(s), and let a, b ∈ AP. In PCTL, each probability bound needs to be satisfied under all schedulers. For example: Alternatively, we can state: where init σ (s) is the starting mode of scheduler σ in state s. Generally, the HyperPCTL fragment which starts with a single universal scheduler quantifier and contains a single bound on a single probability operator is still decidable. However, when a PCTL formula has several probability bounds, its satisfaction requires each bound to be satisfied by all schedulers independently. For example, This is not equivalent to the HyperPCTL formula which states that the probability is either less than or larger than 0.5 under all schedulers, which is true if there exists no scheduler under which the probability is 0.5. Thus, even for a fragment restricted to universal scheduler quantification, combinations of probability bounds allows HyperPCTL to express existential scheduler synthesis problems. Finally, consider a scheduler quantifier followed by state quantifiers, whose scope may contain probability expressions. This means we start several "experiments" in parallel, each one represented by a state quantifier. However, we may use in all experiments the same scheduler. Informally, this allows us to express the existence or absence of schedulers with certain probabilistic hyperproperties for the induced DTMCs. It would however also make sense to flip this quantifier order, such that state quantifiers are followed by scheduler quantifiers. This would mean, that we can use different schedulers in the different concurrently running experiments. This would be meaningful e.g. when users can provide input to the system, i.e. when the scheduler choice lies by the "observers" of the individual experiments, and they can adapt their schedulers to observations made in the other concurrently running experiments. Side-channel timing leaks open a channel to an attacker to infer the value of a secret by observing the execution time of a function. For example, the heart of the RSA public-key encryption algorithm is the modular exponentiation algorithm that computes (a b mod n), where a is an integer representing the plaintext and b is the integer encryption key. A careless implementation can leak b through a probabilistic scheduling channel (see Fig. 4). This program is not secure since the two branches of the if have different timing behaviors. Under a fair execution scheduler for parallel threads, an attacker thread can infer the value of b by running in parallel to a modular exponentiation thread and iteratively incrementing a counter variable until the other thread terminates (lines 12-14). To model this program by an MDP, we can use two nondeterministic actions for the two branches of the if statement, such that the choice of different schedulers corresponds to the choice of different bit configurations b(i) for the key b. This algorithm should satisfy the following property: the probability of observing a concrete value in the counter j should be independent of the bit configuration of the secret key b: ) r e t u r n 0 ; Another example of timing attacks that can be implemented through a probabilistic scheduling side channel is password verification which is typically implemented by comparing an input string with another confidential string (see Fig 5). Also here, an attacker thread can measure the time necessary to break the loop, and use this information to infer the prefix of the input string matching the secret string.
Scheduler-specific observational determinism policy (SSODP) [10] is a confidentiality policy in multi-threaded programs that defends against an attacker that chooses an appropriate scheduler to control the set of possible traces. In particular, given any scheduler and two initial states that are indistinguishable with respect to a secret input (i.e., low-equivalent), any two executions from these two states should terminate in low-equivalent states with equal probability. Formally, given a proposition h representing a secret: where l ∈ L are atomic propositions that classify low-equivalent states. A stronger variation of this policy is that the executions are stepwise low-equivalent: ∀σ.∀ŝ(σ).∀ŝ ′ (σ). hŝ ⊕ hŝ′ ⇒ P l∈L (P lŝ) = (P lŝ′ ) = 1 Probabilistic conformance describes how well a model and an implementation conform with each other with respect to a specification. As an example, consider a 6-sided die. The probability to obtain one possible side of the die is 1/6. We would like to synthesize a protocol that simulates the 6-sided die behavior only by repeatedly tossing a fair coin. We know that such an implementation exists [11], but our aim is to find such a solution automatically by modeling the die as a DTMC and by using an MDP to model all the possible coin-implementations with a given maximum number of states, including 6 absorbing final states to model the outcomes. In the MDP, we associate to each state a set of possible nondeterministic actions, each of them choosing two states as successors with equal probability 1/2. Then, each scheduler corresponds to a particular implementation. Our goal is to check whether there exists a scheduler that induces a DTMC over the MDP, such that repeatedly tossing a coin simulates die-rolling with equal probabilities for the different outcomes: ∃σ.∀ŝ(σ).∃ŝ ′ (σ). initŝ ∧ initŝ′ ⇒

HyperPCTL Model Checking for Non-probabilistic Memoryless Schedulers
Due to the undecidability of HyperPCTL formulas for MDPs, we focus in this section on an alternative semantics, where scheduler quantification ranges over nonprobabilistic memoryless schedulers only. It is easy to see that limiting ourselves to non-probabilistic memoryless schedulers makes the model checking problem decidable, as there are only finitely many such schedulers. Regarding complexity, we have the following property.
Theorem 2. The problem to decide for MDPs the truth of HyperPCTL formulas with a single existential (respectively, universal) scheduler quantifier over nonprobabilistic memoryless schedulers is NP-complete (respectively, coNP-complete) in the state set size of the given MDP.
Next we propose an SMT-based technique for solving the model checking problem for non-probabilistic memoryless scheduler domains, and for the simplified case of having a single scheduler quantifier; the general case for an arbitrary number of scheduler quantifiers is similar, but a bit more involved, so the simplified setting might be more suitable for understanding the basic ideas. The main method listed in Algorithm 1 constructs a formula E that is satisfiable if and only if the input MDP M satisfies the input HyperPCTL formula with a single scheduler quantifier over the nonprobabilistic memoryless scheduler domain. Let us first deal with the case that the scheduler quantifier is existential. In line 2 we encode possible instantiations σ for the scheduler variableσ, choosing in each MDP state s ∈ S a certain enabled action α ∈ Act(s) with probability one. In line 4 we encode the meaning of the quantifier-free inner part ϕ nq of the input formula, whereas line 5 encodes the meaning of the state quantifiers, i.e. for which sets of composed states ϕ nq needs to hold in order to satisfy the input formula. In lines 6-7 we check the satisfiability of the encoding and return the corresponding answer. Formulas with a universal scheduler quantifier ∀σ.ϕ are semantically equivalent to ¬∃σ.¬ϕ. We make use of this fact in lines 8-12 to check first the satisfaction of an encoding for ∃σ.¬ϕ and return the inverted answer.  The Semantics method, shown in Algorithm 2, applies structural recursion to encode the meaning of its quantifier-free input formula. As variables, the encoding uses (1) propositions prob s,ϕ nq ∈ {0, 1} to encode the truth of each Boolean sub-formula ϕ nq of the input formula in each state s ∈ S n of the n-ary self-composition of M; (2) numeric variables prob s,ϕ pr ∈ [0, 1] ⊆ R to encode the value of each probability expression ϕ pr in the input formula in the context of each composed state s ∈ S n .
There are two base cases: the Boolean constant true holds in all states (line 2), whereas atomic propositions hold in exactly those states that are labelled by them (line 3). For conjunction (line 5) we recursively encode the truth values of the operands and state that the conjunction is true iff both operands are true.
..×supp(sn,αn) (holds s ′ ,ϕ 2 ∨ds,ϕ 2 >d s ′ ,ϕ 2 ))) ; For the probabilities P(ϕ 1 U ϕ 2 ) to satisfy an unbounded until formula, the method SemanticsUnboundedUntil shown in Algorithm 3 first encodes the meaning of the until operands (line 2). For each composed state s ∈ S n , the probability of satisfying the until formula in s is encoded in the variable prob s,P(ϕ1 U ϕ2) . If the second until-operand ϕ 2 holds in s then this probability is 1 and if none of the operands are true in s then it is 0 (line 4). Otherwise, depending on the scheduler σ of M (line 5), the value of prob s,P(ϕ1 U ϕ2) is a sum, adding up for each successor state s ′ of s the probability to get from s to s ′ in one step times the probability to satisfy the until-formula on paths starting in s ′ (line 7). However, these encodings work only when at least one state satisfying ϕ 2 is reachable from s with a positive probability: for any bottom SCC whose states all violate ϕ 2 , the probability P(ϕ 1 U ϕ 2 ) is obviously 0, however, assigning any fixed value from [0, 1] to all states of this bottom SCC would yield a fixed-point for the underlying equation system. To assure correctness, in line 8 we enforce smallest fixed-points by requiring that if prob s,P(ϕ1 U ϕ2) is positive then there exists a loop-free path from s to any state satisfying ϕ 2 . In the encoding of this property we use fresh variables d s,ϕ2 and require a path over states with strong monotonically decreasing d s,ϕ2 -values to a ϕ 2 -state (where the decreasing property serves to exclude loops).
The SemanticsBoundedUntil method, listed in Algorithm 4, encodes the probability P(ϕ 1 U [k1,k2] ϕ 2 ) of a bounded until formula in the numeric variables prob s,P(ϕ1 U [k 1 ,k 2 ] ϕ2) for all (composed) states s ∈ S n and recursively reduced time bounds. There are three main cases: (i) the satisfaction of ϕ 1 U [0,k2−1] ϕ 2 requires to satisfy ϕ 2 immediately (lines 2-5): (ii) ϕ 1 U [0,k2−1] ϕ 2 can be satisfied by either satisfying ϕ 2 immediately or satisfying it later, but in the latter case ϕ 1 needs to hold currently (lines 6-12); (iii) ϕ 1 has to hold and ϕ 2 needs to be satisfied some time later (lines [13][14][15][16][17][18][19]. To avoid the repeated encoding of the semantics of the operands, we do it only when we reach case (i) where recursion stops (line 3). For the other cases, we recursively encode the probability to reach a ϕ 2 -state over ϕ 1 states where the deadlines are reduced with one step (lines 7 resp. 14) and use these to fix the values of the variables prob s,P(ϕ1 U [k 1 ,k 2 ] ϕ2) , similarly to the unbounded case but under additional consideration of time bounds. Finally, the Truth method listed in Algorithm 5 encodes the meaning of the state quantification: it states for each universal quantifier that instantiating it with any MDP state should satisfy the formula (conjunction over all states in line 3), and for each existential state quantification that at least one state should lead to satisfaction (disjunction in line 4).
We note that the satisfiability of the generated SMT encoding for a formula with an existential scheduler quantifier does not only prove the truth of the formula but provides also a scheduler as witness, encoded in the solution of the SMT encoding. Conversely, unsatisfiability of the SMT encoding for a formula with a universal scheduler quantifier provides a counterexample scheduler.

Evaluation
We developed a prototypical implementation of our algorithm in python, with the help of several libraries. There is an extensive use of STORMPY [12,13], which provides efficient solution to parsing, building, and storage of MDPs. We also have used the SMT-solver Z3 [15] to solve the generated SMT encoding by Algorithm 1. All of our experiments are run on a MacBook Pro laptop with a 2.7GHz i7 processor with 8GB of RAM. The experimental results are presented in Table 1.
As a first case study, we model and analyze information leakage in the modular exponentiation algorithm (function modexp in Fig. 4); the corresponding results in Table 1 are marked by TA. We experimented with 1, 2, and 3 bits for the encryption key (hence, m ∈ {2, 4, 6}). The specification checks whether there is a timing channel for all possible schedulers, which is the case for the implementation in modexp.
Our second case study is verification of password leakage thorough the string comparison algorithm (function str cmp in Fig 5). Here, we also experimented with m ∈ {2, 4, 8}; results in Table 1 are denoted by PW.
In our third case study we assume two concurrent processes. The first process decrements the value of a secret h by 1 as long as the value is still positive, and after this it sets a low variable l to 1. A second process just sets the value of the same low variable l to 2. The two threads run in parallel; as long as none of them terminated, a fair scheduler chooses for each CPU cycle the next executing thread. As discussed in Section 1, this MDP opens a probabilisitc thread scheduling channel and leaks the value of h. We denote this case study by TS in Table 1 ) has 35 reachable states, verification of TS takes 20 times more than TA. We believe this is due to the fact that the MDP of TS is twice deeper than the MDP of TA, making the SMT constraints more complex.
Our last case study is on probabilistic conformance, denoted PC. The input is a DTMC that encodes the behavior of a 6-sided die as well as a structure of actions having probability distributions with two successor states each; these transitions can be pruned using a scheduler to obtain a DTMC which simulates the die outcomes using a fair coin. Given a fixed state space, we experiment with different numbers of transitions.
Regarding the running times listed in Table 1, we note that our implementation is only prototypical and there are possibilities for numerous optimizations. Most importantly, for purely existentially or purely universally quantified formulas, we could define a more efficient encoding with much less variables. However, it is clear that the running times for even relatively small MPDs are large. This is simply because of the high complexity of the verification of hyperproperties. In addition, the HyperPCTL formulas in our case studies have multiple scheduler and/or state quantifiers, making the problem significantly more difficult.

Conclusion and Future Work
We investigated the problem of specifying and model checking probabilistic hyperproperties of Markov decision processes (MDPs). Our study is motivated by the fact that many systems have probabilistic nature and are influenced by nondeterministic actions of their environment. We extended the temporal logic HyperPCTL for DTMCs [7] to the context of MDPs by allowing formulas to quantify over schedulers. This additional expressive power leads to undecidability of the HyperPCTL model checking problem on MDPs, but we also showed that the undecidable fragment becomes decidable for non-probabilistic memoryless schedulers. Indeed, all applications discussed in this paper only require this type of schedulers.
Due to the high complexity of the problem, more efficient model checking algorithms are greatly needed. An orthogonal solution is to design less accurate and/or approximate algorithms such as statistical model checking that scale better and provide certain probabilistic guarantees about the correctness of verification. Another interesting direction is using counterexample-guided techniques to manage the size of the state space.
A Proof of Theorem 1 Theorem 1. HyperPCTL model checking for MDPs is in general undecidable.
Proof. We reduce the emptiness problem in probabilistic Büchi automata (PBA), which is known to be undecidable [16], to our problem.

A.1 Probabilistic Büchi Automata
PBA can be viewed as nondeterministic Büchi automata where the nondeterminism is resolved by a probabilistic choice. That is, for any state q and letter a in alphabet Σ, either q does not have any a-successor or there is a probability distribution for the a-successors of q.
is the transition probability function, such that for all q ∈ Q and a ∈ Σ: and F ⊆ Q is the set of accepting states.
A run for an infinite word w = a 1 a 2 · · · ∈ Σ ω is an infinite sequence π = q 0 q 1 q 2 · · · of states in Q, such that q i+1 ∈ δ(q i , a i+1 ) = {q ′ | δ(q i , a i+1 , q ′ ) > 0} for all i ≥ 0. Let Inf(π) denote the set of states that are visited infinitely often in π. Run π is called accepting if Inf(π) ∩ F = {}. Given an infinite input word w ∈ Σ ω , the behavior of P is given by the infinite Markov chain that is obtained by unfolding P into a tree using w. This is similar to an induced Markov chain from an MDP by a scheduler. Hence, standard concepts for Markov chains can be applied to define the acceptance probability of w in P, denoted by Pr P (w) or briefly Pr(w), by the probability measure of the set of accepting runs for w in P. We define the accepted language of P as: The emptiness problem is to decide whether or not L(P) = {} for a given input P.

A.2 Mapping
Our idea of mapping the emptiness problem in PBA to HyperPCTL model checking for MDPs is as follows. We map a PBA to an MDP such that the words of the PBA are mimicked by the runs of the MDP. In other words, letters of the words in the PBA appear as propositions in states of the MDP. This way, the existence of a word in the language of the PBA corresponds to the existence of a scheduler that produces a satisfying computation tree in the induced Markov chain of the MDP.
MDP M = (S, Act, P, AP, L): Let P = (Q, δ, Σ, F ) be a PBA with alphabet Σ. We obtain an MDP M = (S, Act , P, AP, L) as follows: -The set of states S = Q × Σ, -The set of actions Act = Σ -The transition probability function P is defined as follows: -The set of atomic propositions AP = Σ ∪ {f }, where f ∈ Σ (we use f to label the accepting states), -The labeling function L is defined as follows. For each a ∈ Σ and q ∈ Q, we have: HyperPCTL formula: The HyperPCTL formula in our mapping is the following: Intuitively, the formula establishes connection between the PBA emptiness problem and HyperPCTL model checking MDPs. In particular: -The existence of schedulerσ in ϕ map corresponds to the existence of a word w in L(P); -The state quantifiers and the left conjunct ensure that the path in the induced Markov chain and the PBA follow the sequence of actions (respectively, letters) in the witness toσ (respectiely, w), and -The right conjunct mimics that a state in F is visited with non-zero probability if and only if a state labeled by proposition f is visited infinitely often in the MDP with non-zero probability.

A.3 Reduction
We now show that L(P) = ∅ if and only if M |= ϕ map . We distinguish two cases: -(⇒) Suppose we have L(P) = ∅. This means there exists a word w ∈ Σ ω , such that Pr P (w) > 0. We use w to eliminate the existential scheduler quantifier and instantiateσ in formula ϕ map . This induces a DTMC and now, we show that the induced DTMC satisfies the following HyperPCTL formula as prescribed in [7]: To this end, observe that the right conjunct is trivially satisfied due to the fact that Pr P (w) > 0. That is, since a state in F is visited infinitely often with non-zero probability in P, a state labeled by f in M is also visited infinitely often with non-zero probability. The left conjunct is also satisfied by construction of the mapped MDP, since the sequence of letters in w appear in all paths of the induced DTMC as propositions. -(⇐) The reverse direction is pretty similar. Since the answer to the model checking problem is affirmative, a witness to scheduler quantifierσ exists. This scheduler induces a DTMC whose paths follow the same sequence of propositions. This sequence indeed provides us with the word w for P. Finally, since the right conjunct in ϕ map is satisfied by the MDP, we are guaranteed that w reaches an accepting state in F infinitely often with non-zero probability.
And this concludes the proof.

B Proof of Theorem 2
Theorem. 2 The problem to decide for MDPs the truth of HyperPCTL formulas with a single existential (respectively, universal) scheduler quantifier over nonprobabilistic memoryless schedulers is NP-complete (respectively, coNP-complete) in the state set size of the given MDP.
Proof. In order to show membership to NP, let M be an MDP and ϕ = ∃σ.ϕ ′ be a HyperPCTL formula. We show that given a solution to the problem, we can verify the solution in polynomial time. Observe that given a non-probabilistic memoryless scheduler as a witness to the existential quantifier ∃σ, one can compute the induced DTMC and then verify the DTMC against the resulting HyperPCTL formula in polynomial time in the size of the induced DTMC [7]. Inspired by the proof technique introduced in [17], for the lower bound, we reduce the SAT problem to our model checking problem.

B.1 The Satisfiability Problem
The SAT problem is as follows: Let {x 1 , x 2 , . . . , x n } be a set of propositional variables. Given is a Boolean formula y = y 1 ∧ y 2 ∧ · · · ∧ y m , where each y j , for j ∈ [1, m], is a disjunction of at least three literals. Is y satisfiable? That is, does there exist an assignment of truth values to x 1 , x 2 , . . . , x n , such that y evaluates to true.

B.2 Mapping
We now present a mapping from an arbitrary instance of SAT to the model checking problem of an MDP and a HyperPCTL formula of the form ∃σ.∃ŝ(σ).∀ŝ ′ (σ).ψ. Then, we show that the MDP satisfies the this formula if and only if the answer to the SAT problem is affirmative. Figure 6 shows an example. MDP M = (S, Act , P, AP, L): -(Atomic propositions AP) We include four atomic propositions: p andp to mark the positive and negative literals in each clause and c andc to mark paths that correspond to clauses of the SAT formula. Thus, AP = p,p, c,c}.
-(Set of states S) We now identify the members of S: • For each clause y j , where j ∈ [1, m], we include a state r j , labeled by proposition c. We also include a state r 0 labeled byc • For each clause y j , where j ∈ [1, m], we introduce the following n states: Each state v j i is labeled with proposition p if x i is a literal in y j , or with p if ¬x i is a literal in y j .
• For each Boolean variable x i , where i ∈ [1, n], we include two states s i ands i . Each state s i (respectively,s i ) is labeled by p (respectively,p).
-(Set of actions Act) The set of actions is Act = {α, β, γ}. Intuitively, the scheduler chooses action α (respectively, β) at a state s i ors i to assign true (respectively, false) to variable x i+1 . Action γ is the sole action available at all other states. -(Transition probability function P) We now identify the members of P . All transitions have probability 1, so we only discuss the actions.
• We add transitions (r j , γ, v j 1 ) for each j ∈ [1, m], where from r j , the probability of reaching v j 1 is 1. • For each i ∈ [1, n), we include transitions (s i , α, s i+1 ), (s i , β,s i+1 ), (s i , α, s i+1 ), and (s i , β,s i+1 ). The intuition here is that when the scheduler chooses action α at state s i ors i , variable x i+1 evaluates to true and when the scheduler chooses action β at state s i ors i , variable x i+1 evaluates to false in the SAT instance. We also include two transitions (r 0 , α, s 1 ) and (r 0 , β,s 1 ) with the same intended meaning. • Finally, we include self-loops (s n , γ, s n ), (s n , γ,s n ), and (v j n , γ, v j n ), for each j ∈ [1, m].

B.3 Reduction
We now show that the given SAT formula is satisfiable if and only if the MDP obtained by our mapping satisfies the HyperPCTL formula ϕ map .
(⇒) Suppose that y is satisfiable. Then, there is an assignment that makes each clause y j , where j ∈ [1, m], true. We now use this assignment to instantiate a scheduler for the formula ϕ map . If x i = true, then we instantiate schedulerσ such that in state s i−1 ors i−1 , it chooses action α. Likewise, if x i = false, then we instantiate schedulerσ, such that in state s i−1 ors i−1 , it chooses action β. We now show that this scheduler instantiation evaluates formula ϕ map to true. First observe thatŝ(σ) can only be instantiate with state r 0 andŝ ′ (σ) can only be instantiate with states r j , where j ∈ [1, m]. Otherwise, the left side of the implication in ϕ map becomes false, making the formula vacuously true. Since each y j is true, there is at least one literal in y j that is true. If this literal is of the form x i , then we have x i = true and the path that starts from r 0 will include s i , which is labeled by p. Hence, the values of p, in both paths that start fromŝ(σ) andŝ ′ (σ) are eventually equal. If the literal in y j is of the form ¬x i , then x i = false and the path that starts fromŝ(σ) will includes i . Again, the values ofp are eventually equal. Finally, since all clauses are true, all paths that start fromŝ ′ (σ) reach a state where the right side of the implication becomes true. (⇐) Suppose our mapped MDP satisfies formula ϕ map . This means that there exists a scheduler and stateŝ(σ) that makes the subformula ∀ŝ ′ (σ) true, i.e., the path that starts from r 0 results in making the inner PCTL formula true for all paths that start from r j . We obtain the truth assignment to the SAT problem as follows. If the scheduler chooses action α to state s i , then we assign x i = true. Likewise, if the scheduler chooses action β to statē s i , then we assign x i = false. Observe that since in no state p andp are simultaneously true and no path includes both s i ands i , variable x i will have only one truth value. Similar to the forward direction, it is straightforward to see that this valuation makes every clause y j of the SAT instance true.
And this concludes the proof.