Supplementary material of the paper: Analysis of spatio-temporal properties of stochastic systems using TSTL

Ludovica Luisa Vissat, Michele Loreti, Laura Nenzi, Jane Hillston, Glenn Marion

Three-Valued Spatio-Temporal (TSTL) properties verification: evacuation routes

To analyse the TSTL property (10 time units, r=2.0) presented in Fig. 3 in the paper:

• Download zip file.

• Run java -jar FireAnalysis.jar

• The MATLAB file AnalysisPlot.m can be used to visualize the output of the analysis.

To analyse the TSTL property (t=0, r=2.0) presented in Fig. 4 in the paper:

• Download zip file.

• Run java -jar GSafe.jar

• The MATLAB file AnalysisPlot.m can be used to visualize the output of the analysis.

• For different agent movement rates, r = 1.0 (zip file), 3.0 (zip file), 4.0 (zip file)

Reliability requirement

To apply the automatic procedure for the analysis of the TSTL property (t=0, r=4.0, k=10) presented in Fig. 6 in the paper:

• Download zip file.

• Run java -jar safeRoute.jar

• The output will show the number of runs needed to satisfy each requirement. The MATLAB file AnalysisPlot.m can be used to visualize the output of the TSTL analysis at the given time point, inserting the correct file name in the MATLAB file (in the first line). The name, safeRoute_n.txt, will depend on the output, where n is the number of runs needed for each requirement.

• The output Result.txt will show the number of simulations and the number of U values of the corresponding analysis.

To apply the automatic procedure for the analysis of the TSTL property (t=5, k=10) presented in Fig. 7 in the paper:

• Download zip file.

• Run java -jar Fire.jar

• The output will show the number of runs needed to satisfy each requirement. The MATLAB file AnalysisPlot.m can be used to visualize the output of the TSTL analysis at the given time point, inserting the correct file name in the MATLAB file (in the first line). The name, fire_n.txt, will depend on the output, where n is the number of runs needed for each requirement.

• The output Result.txt will show the number of simulations and the number of U values of the corresponding analysis.

Three-Valued Spatio-Temporal (TSTL) properties verification: anonymity network

To analyse the properties presented in Fig. 8-12 in the paper:

• Download zip file for the chosen scenario:
  Scenario 1: basic scenario
  Scenario 2: messages M0 5 time faster
  Scenario 3: messages M0 10 time faster
  Scenario 4: 50 initial messages for S0
  

• Run java -jar Scenario_n.jar, choosing the appropriate n, between 1, 2, 3, 4, depending on the scenario.

• Figures 8-11: the Python file plot01.py can be used to visualize the output of the analysis of the TSTL property , while the Python files plotM0.py and plotM1.py can be used to visualize the output of the analysis, looking at the estimated satisfaction probabilities of the relative SSTL properties.
• Figure 12: the Python file plotTotal.py can be used to visualize the output of the analysis of the TSTL property .

Additional material (videos)

We provide the spatio-temporal evolution of TSTL properties related with the case study on emergency evacuation route presented in the paper.

Safe exit (r=2.0)
Safe exit (r=4.0)
Fire spread

Additional material (MELA models)

We present the MELA models we used to perform stochastic simulations.

Case study: Emergency evacuation route
MELA model safe exit

Case study: Anonymity network
Basic Scenario
Messages M0 move 5 time faster
Messages M0 move 10 time faster
Sender S0 has 50 initial messages