We show how to extrapolate an optimal policy controlling a model, which is itself too large to nd the policy directly using probabilistic model checking (PMC). In particular, we look for a global optimal resolution of non{determinism in several small Markov Decision Processes (MDP) using PMC. We then use the resolution to nd a respective set of decision boundaries representing the optimal policies found. Then, a hypothesis is formed on an extrapolation of these boundaries to an equivalent boundary in a large MDP. The resulting hypothetical extrapolated decision boundary is statistically approximately veri ed, whether it indeed represents an optimal policy for the large MDP. The veri cation either weakens or strengthens the hypothesis. The criterion of the optimality of the policy can be expressed in any modal logic that includes the probabilistic operator P p[ ], and for which a PMC method exists.
Probabilistic model checking (PMC) [
A policy of a decision maker (an agent), controlling a Markov Decision
Process (MDP), resolves a non{deterministic choice, which exist in each state of an
MDP in the form of a number of probability distributions over states, of which
one is arbitrarily chosen (for details see Sec. 2). An optimal policy [
Statistical probabilistic model checking (SPMC) [
We address the issue of an estimation of an optimal policy in a model, which is too large to have that policy found using PMC, and also too large to have that policy estimated using SPMC, if an initial, su ciently precise approximation of the policy is unknown. In order to obtain , we rst nd a number of equivalent optimal policies in several scaled-down versions of the large model. Then, we pose a hypothesis on an extrapolation of these policies to the large model. Finally, we strengthen or weaken the hypothesis using SPMC, which approximately veri es, whether the extrapolated policy is optimal by checking whether the policy has the largest tness, when compared to a number of its close variants.
In particular, we begin with searching for a global optimal resolution of non{
determinism [
The paper is constructed as follows. In Sec. 2 we de ne the formalism used. In Sec. 3 we propose a technique which extrapolates and veri es an optimal policy. In Sec. 4 we present a case study. In the last section we conclude the paper. 2
Let us de ne the formalism used throughout the paper. It is fairly standard and
follows [
A discrete-time Markov chain (DTMC) consists of states that represent instantaneous snapshots of the system at a given time, and has transitions labelled by (discrete) probability distributions over the target states.
De nition 1. A DTMC is a tuple D = (S; s ; T; AP; L), where S is a nite set of states, s is the initial state, T : S S ! [0; 1] is a transition probability function such that Ps02S T (s; s0) = 1 for all s 2 S, AP is a set of atomic propositions, and L : S ! 2AP is a valuation function which assigns to every state s 2 S a set L(s) of atomic propositions that are assumed to be true at that state.
Observe that each transition represents the possibility to evolve from one state to another. Moreover, for a state s 2 S of D, the probability of moving to a state s0 2 S in one discrete step is given by T (s; s0). Further, a path of D is an in nite sequence ! = s0; s1; s2; : : : of states such that T (si; si+1) > 0 for all i 0. Each path of D provides one possible evolution of the Markov chain.
Properties of DTMCs can be written in Probabilistic Computation Tree Logic
(PCTL) [
U j
U k
PCTL formulae are interpreted over the states of a DTMC or Markov decision processes (see next section). We say that a state s 2 S satis es a PCTL formula , denoted D; s j= , if is true at the state s. Intuitively, a state s satis es the basic state formula P p[ ] if the probability of taking a path from s satisfying path formula meets the bound p. Further, the path formula X (operator neXt ) is true, if is satis ed in the next state; the path formula 1U 2 (operator until ) is true, if 2 is eventually satis ed and 1 is true until then; the path formula 1U k 2 (operator bounded until ) is true, if 2 is satis ed within k discrete steps and 1 is true until then.
In practice, it is common to write formulae of the following kind: P=?[ ], which asks \what is the probability of to be true". Also, the following useful operators can be derived from the above PCTL syntax: F ::= true U (eventually becomes true) and G ::= :F: ( is true globally ), and a bounded variants of these. 2.2
A Markov decision process (MDP), like DTMC, consists of states, representing possible con gurations of the system being modelled, and transitions between states occur in discrete time-steps. However, at each state the system (decision maker) may choose any action that is available in this state, and then non{ deterministically move into a new state, while providing the decision maker a corresponding probability.
De nition 3. An MDP is a tuple M = (S; s ; Act; ; AP; L), where: { S, s , AP and L : S ! 2AP are de ned as for DTMCs, { Act is a nite set of actions, { : S Act ! Dist(s) is the (partial) transition probability function, with
Dist(S) denoting the set of all discrete probability distributions over S. Observe that for each state s 2 S, the successor state is determined in two stages: rstly, an available action a 2 Act (i.e. one for which (s; a) is de ned) is non{ deterministically selected; secondly, the successor is randomly chosen according to the probability distribution (s; a).
To reason formally about the behaviour of MDPs, normally, the notation of
policies is used. A policy resolves all of the non{deterministic choices in an MDP.
Moreover, under the control of a particular policy, the behaviour of an MDP is
fully probabilistic and, as is for DTMCs, one can de ne a probability space over
the possible paths through the model. Further, it is possible to reason about the
best{ or worst{case system behaviour by quantifying over all possible policies:
for example, it is possible to compute the minimum or maximum probability of
a PCTL property. Finally, the notion of an optimal policy can be used with a
property value optimised by a model checker. For example, Prism [
Properties of MDPs can also be written in PCTL, yet with an implicit quanti cation over policies. For example, the P=? operator used for DTMCs is replaced with two variants Pmin=? (the minimum probability) and Pmax=? (the maximum probability). 3
Let M = (S; s ; Act; ; AP; L) be an MDP. We rst de ne an MDP with classi ed binary choices (MDPCBC) as follows.
De nition 4. An MDPCBC is a tuple X = (S; s ; Act; ; AP; L), where: { S, s , AP and L : S ! 2AP are de ned as for MDPs, { Act = Si=1 Acti is a nite set of actions that is divided into disjoint classes Acti according to their meaning as understood in the modelled phenomenon. Moreover, each class Acti is divided into two disjoint sets of the same size: Acti# and Acti". { : S Act ! Dist(s) is the (partial) transition probability function, with Dist(S) denoting the set of all discrete probability distributions over S, and the following property: any non{deterministic binary choice q contains exactly two actions aq# and aq" such that aq# 2 Acti# and aq" 2 Acti".
For example, if Act = Act1 [ Act2, then Act1 might represent choices of either a black or a white ball and Act2 might represent a decisions if to continue a loop of choosing the balls or, on the contrary, stop the process. Further, if a non{deterministic binary choice represents a class of actions \a choice of either a black or a white ball", then Act1# would contain only choices of the black ball and Act1" would contain only choices of the white ball.
Now we de ne the notation of a decision boundary.
De nition 5. Let X = (S; s ; Act; ; AP; L) be an MDPCBC, and let the binary non{deterministic choices between actions belonging to Acti be available at certain states Si S. A decision boundary is a function Di : Si ! f false; trueg such that if there is a non{deterministic choice between actions aq # and aq ", then the agent chooses aq# if Di(s) = false, and aq" otherwise.
Thus, a decision boundary determines a certain policy controlling an MDPCBC, which then becomes a DTMC, further called a Markov chain with classi ed binary choices (MCCBC).
As seen, thanks to the division of Act into classes, we have a number of class{speci c decision boundaries, which individually may be easier to describe mathematically. On the contrary, mixing actions with vastly di erent meanings might produce a common decision boundary which is hard to analyse. 3.1
Let there be a set X = fXs1mall; : : : ; XsJmall; Xlargeg of MDPCBCs, instantiated
from a common template, but with di erent values of the parameter N , equal
respectively to fNs1mall; : : : ; NsJmall; Nlargeg. The parameter does not in uence on
the nature of the problem, but merely represents a scale of the problem. N can
be e.g. the number of philosophers in the Dining Philosophers Problem [
Let the decision boundary for class i in Xsmall be Dij (s), s 2 Si, and j let us pose a hypothesis on how Dij (s) can be merged into a single function. The hypothesis is represented by Di(s; N ), which generalises all Dij (s) so that Dij (s) = Di(s; Nsjmall); j = 1; : : : ; J . This allows for obtaining a hypothetical extrapolated decision boundary Di(s; Nlarge), controlling Xlarge. Finally, we strengthen or refute the posed hypothesis, by locally verifying the tness of Di(s; Nlarge) using SPMC. 3.2
Let any state in S be represented by a tuple V = (x1; : : : ; xd), a so{called state vector, each of its elements represents some speci c phenomenon in a modelled system. For example V might have an interpretation (temperature; precipitation). Let us build a real coordinate metric space S such that any state s is mapped to a point Vs in S , having coordinates V . We do that because we hope that points close in S may intuitively represent similar situations in the modelled system, thus it is less likely that a decision boundary goes between them. This hopefully simpli es both the shape and semantic interpretation of Di(s; N ).
Due to, amongst others, a nite jjSjj, the extrapolation to Di(s; Nlarge) might be imprecise. Consider the following. See that jjVsjj = jjSjj is nite, and thus we can nd some > 0 which is equal to the closest distance between all possible pairs (Vs1 ; Vs2 ), s1; s2 2 S; s1 6= s2. Therefore, there is an in nite number of decision boundaries representing a single policy. Let any decision boundary be represented by a vector of parameters C(N ) = (y1N ; : : : ; yN ), where 2 N+ is a constant speci c to a method of the representation. For any class i, we can extrapolate Di(s; N ) by a respective extrapolation of J vectors Ci(Nsjmall) to a single vector Ci(Nlarge), the latter determining Di(s; Nlarge). Yet, as C(N ) is arbitrary due to > 0, so is Ci(Nlarge). Moreover, as the extrapolation may augment the arbitrariness, the multiple possible values of Ci(Nlarge) may in turn represent multiple Di(s; Nlarge). y1
Consider the example in Fig. 1(a). C1(100), C1(101) and C1(102) determine a common segment. We extrapolate that segment with a line in order to nd C1(300) = (u; v), which in turn determines hypothetical D1(s; 300). Yet, as MDPCBCs have a nite number of states, C1(300) can not be determined precisely: minor arbitrariness in the placement of the segment scale up roughly a nely with the distance to the segment. We thus see, that there is at least a single reason for Di(s; Nlarge) to be a hit{and{miss when it comes to an estimation of a strategy for Xlarge. 4
Let us study an example { an optimal policy of choosing a coin. There are two coins, a fair one and an unbalanced one. They have the probabilities of the outcome of heads equal to respectively 0.5 and 0.6. A decision maker ips a coin N times, deciding before each ip, which of the two coins to choose (for simplicity, N is even). What is the best policy of maximising the probability of drawing N=2 heads within these ips? The criterion of optimality is thus Popt = Pmax=?[F(f = N ^ h =
N 2 )] Let N be the scaling parameter discussed in Sec. 3.
Let us rst verify a small variant of the model, with N = Nsmall = 100, using Prism's PMC capabilities. Prism is able to compute the optimal policy of a decision maker which has a full knowledge about the system, and the computed policy is given as a transition matrix of a DTMC, which in the case of our model is also an MCCBC. The policy is visualised in Fig. 2(a), where f and h are parts of the vector state which are equal to, respectively, the number of tosses so far and the number of heads drawn so far.
Let Act1" be a choice of the fair coin. The decision boundary, approximated by visually interpreting Fig. 2(a), is h & 0:55 (f 0 fc tosses f (a)
hc 100
Fig. 2(b) depicts probability distributions of h after all Nsmall tosses. As seen, (2) makes (1) almost twice as large if compared to a state{agnostic approach of always choosing the fair coin. 4.1
Firstly, we will attempt to extrapolate from only (2), i.e. let J = 1. Assuming limited computational resources for nding optimal policies of small models, j J = 1 enables us to use the largest possible Nsmall.
Extrapolation. In order to extrapolate from a single point, we will form some supporting hypotheses. It is easy to see that at the state (f = 0; h = 0) the decision maker should choose the fair coin for any N . This is because he is more afraid of an excessively large h, rather than of the number of heads drawn being too small, as the single available unbalanced coin leans towards heads, and thus it can be used to reduce the de ciency of h. The latter also says, that a high de ciency of h leads to the choice of the unbalanced coin. Therefore, we know that at some (f fc; h = 0), fc > 0, the unbalanced coin is chosen, and that for any N , the fair coin is chosen for (0 f < fc; h = 0). We also know that at (f = N 1; h = N=2 1) the decision maker should maximise the probability of drawing a head in order to reach (f = N; h = N=2) (the success is assured only if a head will be drawn, an unbalanced coin is chosen), and that he would minimise that probability for (f = N 1; h = N=2) (the success is assured only if a head will not be drawn, a fair coin is thus chosen). Therefore, we know that for any N the decision boundary goes between these two states. ] ) N 2 0.102 = h 0.1 ^ N 0.098 = f ( F [ ? = P
On the basis of (2) we can guess that the decision boundary is a segment. Let us guess that the placement of the segment scales a nely with N in the sense that fc N=G, where G is a constant. This hypothesis is trivially represented by the following decision boundary: h > h1(f ) =
N 2
f N 1 fc fc =
N 2 1=2
N f 1
N=G
N=G thus
Di(s; N ) = 1=2 8 <G < :true
N
N 1 Veri cation. Using (2) we can estimate G = Ns1mall=fc 100=(9 0:5) 2";G = h10:5; 11:8i. Checking statistically Popt in an MDPCBC controlled by (3) for N = Nlarge = 5000 and G 11 2 G yields the diagram in Fig. 3. An MCCBC with the highest Popt is found for G = G1 = 11, which agrees with the estimation, and we may thus strengthen the hypothesis.
Local maxima are seen in the diagram. For example, we statistically checked MCCBCs for a dense set of values of G in a set G10 such that 8Gi2G10 0:95 Gi 10:05; jjG10jj = 51, then we tted a parabola as seen in the gure, to show that a local gradient{descent optimiser might be trapped in a local maximum around G 10, thus strengthening a respective false hypothesis.
We thus see, that an interval of G wider than the one spanned over G10
should be sampled by such an optimiser. This leads to a considerable numerical
complexity of the resulting SPMC, as we need to use as much as 5 107 samples
per a single estimation in order to get a 99% con dence level of 2:3 10 4,
estimated using Asymptotic Con dence Interval [
A less precise extrapolation might increase the said complexity even more. For example, { a less precise initial estimation of G might result in a larger number of samples to be gathered, in order to localise the maximum around G = 11; { if we would merely assume, that the decision boundary is a segment, whose both ends are unknown and with no known relation, and not that only fc is unknown as we did so far, we would then need to search within at least a two{dimensional optimisation space. For example one with the optimised parameters (G; H) such that the linear boundary of D1(Nlarge) intersects a pair of points (fc = Nlarge=G; 0), (Nlarge 1; H).
Obviously, in general, an MDPCBC with N = Nlarge might become unveri able using both PMC and SPMC, if the extrapolation from PMC{checked models were insu ciently precise or unknown at all. 4.2
We will attempt to estimate D1(Nlarge) using several small MDPCBCs. We won't use the reasoning from Sec. 4.1, but instead, an optimiser will analyse a trajectory of parameters representing di erent decision boundaries.
Extrapolation. We apply a Nelder{Mead Simplex gradient{descent
optimiser [
G
G2 = 10:982 (4) Testing (4) against the three MCCBC matrices returned by Prism, it turns out that this boundary always allows for a right choice within the three MDPCBCs in question. It may be a hint, that the said linear combination has been a right choice.
Veri cation. Due a nite number of states in the MDPCBCs from which we have extrapolated, we may expect imprecisions in (4) as discussed in Sec. 3, especially that we extrapolate from Nsjmall 100 to Nlarge 5000, i.e. to a model with a number of tosses about 50 times as large on average.
We know from the reasoning in Sec. 4.1, that N=2 1 h(N 1) < N=2. For N = Nlarge, h2(Nlarge 1) 2498:95, and is thus too small by 0:05, a di erence which seems to be fairly precise for an extrapolation that distant. Yet, we will correct that imprecision by placing the segment correctly at f = Nlarge 1, and then extracting from (4) merely the value of G2. This boils down to the reuse of the diagram in Fig. 3. Given the low number of statistically veri ed MCCBCs in the diagram and the considerable size of the 99% con dence interval, given in Sec. 4.1, it can be stated that G2 G1. We may thus strengthen the hypothesis.
We are working on a tool for automating the presented extrapolation. As opposed
to the example in the case study, it would apply a number of extrapolating
functions beside a linear combination, in order to choose the best extrapolated policy.
For example, the tool could support an extrapolation of oscillating functions like
in [