www.prismmodelchecker.org

Human-in-the-Loop UAV Mission Planning

[work with Lu Feng, Laura Humphrey and Ufuk Topcu]

Contents

Related publications: [FWHT15]

Introduction

This case study is based on [FWHT15] and considers the control of an unmanned aerial vehicle (UAV) that is interacting with a human operator. The models capture a simple scenario involving road network surveillance by a UAV. Depending on the type (i.e., probabilistic and/or nondeterministic) of knowledge about the uncertainties and imperfections in the human-automation interactions, we use abstractions based on Markov decision processes and augment these models to stochastic two-player games. We synthesize optimal UAV control protocols using both PRISM (for MDP models) and PRISM-games (for game models).

The following figure shows a map of the road network considered in this case study, which has six surveillance waypoints labeled w1, w2, ..., w6. Approaching a waypoint from certain angles may be better than others, e.g., in order to obtain desired look angles on a waypoint target using an ellipsoidal loiter pattern. Angles of approach are thus discretized into eight angle points around each waypoint. Roads connecting waypoints are discretized into road points r1, r2, ..., r9. Red polygons represent “restricted operating zones” (ROZs), areas in which flying the UAV may be dangerous or lead to a higher chance of being detected by an adversary.

A road network for UAV missions

We assume the UAV has a certain degree of autonomy that is used to fulfill most of the piloting functions, e.g., maintaining loiter patterns around waypoints, selecting most of the points that comprise the route, and flying the route. The human operator primarily performs sensor tasks, e.g., steering the onboard sensor to capture imagery of targets at waypoints. However, the operator retains the ability to affect some of the piloting functions of the UAV. The operator decides how many loiters to perform at each waypoint, since more loiters may be needed if the operator is not satisfied with the sensor imagery obtained on previous loiters.

The optimal UAV piloting plan depends on mission objectives (e.g., safety, reachability, coverage) and operator characteristics (e.g., workload, proficiency, and fatigue). The concrete UAV mission objectives we consider in this case study include surveillance of the whole road network with minimum fuel consumption, or flying to certain waypoints while trying to avoid ROZs. We investigate the effects of operator characteristics on UAV mission performance, and the trade-offs between multiple mission objectives.

MDP Models

We model the operator-UAV interaction as a Markov decision process (MDP). The operator's accuracy of performing sensor image analysis varies at different workload levels, represented by accu_load1 (for the low workload) and accu_load2 (for the high workload). Moreover, due to operator fatigue, the accuracy would be discounted by a factor of fd, after the operator analyzes certain number of images (COUNTER). The operator may also choose which road to go at certain checkpoint (e.g., w2 and w6) following a certain probability distribution. The UAV model encodes all the possible routes shown in the road network map. We assume that the UAV may fly in or out of a waypoint via any angle (with a uniform distribution).

The MDP model for the operator-UAV interaction is shown below.

mdp

// operator parameters
const double p=0.5; // probability of increasing workload due to other uncertain tasks
const double accu_load1; // accuracy at the low workload level (real numbers between 0 and 1)
const double accu_load2; // accuracy at the high workload level (real numbers between 0 and 1)
const double fd; // accuracy discount due to fatigue (real numbers between 0 and 1)
const int COUNTER; // fatigue threshold (integers, e.g, 10)
const double risky2; // at w2: probability of choosing a risky route
const double risky6; // at w6: probability of choosing a risky route

global stop : bool init false; // done visiting all waypoints
formula roz = (r=8) | (w=3&a=1) | (w=3&a=2) | (w=5&a=2); // restricted operating zones


// OPERATOR MODEL
module operator
	
	k:[0..100] init 0; // fatigue level measured by completetd tasks
	t:[0..2] init 0; // workload level
	s:[0..2] init 0; // status of image processing, 0: init, 1: good, 2: bad
	c:[0..3] init 0; // choices at the check point

	// image processing, the workload may increase due to other unknown tasks
	[image] !stop & t=0 & s=0 -> (1-p):(t'=1) & (s'=0) + p:(t'=2) & (s'=0);
	// not fatigue, workload level 1
	[process] !stop & t=1 & s=0 & k<=COUNTER -> accu_load1:(s'=1)&(k'=k+1) + (1-accu_load1):(s'=2)&(k'=k+1);
	// fatigue, workload level 1
	[process] !stop & t=1 & s=0 & k>COUNTER -> accu_load1*fd:(s'=1) + (1-accu_load1*fd):(s'=2);
	// not fatigue, workload level 2
	[process] !stop & t=2 & s=0 & k<=COUNTER -> accu_load2:(s'=1)&(k'=k+1) + (1-accu_load2):(s'=2)&(k'=k+1);
	// fatigue, workload level 2
	[process] !stop & t=2 & s=0 & k>COUNTER -> accu_load2*fd:(s'=1) + (1-accu_load2*fd):(s'=2);

	// image analysis is bad, UAV need to wait at the waypoint and take another image
	[wait] !stop & s=2 -> (t'=0) & (s'=0); 

	// if image analysis is good, UAV can continue flying 
	// at check points, operator may suggest route for the UAV

	// w2 -> r5 (c=0) |r6 (c=1) |r7 (c=2)|r9 (c=3)
	[go] !stop & s=1 & w=2 -> risky2:(c'=2) & (t'=0) & (s'=0) + (1-risky2)/3:(c'=3) & (t'=0) & (s'=0)
			+(1-risky2)/3:(c'=1) & (t'=0) & (s'=0) + (1-risky2)/3:(c'=0) & (t'=0) & (s'=0);
	
	// w5 -> r3 (c=0)| r4  (c=1)| w4 (c=2)
	[go] !stop & s=1 & w=5 -> 1/3:(c'=2) & (t'=0) & (s'=0) + 1/3:(c'=1) & (t'=0) & (s'=0) 
			+ 1/3:(c'=0) & (t'=0) & (s'=0);
	
	// w6 -> r2 (c=0)| r3 (c=1) |r8 (c=2)
	[go] !stop & s=1 & w=6 -> risky6:(c'=2) & (t'=0) & (s'=0) + (1-risky6)/2:(c'=1) & (t'=0) & (s'=0)
			+ (1-risky6)/2:(c'=0) & (t'=0) & (s'=0);

	// at non-check-points, UAV has full autonomy to choose flying route
	[go] !stop & s=1 & (w!=2 & w!=5 & w!=6) -> (t'=0) & (s'=0); 

	// operator stops
	[] !stop & w1 & w2 & w6 -> (stop'=true);
	[operator_stop] stop -> true;

endmodule


// UAV MODEL
module UAV
	// UAV positions:
	// inside a waypoint: w!=0, a=0, r=0
	// fly through certain angle of a waypoint: w!=0, a!=0, r=0
	// fly through a road point: w=0, a=0, r!=0
	w:[0..6] init 1; // waypoint 
	a:[0..8] init 0; // angle points
	r:[0..9] init 0; // road points
        send: bool init true;
	in: bool init true;
	// flag that a waypoint has been visited
	w1: bool init true;
	w2: bool init false;
	w3: bool init false;
	w4: bool init false;
	w5: bool init false;
	w6: bool init false;
	
	// at any waypoint:
	// send image to human operator for analysis
	[image] w!=0 & a=0 & r=0 & send -> (send'=false); 
	// wait at the waypoint and send another image
	[wait] !send -> (send'=true);
	// fly into a waypoint and take an image
	[camera] w=1 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w1'=true);
	[camera] w=2 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w2'=true);
	[camera] w=3 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w3'=true);
	[camera] w=4 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w4'=true);
	[camera] w=5 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w5'=true);
	[camera] w=6 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w6'=true);
	// fly out of the waypoint via any angle point
	[go] w!=0 & a=0 & r=0 -> 1/8:(a'=1) & (in'=false) 
			       + 1/8:(a'=2) & (in'=false)
		               + 1/8:(a'=3) & (in'=false) 
		               + 1/8:(a'=4) & (in'=false)
			       + 1/8:(a'=5) & (in'=false) 
		               + 1/8:(a'=6) & (in'=false)
	                       + 1/8:(a'=7) & (in'=false) 
			       + 1/8:(a'=8) & (in'=false);


	// UAV flying plans (based on the road map)
	// check points: receiving commands from the operator
	// w2 -> r5 |r6 |r7 |r9
	[fly] c=0 & w=2 & (a!=0) & r=0 & !in -> (r'=5);
	[fly] c=1 & w=2 & (a!=0) & r=0 & !in -> (r'=6);
	[fly] c=2 & w=2 & (a!=0) & r=0 & !in -> (r'=7);
	[fly] c=3 & w=2 & (a!=0) & r=0 & !in -> (r'=9);
	// w5 -> r3 | r4 | w4 (at any angle point)
	[fly] c=0 & w=5 & (a!=0) & r=0 & !in -> (r'=3);
	[fly] c=1 & w=5 & (a!=0) & r=0 & !in -> (r'=4);
	[fly] c=2 & w=5 & (a!=0) & r=0 & !in -> 1/8:(w'=4) & (a'=1) & (r'=0) & (in'=true)
					   + 1/8:(w'=4) & (a'=2) & (r'=0) & (in'=true)
					   + 1/8:(w'=4) & (a'=3) & (r'=0) & (in'=true)
					   + 1/8:(w'=4) & (a'=4) & (r'=0) & (in'=true)
					   + 1/8:(w'=4) & (a'=5) & (r'=0) & (in'=true)
					   + 1/8:(w'=4) & (a'=6) & (r'=0) & (in'=true)
					   + 1/8:(w'=4) & (a'=7) & (r'=0) & (in'=true)
					   + 1/8:(w'=4) & (a'=8) & (r'=0) & (in'=true);
	// w6 -> r2 | r3 |r8
	[fly] c=0 & w=6 & (a!=0) & r=0 & !in -> (r'=2);
	[fly] c=1 & w=6 & (a!=0) & r=0 & !in -> (r'=3);
	[fly] c=2 & w=6 & (a!=0) & r=0 & !in -> (r'=8);

	// non check points: fly autonomy
	// w1 -> r1 | r9
	[fly] w=1 & (a!=0) & r=0 & !in -> (r'=1);
	[fly] w=1 & (a!=0) & r=0 & !in -> (r'=9);
	// w3 -> r6 | w4 (any angle point)
	[fly] w=3 & (a!=0) & r=0 & !in -> (r'=6);
	[fly] w=3 & (a!=0) & r=0 & !in -> 1/8:(w'=4) & (a'=1) & (r'=0) & (in'=true)
				     + 1/8:(w'=4) & (a'=2) & (r'=0) & (in'=true)
				     + 1/8:(w'=4) & (a'=3) & (r'=0) & (in'=true)
			             + 1/8:(w'=4) & (a'=4) & (r'=0) & (in'=true)
			             + 1/8:(w'=4) & (a'=5) & (r'=0) & (in'=true)
				     + 1/8:(w'=4) & (a'=6) & (r'=0) & (in'=true)
				     + 1/8:(w'=4) & (a'=7) & (r'=0) & (in'=true)
			             + 1/8:(w'=4) & (a'=8) & (r'=0) & (in'=true);

	// w4 -> w3 | w5
	[fly] w=4 & (a!=0) & r=0 & !in -> 1/8:(w'=3) & (a'=1) & (r'=0) & (in'=true)
				     + 1/8:(w'=3) & (a'=2) & (r'=0) & (in'=true)
				     + 1/8:(w'=3) & (a'=3) & (r'=0) & (in'=true)
			             + 1/8:(w'=3) & (a'=4) & (r'=0) & (in'=true)
			             + 1/8:(w'=3) & (a'=5) & (r'=0) & (in'=true)
				     + 1/8:(w'=3) & (a'=6) & (r'=0) & (in'=true)
				     + 1/8:(w'=3) & (a'=7) & (r'=0) & (in'=true)
			             + 1/8:(w'=3) & (a'=8) & (r'=0) & (in'=true);

	[fly] w=4 & (a!=0) & r=0 & !in -> 1/8:(w'=5) & (a'=1) & (r'=0) & (in'=true)
				     + 1/8:(w'=5) & (a'=2) & (r'=0) & (in'=true)
				     + 1/8:(w'=5) & (a'=3) & (r'=0) & (in'=true)
			             + 1/8:(w'=5) & (a'=4) & (r'=0) & (in'=true)
			             + 1/8:(w'=5) & (a'=5) & (r'=0) & (in'=true)
				     + 1/8:(w'=5) & (a'=6) & (r'=0) & (in'=true)
				     + 1/8:(w'=5) & (a'=7) & (r'=0) & (in'=true)
			             + 1/8:(w'=5) & (a'=8) & (r'=0) & (in'=true);
	// r1 -> r2 | w1
	[fly] r=1 -> (r'=2);
	[fly] r=1 -> 1/8:(w'=1) & (a'=1) & (r'=0) & (in'=true)
		+ 1/8:(w'=1) & (a'=2) & (r'=0) & (in'=true)
		+ 1/8:(w'=1) & (a'=3) & (r'=0) & (in'=true)
		+ 1/8:(w'=1) & (a'=4) & (r'=0) & (in'=true)
		+ 1/8:(w'=1) & (a'=5) & (r'=0) & (in'=true)
		+ 1/8:(w'=1) & (a'=6) & (r'=0) & (in'=true)
		+ 1/8:(w'=1) & (a'=7) & (r'=0) & (in'=true)
		+ 1/8:(w'=1) & (a'=8) & (r'=0) & (in'=true);
	// r2 -> r1 | w6
	[fly] r=2 -> (r'=1);
	[fly] r=2 -> 1/8:(w'=6) & (a'=1) & (r'=0) & (in'=true)
		+ 1/8:(w'=6) & (a'=2) & (r'=0) & (in'=true)
		+ 1/8:(w'=6) & (a'=3) & (r'=0) & (in'=true)
		+ 1/8:(w'=6) & (a'=4) & (r'=0) & (in'=true)
		+ 1/8:(w'=6) & (a'=5) & (r'=0) & (in'=true)
		+ 1/8:(w'=6) & (a'=6) & (r'=0) & (in'=true)
		+ 1/8:(w'=6) & (a'=7) & (r'=0) & (in'=true)
		+ 1/8:(w'=6) & (a'=8) & (r'=0) & (in'=true);
	// r3 -> w5 | w6
	[fly] r=3 -> 1/8:(w'=5) & (a'=1) & (r'=0) & (in'=true)
		+ 1/8:(w'=5) & (a'=2) & (r'=0) & (in'=true)
		+ 1/8:(w'=5) & (a'=3) & (r'=0) & (in'=true)
		+ 1/8:(w'=5) & (a'=4) & (r'=0) & (in'=true)
		+ 1/8:(w'=5) & (a'=5) & (r'=0) & (in'=true)
		+ 1/8:(w'=5) & (a'=6) & (r'=0) & (in'=true)
		+ 1/8:(w'=5) & (a'=7) & (r'=0) & (in'=true)
		+ 1/8:(w'=5) & (a'=8) & (r'=0) & (in'=true);

	[fly] r=3 -> 1/8:(w'=6) & (a'=1) & (r'=0) & (in'=true)
		+ 1/8:(w'=6) & (a'=2) & (r'=0) & (in'=true)
		+ 1/8:(w'=6) & (a'=3) & (r'=0) & (in'=true)
		+ 1/8:(w'=6) & (a'=4) & (r'=0) & (in'=true)
		+ 1/8:(w'=6) & (a'=5) & (r'=0) & (in'=true)
		+ 1/8:(w'=6) & (a'=6) & (r'=0) & (in'=true)
		+ 1/8:(w'=6) & (a'=7) & (r'=0) & (in'=true)
		+ 1/8:(w'=6) & (a'=8) & (r'=0) & (in'=true);
	// r4 -> r5 | w5
	[fly] r=4 -> (r'=5);
	[fly] r=4 -> 1/8:(w'=5) & (a'=1) & (r'=0) & (in'=true)
		+ 1/8:(w'=5) & (a'=2) & (r'=0) & (in'=true)
		+ 1/8:(w'=5) & (a'=3) & (r'=0) & (in'=true)
		+ 1/8:(w'=5) & (a'=4) & (r'=0) & (in'=true)
		+ 1/8:(w'=5) & (a'=5) & (r'=0) & (in'=true)
		+ 1/8:(w'=5) & (a'=6) & (r'=0) & (in'=true)
		+ 1/8:(w'=5) & (a'=7) & (r'=0) & (in'=true)
		+ 1/8:(w'=5) & (a'=8) & (r'=0) & (in'=true);
	// r5 -> r4 | w2
	[fly] r=5 -> (r'=4);
	[fly] r=5 -> 1/8:(w'=2) & (a'=1) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=2) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=3) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=4) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=5) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=6) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=7) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=8) & (r'=0) & (in'=true);
	// r6 -> w2 | w3
	[fly] r=6 -> 1/8:(w'=2) & (a'=1) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=2) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=3) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=4) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=5) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=6) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=7) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=8) & (r'=0) & (in'=true);

	[fly] r=6 -> 1/8:(w'=3) & (a'=1) & (r'=0) & (in'=true)
		+ 1/8:(w'=3) & (a'=2) & (r'=0) & (in'=true)
		+ 1/8:(w'=3) & (a'=3) & (r'=0) & (in'=true)
		+ 1/8:(w'=3) & (a'=4) & (r'=0) & (in'=true)
		+ 1/8:(w'=3) & (a'=5) & (r'=0) & (in'=true)
		+ 1/8:(w'=3) & (a'=6) & (r'=0) & (in'=true)
		+ 1/8:(w'=3) & (a'=7) & (r'=0) & (in'=true)
		+ 1/8:(w'=3) & (a'=8) & (r'=0) & (in'=true);
	// r7 -> w2 | r8
	[fly] r=7 -> 1/8:(w'=2) & (a'=1) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=2) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=3) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=4) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=5) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=6) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=7) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=8) & (r'=0) & (in'=true);
	[fly] r=7 -> (r'=8);
	// r8 -> w6 | r7
	[fly] r=8 -> 1/8:(w'=6) & (a'=1) & (r'=0) & (in'=true)
		+ 1/8:(w'=6) & (a'=2) & (r'=0) & (in'=true)
		+ 1/8:(w'=6) & (a'=3) & (r'=0) & (in'=true)
		+ 1/8:(w'=6) & (a'=4) & (r'=0) & (in'=true)
		+ 1/8:(w'=6) & (a'=5) & (r'=0) & (in'=true)
		+ 1/8:(w'=6) & (a'=6) & (r'=0) & (in'=true)
		+ 1/8:(w'=6) & (a'=7) & (r'=0) & (in'=true)
		+ 1/8:(w'=6) & (a'=8) & (r'=0) & (in'=true);
	[fly] r=8 -> (r'=7);
	// r9 -> w1 | w2
	[fly] r=9 -> 1/8:(w'=1) & (a'=1) & (r'=0) & (in'=true)
		+ 1/8:(w'=1) & (a'=2) & (r'=0) & (in'=true)
		+ 1/8:(w'=1) & (a'=3) & (r'=0) & (in'=true)
		+ 1/8:(w'=1) & (a'=4) & (r'=0) & (in'=true)
		+ 1/8:(w'=1) & (a'=5) & (r'=0) & (in'=true)
		+ 1/8:(w'=1) & (a'=6) & (r'=0) & (in'=true)
		+ 1/8:(w'=1) & (a'=7) & (r'=0) & (in'=true)
		+ 1/8:(w'=1) & (a'=8) & (r'=0) & (in'=true);

	[fly] r=9 -> 1/8:(w'=2) & (a'=1) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=2) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=3) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=4) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=5) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=6) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=7) & (r'=0) & (in'=true)
		+ 1/8:(w'=2) & (a'=8) & (r'=0) & (in'=true);

endmodule


rewards "time" // flight time
        [wait] true: 10;
        [fly] true: 60;
endrewards

rewards "ROZ" // ROZ occupancy
	[fly] roz : 1;
endrewards
View: printable version          Download: uav-mdp.nm

To compute the expected time of completing the mission (e.g., covering waypoints w1, w2 and w6), we use the PRISM property:

R{"time"}min=? [ F w1&w2&w6 ]

We can also study the Pareto curve of two mission objectives (e.g., minimising the expected mission completion time vs. minimising ROZ visits) to analyze their trade-offs, using the multi-objective query:

multi(R{"time"}min=? [ C ], R{"ROZ"}min=? [ C ])

An example of the results from the latter query is shown below, where L and H refer to the probabilities of capturing good quality imagery when operating at low and high workload levels, respectively. See [FWHT15] for more details.

Pareto curve: minimising the expected mission completion time vs. minimising ROZ visits

Stochastic Game Models

In the MDP models, we assume that the operator picks a road at each checkpoint for the UAV with some predefined probability distribution. In reality, however, it may be difficult to obtain and enforce such a distribution. We augment the MDP models as two-play stochastic games, in which we do not assume any distribution and allow the operator to choose any road/angle points nondeterministically. At each checkpoint, with certain delegation probability del, the operator delegates the UAV automation the task of picking the next road; otherwise, the route would be decided by the operator.

The stochastic game model for the operator-UAV interaction is shown below.

smg

// operator parameters
const double p=0.5; // probability of increasing workload due to other uncertain tasks
const double accu_load1; // accuracy at workload level 1 (low)
const double accu_load2; // accuracy at workload level 2 (high)
const double fd; // accuracy discount due to fatigue
const int COUNTER; // fatigue threshold
const double del; // probability of operator to delegate

// uav variables
global stop : bool init false; // done visiting all waypoints
global c:[0..3] init 0; // choices at the check point
formula roz = (r=8) | (w=3&a=1) | (w=3&a=2) | (w=5&a=2); // restricted operating zones

//players
global pl : [1..2] init 1; // 1 ... UAV, 2 ... operator
player p1
	UAV, [camera], [fly], [delegated], [uav_stop]
endplayer

player p2
	operator, [image], [process], [wait], [delegate], [prescribe], [operator_stop]
endplayer

// OPERATOR MODEL
module operator
	k:[0..100] init 0; // fatigue level measured by completed tasks
	t:[0..2] init 0; // workload level
	s:[0..2] init 0; // status of image processing, 0: init, 1: good, 2: bad
	q:[0..2] init 2; // delegation status: don't care if 2, delegation if 0, no delegation if 1

	// image processing, the workload may increase due to other unknown tasks
	[image] !stop & t=0 & s=0 -> (1-p):(t'=1) & (s'=0) + p:(t'=2) & (s'=0);
	// not fatigue, workload level 1
	[process] !stop & pl=2 & t=1 & s=0 & k<=COUNTER -> accu_load1:(s'=1)&(k'=k+1) + (1-accu_load1):(s'=2)&(k'=k+1);
	// fatigue, workload level 1
	[process] !stop & pl=2 & t=1 & s=0 & k>COUNTER -> accu_load1*fd:(s'=1) + (1-accu_load1*fd):(s'=2);
	// not fatigue, workload level 2
	[process] !stop & pl=2 & t=2 & s=0 & k<=COUNTER -> accu_load2:(s'=1)&(k'=k+1) + (1-accu_load2):(s'=2)&(k'=k+1);
	// fatigue, workload level 2
	[process] !stop & pl=2 & t=2 & s=0 & k>COUNTER -> accu_load2*fd:(s'=1) + (1-accu_load2*fd):(s'=1);

	// image analysis is bad, UAV needs to wait at the waypoint and take another image
	[wait] !stop & pl=2 & s=2 -> (pl'=1) & (t'=0) & (s'=0); 

	// if image analysis is good, UAV can continue flying 
	// at check points, operator may suggest route for the UAV

	// with probability del, the operator delegates the decision of the next cornerpoint to the UAV,
	[] !stop & pl=2 & s=1 & (w=2 | w=5 | w=6) & (q=2) -> del : (q'=0) + (1-del) : (q'=1);

	[delegate] !stop & pl=2 & s=1 & (w=2 | w=5 | w=6) & (q=0) -> (pl'=1) & (t'=0) & (s'=0) & (q'=2); // allow UAV to choose

	// w2 -> r5 (c=0) |r6 (c=1) |r7 (c=2)|r9 (c=3)
	[prescribe] !stop & pl=2 & s=1 & w=2 & (q=1) -> (pl'=1) & (c'=3) & (t'=0) & (s'=0)& (q'=2);
	[prescribe] !stop & pl=2 & s=1 & w=2 & (q=1) -> (pl'=1) & (c'=2) & (t'=0) & (s'=0)& (q'=2);
	[prescribe] !stop & pl=2 & s=1 & w=2 & (q=1)-> (pl'=1) & (c'=1) & (t'=0) & (s'=0)& (q'=2);
	[prescribe] !stop & pl=2 & s=1 & w=2 & (q=1)-> (pl'=1) & (c'=0) & (t'=0) & (s'=0)& (q'=2);

	// w5 -> r3 (c=0)| r4  (c=1)| w4 (c=2)
	[prescribe] !stop & pl=2 & s=1 & w=5 & (q=1)-> (pl'=1) & (c'=2) & (t'=0) & (s'=0)& (q'=2);
	[prescribe] !stop & pl=2 & s=1 & w=5 & (q=1)-> (pl'=1) & (c'=1) & (t'=0) & (s'=0)& (q'=2);
	[prescribe] !stop & pl=2 & s=1 & w=5 & (q=1)-> (pl'=1) & (c'=0) & (t'=0) & (s'=0)& (q'=2);

	// w6 -> r2 (c=0)| r3 (c=1) |r8 (c=2)
	[prescribe] !stop & pl=2 & s=1 & w=6 & (q=1)-> (pl'=1) & (c'=2) & (t'=0) & (s'=0)& (q'=2);
 	[prescribe] !stop & pl=2 & s=1 & w=6 & (q=1)-> (pl'=1) & (c'=1) & (t'=0) & (s'=0)& (q'=2);
	[prescribe] !stop & pl=2 & s=1 & w=6 & (q=1)-> (pl'=1) & (c'=0) & (t'=0) & (s'=0)& (q'=2);

	// at non-check-points, UAV has full autonomy to choose flying route
	[delegate] !stop & pl=2 & s=1 & (w!=2 & w!=5 & w!=6) -> (pl'=1) & (t'=0) & (s'=0); 
	
	// operator stops
	[operator_stop] stop & pl=2 -> true;

endmodule

// UAV MODEL
module UAV
	// UAV positions:
	// inside a waypoint: w!=0, a=0, r=0
	// fly through certain angle of a waypoint: w!=0, a!=0, r=0
	// fly through a road point: w=0, a=0, r!=0
	w:[0..6] init 1; // waypoint 
	r:[0..9] init 0; // road points
        send: bool init true;
	in: bool init true;
	// flag which waypoints were visited
	w1: bool init true;
	w2: bool init false;
	w3: bool init false;
	w4: bool init false;
	w5: bool init false;
	w6: bool init false;
	// if operator delegated decision at checkpoint
	delegated: bool init false;
	
	// at any waypoint:
	// send image to operator for analysis
	[image] pl=1 & w!=0 & a=0 & r=0 & send -> (pl'=2) & (send'=false); 
	// wait at the waypoint and send another image
	[wait] !send -> (send'=true);
	// fly into a waypoint and take an image
	// also, if done is true, then reset the waypoints
	[camera] pl=1 & w=1 & a!=0 & r=0 & in & !delegated -> (send'=true) & (w1'=true);
	[camera] pl=1 & w=2 & a!=0 & r=0 & in & !delegated -> (send'=true) & (w2'=true);
	[camera] pl=1 & w=3 & a!=0 & r=0 & in & !delegated -> (send'=true) & (w3'=true);
	[camera] pl=1 & w=4 & a!=0 & r=0 & in & !delegated -> (send'=true) & (w4'=true);
	[camera] pl=1 & w=5 & a!=0 & r=0 & in & !delegated -> (send'=true) & (w5'=true);
	[camera] pl=1 & w=6 & a!=0 & r=0 & in & !delegated -> (send'=true) & (w6'=true);
	// fly out of the waypoint via any angle point
	[prescribe] w!=0 & a=0 & r=0 -> (in'=false);
	[delegate] w!=0 & a=0 & r=0 & (w=2 | w=5 | w=6) -> (delegated'=true);
	[delegate] w!=0 & a=0 & r=0 & !(w=2 | w=5 | w=6) -> (in'=false);
	// UAV flying plans (based on the road map)
	// check points: receiving commands from the operator
	// w2 -> r5 |r6 |r7 |r9
	[delegated] pl=1 & w=2 & a!=0 & r=0 & delegated=true -> (in'=false) & (c'=0) & (delegated'=false);
	[delegated] pl=1 & w=2 & a!=0 & r=0 & delegated=true -> (in'=false) & (c'=1) & (delegated'=false);
	[delegated] pl=1 & w=2 & a!=0 & r=0 & delegated=true -> (in'=false) & (c'=2) & (delegated'=false);
	[delegated] pl=1 & w=2 & a!=0 & r=0 & delegated=true -> (in'=false) & (c'=3) & (delegated'=false);
	[fly] pl=1 & c=0 & w=2 & (a!=0) & r=0 & !in -> (r'=5);
	[fly] pl=1 & c=1 & w=2 & (a!=0) & r=0 & !in -> (r'=6);
	[fly] pl=1 & c=2 & w=2 & (a!=0) & r=0 & !in -> (r'=7);
	[fly] pl=1 & c=3 & w=2 & (a!=0) & r=0 & !in -> (r'=9);

	// w5 -> r3 | r4 | w4 (at any angle point)
	[delegated] pl=1 & w=5 & a!=0 & r=0 & delegated=true -> (in'=false) & (c'=0) & (delegated'=false);
	[delegated] pl=1 & w=5 & a!=0 & r=0 & delegated=true -> (in'=false) & (c'=1) & (delegated'=false);
	[delegated] pl=1 & w=5 & a!=0 & r=0 & delegated=true -> (in'=false) & (c'=2) & (delegated'=false);
	[fly] pl=1 & c=0 & w=5 & (a!=0) & r=0 & !in -> (r'=3);
	[fly] pl=1 & c=1 & w=5 & (a!=0) & r=0 & !in -> (r'=4);
	[fly] pl=1 & c=2 & w=5 & (a!=0) & r=0 & !in -> (w'=4) & (r'=0) & (in'=true); // set angle

	// w6 -> r2 | r3 |r8
	[delegated] pl=1 & w=6 & a!=0 & r=0 & delegated=true -> (in'=false) & (c'=0) & (delegated'=false);
	[delegated] pl=1 & w=6 & a!=0 & r=0 & delegated=true -> (in'=false) & (c'=1) & (delegated'=false);
	[delegated] pl=1 & w=6 & a!=0 & r=0 & delegated=true -> (in'=false) & (c'=2) & (delegated'=false);
	[fly] pl=1 & c=0 & w=6 & (a!=0) & r=0 & !in -> (r'=2);
	[fly] pl=1 & c=1 & w=6 & (a!=0) & r=0 & !in -> (r'=3);
	[fly] pl=1 & c=2 & w=6 & (a!=0) & r=0 & !in -> (r'=8);

	// non check points: fly autonomously
	// w1 -> r1 | r9
	[fly] pl=1 & w=1 & (a!=0) & r=0 & !in -> (r'=1);
	[fly] pl=1 & w=1 & (a!=0) & r=0 & !in -> (r'=9);

	// w3 -> r6 | w4 (any angle point)
	[fly] pl=1 & w=3 & (a!=0) & r=0 & !in -> (r'=6);
	[fly] pl=1 & w=3 & (a!=0) & r=0 & !in -> (w'=4) & (r'=0) & (in'=true); // set angle

	// w4 -> w3 | w5
	[fly] pl=1 & w=4 & (a!=0) & r=0 & !in -> (w'=3) & (r'=0) & (in'=true); // set angle
	[fly] pl=1 & w=4 & (a!=0) & r=0 & !in -> (w'=5) & (r'=0) & (in'=true); // set angle

	// r1 -> r2 | w1
	[fly] pl=1 & r=1 -> (r'=2);
	[fly] pl=1 & r=1 -> (w'=1) & (r'=0) & (in'=true); // set angle

	// r2 -> r1 | w6
	[fly] pl=1 & r=2 -> (r'=1);
	[fly] pl=1 & r=2 -> (w'=6) & (r'=0) & (in'=true); // set angle

	// r3 -> w5 | w6
	[fly] pl=1 & r=3 -> (w'=5) & (r'=0) & (in'=true); // set angle

	[fly] pl=1 & r=3 -> (w'=6) & (r'=0) & (in'=true); // set angle

	// r4 -> r5 | w5
	[fly] pl=1 & r=4 -> (r'=5);
	[fly] pl=1 & r=4 -> (w'=5) & (r'=0) & (in'=true); // set angle

	// r5 -> r4 | w2
	[fly] pl=1 & r=5 -> (r'=4);
	[fly] pl=1 & r=5 -> (w'=2) & (r'=0) & (in'=true); // set angle

	// r6 -> w2 | w3
	[fly] pl=1 & r=6 -> (w'=2) & (r'=0) & (in'=true); // set angle
	[fly] pl=1 & r=6 -> (w'=3) & (r'=0) & (in'=true); // set angle

	// r7 -> w2 | r8
	[fly] pl=1 & r=7 -> (w'=2) & (r'=0) & (in'=true); // set angle
	[fly] pl=1 & r=7 -> (r'=8);

	// r8 -> w6 | r7
	[fly] pl=1 & r=8 -> (w'=6) & (r'=0) & (in'=true); // set angle
	[fly] pl=1 & r=8 -> (r'=7);

	// r9 -> w1 | w2
	[fly] pl=1 & r=9 -> (w'=1) & (r'=0) & (in'=true); // set angle
	[fly] pl=1 & r=9 -> (w'=2) & (r'=0) & (in'=true); // set angle

	// stop if target reached
	[uav_stop] stop & pl=1 -> true;

endmodule

// CHOICE OF ANGLE POINTS
module angle_choice
	a:[0..8] init 0; // angle points

	// 3 -- 4 -- 5
	// |    |    |
	// 2    o    6
	// |    |    |
	// 1 -- 8 -- 7

	[prescribe] true -> (a'=1);
	[prescribe] true -> (a'=2);
	[prescribe] true -> (a'=3);
	[prescribe] true -> (a'=4);
	[prescribe] true -> (a'=5);
	[prescribe] true -> (a'=6);
	[prescribe] true -> (a'=7);
	[prescribe] true -> (a'=8);
	[delegate] true -> (a'=1);
	[delegate] true -> (a'=2);
	[delegate] true -> (a'=3);
	[delegate] true -> (a'=4);
	[delegate] true -> (a'=5);
	[delegate] true -> (a'=6);
	[delegate] true -> (a'=7);
	[delegate] true -> (a'=8);

	[camera] true -> (a'=0);
endmodule

// MISSION OBJECTIVE
module waypoint_check
	// check if waypoints w1, w2 and w6 have been visited
	[fly] w1 & w2 & w6 -> (stop'=true);
	[camera] w1 & w2 & w6 -> (stop'=true);
	[camera] !(w1 & w2 & w6) -> true;
	[fly] !(w1 & w2 & w6) -> true;
endmodule

rewards "time" // flight time
        [wait] true: 10;
        [fly] true: 60;
endrewards

rewards "ROZ" // ROZ occupancy
	[fly] roz : 1;
endrewards
View: printable version          Download: uav-game.prism

The properties explained above, for MDPs, are then expressed as follows:

// Expected time of completing the mission (covering waypoints w1, w2 and w6)
<<p1>> R{"time"}min=? [ Fc w1&w2&w6 ]

// Pareto curve: minimising the expected mission completion time vs. minimising ROZ visits
const double v_ROZ;
const double v_time;
<<p1>> (R{"ROZ"}<=v_ROZ [ C ] & R{"time"}<=v_time [ C ])

Case Studies