Monitoring Execution Traces using Metric Alternating Automata
Ghulam Mujtaba
We present an automata based verification framework to monitor a running system against a high level specification. Our framework includes specification formalisms to express system properties and verification algorithms to check an execution trace of a system against the intended behavior.
Linear Temporal Logic (LTL) is a widely used specification language to express temporal properties of a system. We present Bounded Temporal Logic (BTL), which extends LTL by parameterizing temporal operators with time bounds. As compared to LTL, BTL is a natural and a more compact formalism to express time-bounded temporal properties.
In automata based verification, alternating automata (AA) are commonly used as intermediate representations of LTL specifications, because of their succinctness and linear translations from LTL formulae. However, the translation from BTL formulae to AA is exponential. We present metric alternating automata (MAA), a variant of AA, and a linear translation mechanism from BTL formulae to MAA.
A collection of algorithms, based on MAA, are presented to monitor an execution trace against a BTL specification. We start with specialized algorithms for different sublogics of BTL, and then present a generic algorithm which handles all the sublogics of BTL (including LTL) and performs as efficiently as the corresponding specialized algorithms for those sublogics.
Diploma Thesis.