Comparing LTL semantics for runtime verification

Date

2010

Authors

Bauer, Andreas
Leucker, Martin
Schallhart, Christian

Journal Title

Journal ISSN

Volume Title

Publisher

Oxford University Press

Abstract

When monitoring a system w.r.t. 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,

Description

Keywords

Keywords: Classical semantics; Execution trace; Finite traces; Finite words; Four-valued logic; Infinite word; Linear temporal logic; LTL property; Moore machines; Observed systems; Run-time verification; Runtimes; Semantics; Temporal logic Monitoring; Runtime verification; Temporal logic

Citation

Source

Journal of Logic and Computation

Type

Journal article

Book Title

Entity type

Access Statement

License Rights

Restricted until

2037-12-31