Comparing LTL Semantics for Runtime Verification.
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, whereas at runtime only finite but incrementa...
| Main Authors: | , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
2010
|
| _version_ | 1797059908663771136 |
|---|---|
| author | Bauer, A Leucker, M Schallhart, C |
| author_facet | Bauer, A Leucker, M Schallhart, C |
| author_sort | Bauer, A |
| collection | OXFORD |
| description | 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, whereas at runtime only finite but incrementally expanding prefixes are available.In this work, we review LTL-derived logics for finite traces from a runtime-verification perspective. In doing so, we establish four maxims to be satisfied by any LTL-derived logic aimed at runtime verification. As no pre-existing logic readily satisfies all of them, we introduce a new four-valued logic Runtime Verification Linear Temporal Logic RV-LTL in accordance to these maxims. The semantics of Runtime Verification Linear Temporal Logic (RV-LTL) indicates whether a finite word describes a system behaviour which either (i) satisfies the monitored property, (ii) violates the property, (iii) will presumably violate the property, or (iv) will presumably conform to the property in the future, once the system has stabilized. Notably, (i) and (ii) correspond to the classical semantics of LTL, whereas (iii) and (iv) 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 Moore machines signalizing the semantics of the so far obtained execution trace w.r.t. the monitored property. © The Author, 2010. Published by Oxford University Press. All rights reserved. |
| first_indexed | 2024-03-06T20:10:44Z |
| format | Journal article |
| id | oxford-uuid:2a79b4f4-e240-424d-9309-dc5abb52c937 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T20:10:44Z |
| publishDate | 2010 |
| record_format | dspace |
| spelling | oxford-uuid:2a79b4f4-e240-424d-9309-dc5abb52c9372022-03-26T12:25:14ZComparing LTL Semantics for Runtime Verification.Journal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:2a79b4f4-e240-424d-9309-dc5abb52c937EnglishSymplectic Elements at Oxford2010Bauer, ALeucker, MSchallhart, CWhen 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, whereas at runtime only finite but incrementally expanding prefixes are available.In this work, we review LTL-derived logics for finite traces from a runtime-verification perspective. In doing so, we establish four maxims to be satisfied by any LTL-derived logic aimed at runtime verification. As no pre-existing logic readily satisfies all of them, we introduce a new four-valued logic Runtime Verification Linear Temporal Logic RV-LTL in accordance to these maxims. The semantics of Runtime Verification Linear Temporal Logic (RV-LTL) indicates whether a finite word describes a system behaviour which either (i) satisfies the monitored property, (ii) violates the property, (iii) will presumably violate the property, or (iv) will presumably conform to the property in the future, once the system has stabilized. Notably, (i) and (ii) correspond to the classical semantics of LTL, whereas (iii) and (iv) 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 Moore machines signalizing the semantics of the so far obtained execution trace w.r.t. the monitored property. © The Author, 2010. Published by Oxford University Press. All rights reserved. |
| spellingShingle | Bauer, A Leucker, M Schallhart, C Comparing LTL Semantics for Runtime Verification. |
| title | Comparing LTL Semantics for Runtime Verification. |
| title_full | Comparing LTL Semantics for Runtime Verification. |
| title_fullStr | Comparing LTL Semantics for Runtime Verification. |
| title_full_unstemmed | Comparing LTL Semantics for Runtime Verification. |
| title_short | Comparing LTL Semantics for Runtime Verification. |
| title_sort | comparing ltl semantics for runtime verification |
| work_keys_str_mv | AT bauera comparingltlsemanticsforruntimeverification AT leuckerm comparingltlsemanticsforruntimeverification AT schallhartc comparingltlsemanticsforruntimeverification |