Bauer, Andreas; Leucker, Martin; Schallhart, Christian
This article studies runtime verification of properties expressed either in lineartime temporal logic (LTL) or timed lineartime temporal logic (TLTL). It classifies runtime verification in identifying its distinguishing features to model checking and testing, respectively. It introduces a three-valued semantics (with truth values true, false, inconclusive) as an adequate interpretation as to whether a partial observation of a running system meets an LTL or TLTL property. For LTL, a conceptually...[Show more]
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.