Comparing LTL semantics for runtime verification

Date

Authors

Bauer, Andreas

Leucker, Martin

Schallhart, Christian

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,

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

URI

http://hdl.handle.net/1885/56980

Collections

ANU Research Publications

Source

Journal of Logic and Computation

Type

Journal article

DOI

10.1093/logcom/exn075

Restricted until

2037-12-31

Downloads

File

Description

01_Bauer_Comparing_LTL_semantics_for_2010.pdf (444.62 KB)

02_Bauer_Comparing_LTL_semantics_for_2010.pdf (429.32 KB)

03_Bauer_Comparing_LTL_semantics_for_2010.pdf (111.56 KB)