Quantified Dynamic Metric Temporal Logic for Dynamic Networks of Stochastic Hybrid Automata

Multiprocessing systems are capable of running multiple processes concurrently. By now such systems have established themselves as the defacto standard for operating systems. At the core of an operating system is the ability to execute programs and as such there must be a primitive for instantiating new processes - also programs are allowed to die/terminate. Operating systems may allow the executing programs to split (spawn) into more computational threads in order to let programs take advantage of concurrent execution as well. One of the most used modelling languages, Timed Automata, is based on multiple automata interacting thus they easily model the concurrent execution of programs. However, this language assumes a fixed size system in the sense that automata cannot be created at will but must be instantiated when the overall system is created. This is in contrast with the fact that developers are able to create threads when needed. In this paper we present our continued work to incorporate spawning of threads into UPPAAL SMC. Our modelling language, Dynamic Networks of Stochastic Hybrid Automata, is essentially Timed Automata extended with a spawning primitive and a tear-down primitive. The dynamic creation of threads has the side-effect that it is no longer possible to use ordinary logics to specify behaviours of individual threads - because the threads no longer have unique names. In this paper we propose an extension of Metric Temporal Logic with means for quantifying over the dynamically created threads. This makes it possible to zoom in on individual threads and specify requirements to their future behaviour. Furthermore, we present a monitoring procedure for the logic based on rewriting formulas. The presented modelling language and the specification language have been implemented in UPPAAL SMC version 4.1.18.