www.prismmodelchecker.org

Futures Market Investor

(McIver and Morgan)

Contents

Introduction:

This case study is based on an investor in a futures market; it is taken from [MM07, MM02], where it is used to explore the interaction of angelic, demonic and probabilistic choice in the context of a minimax-valued logic. This example can be considered as a two player game where one player (the investor) tries to maximize his or her return against the other player (the futures market) which attempts to minimize this return.

The Investor (I) has been given the right to make an investment in `futures': a fixed number of shares in a specific company that he can reserve on the first day of any month he chooses. Exactly one month later, the shares will be delivered and will collectively have a market value on that day — he or she can then sell the shares. The investors problem is to decide when to make the reservation so that the subsequent sale has maximum value. If the investor never reserves, then his or her return is zero.

The futures market (M) has the following structure:

  1. The market value v of the shares is a whole number of pounds between £0 and £10 inclusive; it has a probability p of going up by £1 in any month, and 1-p of going down by £1 — but it remains within those bounds. The probability p represents short-term market uncertainty.
  2. The probability p itself varies month-by-month in steps of 0.1 between zero and one: when v is less than £5 the probability that p will rise is 2/3; when v is more than £5 the probability of p's falling is 2/3; and when v is £5 exactly the probability is 1/2 of going either way. The movement of p represents investors' knowledge of long-term `cyclic second-order' trends.
  3. There is a cap c on the value of v, initially £10, which has probability 1/2 of falling by £1 in any month; otherwise it remains where it is. The `falling cap' models the fact that the company is in a slow decline.
  4. If in a given month the investor does not reserve, then at the very next month the market can temporarily bar the investor from reserving. But the market cannot bar the investor in two consecutive months.

The Model

The situation of the game can be summed up as follows:

  • During each month there are three probabilistic transitions that occur: the share value v rises or falls, according to p; probability p itself rises or falls, according to long-term trends; and the capped value c of the stock either falls or stays the same. The compounded effect of these choices determine a transition representing one month's stock market activity.
  • At the beginning of each month, the investor makes a maximising choice of whether to reserve; but, if he does not, then
  • At the beginning of the next month, the market makes a minimising choice of whether to bar the investor or not.

Graphically, the behaviour of the model is given by the transition system below.

behaviour of the system

Modelling the system in PRISM

Below we give the PRISM code for this model. The model has 6,688 states and in PRISM it takes 0.169 seconds to construct this model.

// EXAMPLE: INVESTING IN THE FUTURES MARKET
// (McIver and Morgan 03)

mdp

// module use to synchronize transitions
module month
    
    m : [0..1];

    [invest] (m=0) -> (m'=1); // transitions made at the start of the month synchronize on 'invest'
    [month] (m=1) -> (m'=0); // transitions made during the month synchronize on 'month'
    [done] (m=0) -> (m'=0); // once investor has cashed in shares nothing changes

endmodule

// the investor
module investor
    
    i : [0..1]; // i=0 no reservation and i=1 made reservation

    [invest] (i=0) -> (i'=0); // do nothing
    [invest] (i=0) -> (i'=1); // make reservation
    [invest] (i=1) & (b=1) -> (i'=0); // barred previous month: try again and do nothing
    [invest] (i=1) & (b=1) -> (i'=1); // barred previous month: make reservation
    [done] (i=1) & (b=0) -> (i'=1); // cash in shares (not barred)

endmodule

// bar on the investor
module barred
    
    b : [0..1] init 1; // initially cannot bar
    // b=0 - not barred and b=1 - barred

    [invest] true  -> (b'=0); // do not bar this month
    [invest] (b=0) -> (b'=1); // bar this month (cannot have barred the previous month) 

endmodule

// value of the shares
module value
    
    v : [0..10] init 10;

    [month] true -> p/10 : (v'=min(v+1,c)) + (1-p/10) : (v'=min(max(v-1,0),c));

endmodule

// probability of shares going up/down
module probability
    
    p : [0..10] init 5; // probabilitity is p/10 and initially the probability is 1/2

    [month] (v<5) -> 2/3 : (p'=min(p+1,10)) + 1/3 : (p'=max(p-1,0));
    [month] (v=5) -> 1/2 : (p'=min(p+1,10)) + 1/2 : (p'=max(p-1,0));
    [month] (v>5) -> 1/3 : (p'=min(p+1,10)) + 2/3 : (p'=max(p-1,0));

endmodule

// cap on the value of the shares
module cap
    
    c : [0..10] init 10; // cap on the shares

    [month] true -> 1/2 : (c'=max(c-1,0)) + 1/2 : (c'=c); // probability 1/2 the cap decreases

endmodule
View: printable version          Download: investor.nm

Value of the Game

Using the game interpretation, we can generate a probabilistic tree from the transition system above by duplicating nodes with multiple incoming arcs, `unfolding' back-loops, and making minimising or maximising choices as they are encountered. In this example, at each unfolding both the investor I (making choices as to whether to invest) and the stock market M (making choices whether to impose a bar) need to choose between two ongoing branches — and their choice could be different each time they revisit their respective decision points. Each of I and M will be using a strategy.

For example, the investor I's strategy (maximising, he or she hopes) for dealing with the falling cap might be: wait until the share value v (rising) meets the cap c (falling), and then reserve. Waiting for v to rise is a good idea, but when it has met the cap c there is clearly no point in waiting further. We call this strategy I's `seat-of-the-pants' strategy.

On the other hand, M's strategy (minimising, the investor fears) might be: bar the investor, if possible, whenever the shares' probability p of rising exceeds 1/2.

As is usual in game theory, when the actual strategies of the two players are unknown, we define the value of the game to be the the minimax over all strategy sequences of the expected payoff — but it is well-defined only when it is the same as the maximin. From the results presented in [MM07] the game's value is indeed well-defined.

We have used both Mathematica and PRISM in conjunction with Matlab for this calculation. The scripts are available online from here and further details are available in [MM07].

For example, if p is initially 0.5 and the cap c is 10, then the optimal expected sale-value for the investor is given in the table below. In the table we also include the results when the investor follows the `seat-of-the-pants' strategy given above.

initial share value:   expected sale price:
optimal strategy `seat-of-the-pants' strategy
0 4.163.68
1 4.303.79
2 4.553.97
3 4.884.17
4 5.244.29
5 5.524.17
6 6.004.16
7 7.004.65
8 8.005.61
9 9.006.78
109.509.50

We see that, even when the share value is only `moderately high', there is nothing to be gained by waiting, since the cap is likely to drop. For low initial values, however, some benefit can be gained by delaying the reservation for a while. Furthermore, by following the `seat-of-the-pants' strategy we see a significantly lower expected return against `worst-case' play by M. From this we might guess that when v is at least £6 it is better to `reserve now' than to follow the `seat-of-the-pants' strategy and wait.

Due to the simple structure of this game, using theorems presented in [MM97, MM04], the strategy which actually achieves the optimal return states that the investor should follow the following strategy: make an immediate reservation just when the expected value of the stock in one month's time is at least as great as the expected value of the whole game played from this point; otherwise wait.

Verification with PRISM

By replacing the non-deterministic choices of the market as to whether to bar or not with a probabilistic choice we reach a situation where the investor is trying to maximize his or her return against a purely probabilistic market. For such a game we can use PRISM directly to calculate the optimal reward of the investor.

In the table and graph below we give the optimal return of the investor (in the case when p is initially 0.5 and the cap c is 10) as the probability of the market choosing to bar and the initial value of v varies.

initial share value:   maximum expected sale price:
probability of choosing to bar
00.10.20.30.40.50.60.70.80.91
0 4.574.504.474.454.434.414.394.374.364.354.34
1 4.674.634.614.584.564.544.524.514.504.484.47
2 4.914.884.854.824.804.784.774.754.744.734.73
3 5.225.195.165.145.125.105.085.075.065.055.04
4 5.535.495.475.455.435.415.405.395.385.385.37
5 5.805.775.755.735.715.705.685.675.665.655.64
6 6.226.196.176.156.136.116.106.086.076.066.05
7 7.027.007.007.007.007.007.007.007.007.007.00
8 8.008.008.008.008.008.008.008.008.008.008.00
9 9.009.009.009.009.009.009.009.009.009.009.00
109.509.509.509.509.509.509.509.509.509.509.50

graphical representation of results

The results demonstrate that, as the probability of the market barring the investor increases, the return of the investor decreases. This is to be expected since as this probability increases the choices the investor has available decrease (there is more chance of the investor being barred in a month).

Case Studies