Paper Info
Title
Runtime verification of traces under recording uncertainty
Abstract
We present an on-line algorithm for the runtime checking of temporal properties, expressed as past-time Linear Temporal Logic (LTL) over the traces of observations recorded by a "black box"-like device. The recorder captures the observed values but not the precise time of their occurrences, and precise truth evaluation of a temporal logic formula cannot always be obtained. In order to handle this uncertainty, the checking algorithm is based on a three-valued semantics for past-time LTL defined in this paper. In addition to the algorithm, the paper presents results of an evaluation that aimed to study the effects of the recording uncertainty on different kinds of temporal logic properties.
Year
DOI
Venue
2011
10.1007/978-3-642-29860-8_35
RV
Keywords
Field
DocType
recording uncertainty,precise truth evaluation,checking algorithm,temporal logic formula,precise time,on-line algorithm,runtime verification,temporal property,past-time ltl,temporal logic property,past-time linear temporal logic
Computation tree logic,Black box (phreaking),Programming language,Computer science,Runtime verification,Theoretical computer science,Real-time computing,Linear temporal logic,Temporal logic,Semantics
Conference
Citations 
PageRank 
References 
8
0.51
12
Authors
4
Name
Order
Citations
PageRank
Shao-hui Wang112619.62
Anaheed Ayoub21048.15
Oleg Sokolsky32193154.94
Insup Lee44996413.64