Random Graphs

Contents

• Introduction
• The PRISM Model
• Model Checking

Introduction

In this case study we investigate the likelihood that a pair of nodes are connected in a random graph. More precisely, we consider the set of random graphs G(n,p), i.e. the set of random graphs with n nodes where the probability of there being an edge between any two nodes equals p. We examine whether a graph G is ''1-2 connected'', i.e. whether there exists a path from node 1 to node 2.

The PRISM Model

To model this problem in PRISM we split the modelling into two stages. In the first stage, we (randomly) construct a graph from G(n,p). In the second stage, we find all nodes that can reach node 2, and hence find whether node 1 can reach node 2. More precisely, in the second stage, we find nodes that have a path to node 2 by searching for nodes for which one can reach (in one step) a node for which we have already found the existence of a path to node 2. Note that, because the above may hold for a set of nodes we make a non-deterministic choice as to which node we choose to consider first. Hence, the model is an MDP.

Below we give the PRISM code for in the case when n equals 4.

// checking for a path between nodes 1 and 2 for random graphs ($ nodes)
// gxn/dxp 12/11/04

mdp

const double p; // probability there exists an edge between two nodes

// program counter (decides which edge is set randomly next)
// note: the second modelling stage does not start until the program
// counter has reached its maximum value, i.e. the random graph has 
// been constructed
module PC
	
	pc : [0..12];
	
	[s12] pc=0 -> (pc'=pc+1);
	[s13] pc=1 -> (pc'=pc+1);
	[s14] pc=2 -> (pc'=pc+1);
	[s23] pc=3 -> (pc'=pc+1);
	[s24] pc=4 -> (pc'=pc+1);
	[s34] pc=5 -> (pc'=pc+1);
	
endmodule

// module for path between 1 and 2
module M12
	
	x12 : bool;
	
	// randomly decide if there exists an edge
	[s12] true -> p:(x12'=true)+(1-p):(x12'=false);
	// update if we can find a path to 2
	[] pc=6 & !x12 & (false | (x13 & x23) | (x14 & x24)) -> (x12'=true);
	
endmodule

// module for path between 1 and 3
module M13
	
	x13 : bool;
	
	// randomly decide if there exists an edge
	[s13] true -> p:(x13'=true)+(1-p):(x13'=false);
	
endmodule

// module for path between 1 and 4
module M14
	
	x14 : bool;
	
	// randomly decide if there exists an edge
	[s14] true -> p:(x14'=true)+(1-p):(x14'=false);
	
endmodule

// module for path between 2 and 3
module M23
	
	x23 : bool;
	
	// randomly decide if there exists an edge
	[s23] true -> p:(x23'=true)+(1-p):(x23'=false);
	// update if we can find a path to 2
	[] pc=6  & !x23 & (false | (x12 & x13) | (x24 & x34)) -> (x23'=true);
	
endmodule

// module for path between 3 and 4
module M24
	
	x24 : bool;
	
	// randomly decide if there exists an edge
	[s24] true -> p:(x24'=true)+(1-p):(x24'=false);
	// update if we can find a path to 2
	[] pc=6  & !x24 & (false | (x12 & x14) | (x23 & x34)) -> (x24'=true);
	
endmodule

// module for path between 3 and 4
module M34
	
	x34 : bool;
	
	// randomly decide if there exists an edge
	[s34] true -> p:(x34'=true)+(1-p):(x34'=false);
	
endmodule

The table below shows statistics for models we have built for random graphs with different numbers of nodes (different values of n). Note that these statistics are identical for all values of p, expect for the special cases when p equals 0, 0.5 or 1. The tables include:

• the number of states in the MDP representing the model;
• both the number of nodes and leaves of the MTBDD which represents the model;
• the construction time which equals the time taken for the system description to be parsed and converted to the MTBDD representing it, and the time to perform reachability, identify the non-reachable states and filter the MTBDD accordingly;
• the number of iterations required to find the reachable states (which is performed via a BDD based fixpoint algorithm).

n:		Model:		MTBDD:			Construction:
		States:		Nodes:	Leaves:		Time (s):	Iter.s:
2		3		18	4		0.063	2
3		15		86	4		0.071	4
4		127		291	4		0.098	7
5		2,047		732	4		0.120	11
6		65,535		1,629	4		0.149	16
7		194,303		3,664	4		0.284	22
8		536,870,911		8,234	4		0.455	29
9		137,438,953,471		19,079	4		0.915	37
10		70,368,744,177,663		32,119	4		2.52	46

Model Checking

To find the probability that the nodes 1 and 2 are connected we verify the property: Pmax=?[true U x12].

The following graph plots, for the cases when n=2,3,...,10, this probability as the value of p varies.

In addition, we have calculated the expected shortest path between 1 and 2. To treat the cases when the nodes 1 and 2 are not connected, we set the path length to be c when no path between 1 and 2 exists.

Each of the following graphs plot, for the cases when n=2,3,...,10, the expected shortest path between 1 and 2 as the value of p varies. The difference between the graphs is the value we assign c, that is the cost associated with a graph when the nodes 1 and 2 are not connected.

Site hosted at the Department of Computer Science, University of Oxford