Instructions

• Exercise 1 focuses on Deep Neural Networks and is mandatory
• Package your answers (Jupyter notebook, Prism model files) into zip and share it with us

●Exercise 2 focuses on Probabilistic Model Checking and is ‘best-effort’

Exercise 1: Deep Neural Networks

Objectives

1.Run and fine-tune a pre-trained pix2pix (DNN1) that can translate images from a satellite view to a flood segmentation map (sat2map) network. This result is DNN2.

2.Evaluate the model on a hand-made labelled dataset on both DNN1 and DNN2.

• Report IoU metric (to be implemented) for 10 different cross validation splits of our 87 images xBD2seg.zip dataset.

Given

• Existing implementation of the pix2pix model designed for paired image-to-image translation task and associated data.
• xBD2seg.zip dataset: a dataset of images (1024 x1024 pixels) extended from xBD (Building damage satellite imagery) as input X, and a segmentation of floods in the output image for each image input. The dataset is small and manually annotated.

Tasks

1.Run the pretrained pix2pix DNN (DNN1)

2.Implement and briefly describe two fine tuning strategies, i.e., one should be adding one-two final layers to DNN1 and train on the xBD2seg-train set to finetune DNN2 to segment xBD2seg-test set.

3.Implement the Intersection-over-union (IoU) metric to quantify ability of the network at segmenting floods from satellite images of size.

4.Report IoU for 10 different splits train/test of xBD2Seg dataset.

5.According to literature, an IoU of 0.5-0.65 is the state of the art on segmentation tasks over high resolution satellite imagery. Can fine tuning of DNN2 achieve this performance?

6.Compare your fine tuned network to the results you obtain from training a model from scratch using 256×256 cropos over our 1024×1024 xBD2seg dataset.

Help

You may report visual results for real image A, real image B and Generated image B with pix2pix sat2map model in a similar grid as the one below

but where the fake images should be segmented areas of flood:

Expected output

The provided segmented dataset evaluated together with the ground truth labelled data:

The IoU metric reported for each image in the given dataset in a pdf of the final Jupyter notebook: IoU of sample #1 is…

IoU of sample #2 is …

IoU of sample #3 is …

IoU of sample #n

Exercise 2: Probabilistic Model Checking

Objective

1.Use probabilistic modelling to model a medical rescue scenario involving drones that have to deliver supplies to a first responder team treating an injured runner in the park (location 4 in the figure). Two nearby healthcare centers (locations 1 and 2) are equipped to dispatch drones of different types (A and B, respectively).

• Verify properties of interest for the modelled scenario

Scenario

When moving to the location where the first-responder team is placed, drones have to cover some distance, and that consumes energy of their batteries. Drones A and B have different energy efficiency, meaning that drone A consumes 1000 mwh per kilometer, while drone B consumes 2000 mwh per kilometer.

Moreover, the air space is not entirely safe and drones might collide against obstacles when they are on their way to deliver their payload. In particular, the probability of collision of the drones are:

●Drone A: 0.3 when moving between locations 1 and 2;

●Drone B: 0.6 when moving between locations 2 and 3;

●Drones A and B: 0.1 when moving between locations 3 and 4.

Finally, municipal regulations also prescribe that, at any given time, only a single drone can be flying within the park’s airspace. Hence, your model should be constrained so that the situation in which more than one drone is within park premises (i.e., in location 4) at the same time never occurs.

Tasks

1.Model the described scenario as a DTMC using the probabilistic modelling language Prism

2.Write and verify a probabilistic computational tree logic (PCTL) propertyto calculate the overall probability that the payload will be eventually delivered to the first responder team

3.Write and verify a PCTL property to calculate the overall probability that any of the drones will collide before arriving at the park.

For Tasks (2) and (3), provide:

• the PCTL formula you have written to check the property.
• A brief, informal description of the PCTL property, including the adequacy of temporal operators employed, the meaning of the different elements in the formula (relating them e.g., to the meaning of variables and other elements in your model, if needed), and how they work together to achieve the desired result.
• A screenshot of the result of checking the formula in PRISM, along with a brief explanation of your interpretation of the results (i.e., what does the result mean?).

Help

• You can download Prism from http://prismmodelchecker.org/download.php
• A DTMC Prism model of a fair 6-sided die with PCTL properties that can be evaluated using this model are available at http://prismmodelchecker.org/tutorial/die.php

The data set file is too long that is why cannot uploaded here. the data set will be given later through google drive