Title: A Proof-Theoretic Study of Linear Temporal Logic Monitoring

Abstract:
Runtime verification is becoming increasingly popular in software engineering where  system correctness is being extensively sought for.  A possible approach for runtime verification is to have a monitor generated from the high-level logic of choice, such as LTL, checking whether the correctness property is observed. Although there is a body of work dealing with the monitorability of properties expressed in Linear Temporal Logic, the synthesis algorithms discussed in such work uses different concepts and mechanisms. These differences hinder the full understanding of each monitoring approach and complicate comparisons.

The solution proposed in this work is that of viewing monitoring algorithms as a proof system. This teases apart the semantics of the logic from algorithms that check respective satisfactions in this logic. The advantage of this approach is that of having a common underlying framework whereby different monitoring approaches can be expressed and subsequently compared.