Supplementary material of the paper:

Three-Valued Spatio-Temporal Logic a further analysis on spatio-temporal properties of stochastic systems

Ludovica Luisa Vissat, Michele Loreti, Laura Nenzi, Jane Hillston, Glenn Marion (QEST 2017)


Three-Valued Spatio-Temporal (TSTL) properties verification

We provide the spatio-temporal evolution of TSTL properties related with the case studies presented in the paper.
Case study: Defining safety zones
High risk zones
Safe zones without control
Safe zones with control

Case study: Emergency evacuation route
Safe exit (r=2.0)
Safe exit (r=4.0)
Fire spread

MELA models

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

Case study: Defining safety zones
MELA model without control
MELA model with control

Case study: Emergency evacuation route
MELA model safe exit

jSSTL: java Signal Spatio-Temporal Logic

jSSTL is a Java tool for the specification and verification of Signal Spatio-Temporal Logic SSTL.