Optimizing LOLA Specifications
Mark Timon Hüneberg
LOLA is a stream-based specification language for the online monitoring of synchronous systems. For this, LOLA offers two main functions. On the one hand it can serve as a verification tool and check, whether a single execution path satisfies a certain property. On the other hand it allows for the collection of statistics about the system execution. The monitoring algorithm can become inefficient, if LOLA specifications contain streams that depend on their own future values. In this thesis we will present methods to remove such forward-recursion from LOLA specifications in order to optimize the performance of the monitoring algorithm. We will use an automata-theoretic approach to optimize specifications, which are supposed to check properties, and we will use a mathematical approach to optimize specification that collect statistics. We will also present our implementation of these methods and illustrate experimental results to demonstrate the effectiveness of our optimization procedures.
Bachelor Thesis.