Sciweavers

Share
LOGCOM
2010

Comparing LTL Semantics for Runtime Verification

9 years 4 months ago
Comparing LTL Semantics for Runtime Verification
When monitoring a system wrt. 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, whereas at runtime only finite but incrementally expanding prefixes are available. In this work, we review LTL-derived logics for finite traces from a runtimeverification perspective. In doing so, we establish four maxims to be satisfied by any LTL-derived logic aimed at runtime-verification. As no preexisting logic readily satisfies all of them, we introduce a new four-valued logic RV-LTL in accordance to these maxims. The semantics of RV-LTL indicates whether a finite word describes a system behaviour which either (1) satisfies the monitored property, (2) violates the property, (3) will presumably violate the property, or (4) will presumably conform to the property in the future, once the system has stabilised. Notably, (1) and (2) cor...
Andreas Bauer 0002, Martin Leucker, Christian Scha
Added 20 May 2011
Updated 20 May 2011
Type Journal
Year 2010
Where LOGCOM
Authors Andreas Bauer 0002, Martin Leucker, Christian Schallhart
Comments (0)
books