Comparing LTL Semantics for Runtime Verification

When monitoring a system wrt. a property defined in a temporal logic such as LTL, a major concern is to settle with an adequate interpretation of observable system events; that is, models of temporal logic formulae are usually infinite words of events, whereas at runtime only finite but incrementally expanding prefixes are available. In this work, we review LTL-derived logics for finite traces from a runtimeverification perspective. In doing so, we establish four maxims to be satisfied by any LTL-derived logic aimed at runtime-verification. As no preexisting logic readily satisfies all of them, we introduce a new four-valued logic RV-LTL in accordance to these maxims. The semantics of RV-LTL indicates whether a finite word describes a system behaviour which either (1) satisfies the monitored property, (2) violates the property, (3) will presumably violate the property, or (4) will presumably conform to the property in the future, once the system has stabilised. Notably, (1) and (2) cor...

• Type: Journal
• Year: 2010
• Where: LOGCOM
• Authors: Andreas Bauer 0002, Martin Leucker, Christian Schallhart
• Keywords: LOGCOM 2010, Logic, Ltl-derived Logic, Monitored Property, Programming Languages