Dining philosophers problem will serve as an explanatory example showing capabilities of the presented approach.

Many solutions to this problem can be found in the literature. The desired solution should not only solve the problem of deadlocks but also of a starvation. The proposed solutions can be easily modelled using place-transition Petri nets. If the reachability graph of the net is subjected to the translation to nuXmv code, it becomes possible to verify problems of starvation and deadlocks with properties of the system written as suitable LTL and CTL formulae.

One of the proposed solutions involves a condition that philosophers should take both forks at the same time. Thus, philosopher who raises forks can immediately begin to eat and the problem of deadlocks is eliminated. However, in order to verify these properties, appropriate Petri net was modelled. It is presented in the figure below.

Places p0 to p4 denote the fork usage. If a place has a token it means that the corresponding fork is free. If a token is absent, it means that a corresponding fork is taken. Firing of a transition between neighbour places (for example the transition t0 between places p0 and p1) denotes that both forks are being taken by a philosopher. Tokens in places p5 to p9 mean that the corresponding philosophers are in the process of eating.

To verify that the net resolves problems described above, coverability graph has been generated and exported to .kts file. A graphical representation of the graph is shown in the figure below.

The coverability graph should be analysed to check whether all the states corresponding to the eating of particular philosophers are reachable and whether the system does not include terminal states.

Using PetriNet2ModelChecker to translate coverability graph into description of the system in nuXmv code, the following file was generated:

MODULE main
VAR
	s: {s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10};
	p0 : boolean;
	p1 : boolean;
	p2 : boolean;
	p3 : boolean;
	p4 : boolean;
	p5 : boolean;
	p6 : boolean;
	p7 : boolean;
	p8 : boolean;
	p9 : boolean;
ASSIGN
	init(s) := s0;
	next(s) := case
		s = s0 : {s1, s2, s3, s4, s5};
		s = s1 : {s0, s6, s7};
		s = s2 : {s0, s8, s9};
		s = s3 : {s0, s6, s10};
		s = s4 : {s0, s7, s8};
		s = s5 : {s0, s9, s10};
		s = s6 : {s1, s3};
		s = s7 : {s1, s4};
		s = s8 : {s2, s4};
		s = s9 : {s2, s5};
		s = s10 : {s3, s5};
	esac;
	p0 := case
		s = s0 : TRUE;
		s = s2 : TRUE;
		s = s3 : TRUE;
		s = s4 : TRUE;
		s = s8 : TRUE;
		TRUE : FALSE;
	esac;
	p1 := case
		s = s0 : TRUE;
		s = s3 : TRUE;
		s = s4 : TRUE;
		s = s5 : TRUE;
		s = s10 : TRUE;
		TRUE : FALSE;
	esac;
	p2 := case
		s = s0 : TRUE;
		s = s1 : TRUE;
		s = s4 : TRUE;
		s = s5 : TRUE;
		s = s7 : TRUE;
		TRUE : FALSE;
	esac;
	p3 := case
		s = s0 : TRUE;
		s = s1 : TRUE;
		s = s2 : TRUE;
		s = s5 : TRUE;
		s = s9 : TRUE;
		TRUE : FALSE;
	esac;
	p4 := case
		s = s0 : TRUE;
		s = s1 : TRUE;
		s = s2 : TRUE;
		s = s3 : TRUE;
		s = s6 : TRUE;
		TRUE : FALSE;
	esac;
	p5 := case
		s = s1 : TRUE;
		s = s6 : TRUE;
		s = s7 : TRUE;
		TRUE : FALSE;
	esac;
	p6 := case
		s = s2 : TRUE;
		s = s8 : TRUE;
		s = s9 : TRUE;
		TRUE : FALSE;
	esac;
	p7 := case
		s = s3 : TRUE;
		s = s6 : TRUE;
		s = s10 : TRUE;
		TRUE : FALSE;
	esac;
	p8 := case
		s = s4 : TRUE;
		s = s7 : TRUE;
		s = s8 : TRUE;
		TRUE : FALSE;
	esac;
	p9 := case
		s = s5 : TRUE;
		s = s9 : TRUE;
		s = s10 : TRUE;
		TRUE : FALSE;
	esac;

For the present example, the following LTL and CTL formulae were prepared:

1. EF(p5), EF(p6), EF(p7), EF(p8), EF(p9) - Formula EF(p5) means that there is a path in which the first philosopher is in possession of both forks. Other formulas are similar but relate to other philosophers.
2. GF(p5), GF(p6), GF(p7), GF(p8), GF(p9) - Formula GF(p5) means that no matter what state of the system is reached, there will always be a next state in which the first philosopher will be in possession of both forks. This requirement means that the philosopher will always be able to eat again. Other formulae have similar meaning but refer to other philosophers.
3. G ( ( ¬(p0) ∧ ¬(p1) ∧ ¬(p2) ∧ ¬(p3) ∧ ¬(p4) ) —→ ( (p5) ∨ (p6) ∨ (p7) ∨ (p8) ∨ (p9) ) )

Go back