The Good, the Bad, and the Ugly, But How Ugly Is Ugly?

When monitoring a system wrt. a property defined in some temporal logic, e. g., 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 streams of events, whereas at runtime only prefixes are available. This work defines a four-valued semantics for LTL over finite traces, which extends the classical semantics, and allows to infer whether a system behaves (1) according to the monitored property, (2) violates the property, (3) will possibly violate the property in the future, or (4) will possibly conform to the property in the future, once the system has stabilised. Notably, (1) and (2) correspond to the classical semantics of LTL, whereas (3) and (4) are chosen whenever an observed system behaviour has not yet lead to a violation or acceptance of the monitored property. Moreover, we present a monitor construction for RV-LTL properties in terms of a Moore machine signalising the se...

• Type: Conference
• Year: 2007
• Where: RV
• Authors: Andreas Bauer 0002, Martin Leucker, Christian Schallhart
• Keywords: Classical Semantics, RV 2007, Temporal Logic, Temporal Logic Formulae