On Monitoring Linear Temporal Properties

Runtime verification facilitates monitoring the executions of a system against temporal properties, commonly to detect violations. Not every temporal property is fully monitorable however: in some cases, a positive or negative verdict on the monitored execution does not depend on any finite prefix of it. We study the problem of monitoring properties written in Linear Temporal Properties. We concentrate on two topics: (1) the classification of properties according to the ability to provide positive and negative verdicts in finite time, and (2) the use of past LTL as opposed to future LTL for monitorability.