Observation strategies for event detection with incidence on runtime verification

In many applications, it is required to detect the occurrence of an event in a system, which entails observing the system. Observation can be costly, so it makes sense to try and reduce the number of observations, without losing certainty about the event's occurrence. In this paper, we propose a formalization of the problem. We show (formally) that when the event to be detected follows a discrete spatial or temporal pattern, it is possible to reduce the number of observations. We provide an experimental evaluation of algorithms for this purpose. We apply the result to verification of linear temporal logics formulæ. Finally, we discuss possible generalizations, and how event detection and related applications can benefit from logic programming techniques.