Description

We generated LTL and CTL specifications for the considered mission requirements. We (i) encoded the LTL and CTL specifications and the model of the scenario in NuSMV; (iii) we used NuSMV to check whether the verification of the specifications returned the same results. Mission requirements were generally not satisfied, since for being satisfied they have to hold on all the paths of the models. NuSMV always returned the same results for LTL and CTL specifications confirming the correctness of CTL specifications.

Reproduction Kit

To replicate this experiment run java -jar Exp5.jar randomMissions.txt 6 ./ true

Specifications & Data

Archive	File Contents #
Exp5.zip	13