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 semantics of the so far obtained execution trace.
机构:
Univ Toronto, Dept Med, Toronto, ON, Canada
Univ Toronto, Dept Lab Med & Pathobiol, Toronto, ON, Canada
Toronto Gen Hosp, Res Inst, Expt Therapeut, Toronto, ON, Canada
Univ Hlth Network, Div Haematol Oncol, Toronto, ON, Canada
Canadian Blood Serv, Ctr Innovat, Toronto, ON, CanadaUniv Toronto, Dept Med, Toronto, ON, Canada