Description

We generated the LTL specifications of the considered mission requirements. We (i) negated the LTL specification; (ii) encoded the specification and the model of the scenario in NuSMV; (iii) used NuSMV to check whether the models contained a path that satisfied the mission specification (violates its negation). If a plan was present we used Simbad to simulate the robot executing the plan. We verified whether the results where correct: when we expected a plan to not be present in the given model, NuSMV was not able to compute it, and, when a plan was expected to be present it was computed by NuSMV. We also checked the correctness of the generated plans using the Simbad simulator.

Video

Reproduction Kit

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

Specifications & Data

Archive	File Contents #
Exp4.zip	13