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 veri cation of linear temporal logics formul . Finally, we discuss possible generalizations, and how event detection and related applications can bene t from logic programming techniques.
An event is an observable state in a system, that may occur at some point in
space and time, and event detection is a crucial process in many applications
(such as monitoring, runtime veri cation, diagnosis, intention recognition,
and more [
However, observation may be a costly process. In this case, observing the system at all spatial or temporal points may be undesirable, and a question arises: is it possible to reduce the number of necessary observations, without losing certainty about the event's occurrence?
In this paper we formalize the problem, and show that, for the simple, but signi cant case where the observation space can be modelled as the set of natural numbers, the answer is yes.
The paper is structured as follows. In Section 2, we formulate the problem in a general setting. In Section 3, we study the problem for the special case where the temporal or spatial event structure can be described by a set of natural numbers. In Section 4, we compare experimentally a complete and an approximation algorithm. In Section 5, we give a formulation of the problem suitable for runtime veri cation of Linear Temporal Logic formul . In Section 6, we discuss possible extensions and generalizations of our approach, and the applications of techniques borrowed from logic programming to problems beyond simple event detection. 2 2.1
Coordinate system A coordinate system de nes points where events can happen. Coordinates can be interpreted, for instance, as spatial, temporal, or both. We only require sum to be de ned over coordinates.
De nition 1. A coordinate system S is the cartesian product of N sets, closed under the sum operation.
Each of the sets can be continuous (e.g., the set R of real numbers), or discrete (e.g., the sets N of natural numbers or Z of integer numbers). 2.2
Patterns A pattern associates a value taken from a value set V to (some) points in the coordinate system.
In the simplest case, V will have only one element. This representation is satisfactory in cases where the value is not signi cant, and the relevant information is the set of points where the pattern is de ned.
De nition 2. Given a coordinate system S, a pattern P over S is a partial function from S to some value set V.
As usual, we call the pattern's domain the set of points where the pattern is de ned.
S N R2 R2 R2
V f1g R R R
P fh0; 1i; h4; 1i; h5; 1ig
fhh0; 0i; 0ig fhhx; yi; xi j x 2 R ^ y 2 Rg fhhx; yi; 1i j 0 x 1 ^ 0 y
1g De nition 3. Given a pattern P and 2 S, the event EP ( )of pattern P and o set is the set fh + p; P(p)i j p 2 dom Pg.
We call unfolding the set of all possible events of a given pattern.
De nition 4. Given a pattern P in a coordinate system S, the unfolding UP of P is the set fEP ( ) j 2 Sg.
De nition 5. An event e's observability set O(e) is e's projection over S.
Intuitively, the observability set is the set of points in the coordinate system where the event can be observed.
Example 1. If P is the rst pattern in Table 1, the event EP (5) is fh5; 1i; h9; 1i; h10; 1ig, and its observability set is f5; 9; 10g.
A set of points in the coordinate system that is guaranteed to intersect the observability set of any event with a given pattern can be understood as the set of points to observe to decide about the occurrence of such an event. We say that such a set covers the pattern or is one of the pattern's covering sets. For example, if the coordinate system represents a spatial area, a covering set can be understood as a set of positions to deploy sensors (as in wireless sensor networks applications).
De nition 6. A set C S covers a pattern P if and only if for each 2 S there exists an element of O(EP ( )) that belongs to C.
Example 2. Consider a pattern P, whose domain is f0; 1; 2g. f3n j n 2 Ng covers P. C , f1; 2g does not cover P, because, for instance, 3 belongs to the observability set of the event of pattern P and o set 3 and does not belong to C. For the same reason, f4n j n 2 Ng does not cover P.
Example 3. C , Z Z covers the last pattern in Table 1. Indeed, the observability set of an event of o set , h x; yi is fhx; yi j x x x + 1 ^ y y y + 1g. It contains hb xc+1; b yc+1i (an element of C), because, for any 2 R, b c + 1 + 1. 2.3
The sampling problem If the application requires to determine the occurrence of an event with a given pattern, it is of interest to determine a set of points in the coordinate system that guarantees that, if an event occurs, it will be observed.
De nition 7. Given a pattern P over S, the sampling problem consists of nding a set C S that covers P.
The general problem has a trivial solution (S), but the solution may be required to enjoy some property. A reasonable requirement is for it to minimize a cost function. If the cost of observation is a constant, that translates to minimum cardinality. However, applications can impose more requirements. For instance, if the points in the coordinate system represent time points, then it may be required for the covering set to intersect observability sets at or near their minimum, in order to detect events as soon as possible. 3
Sampling problem for natural patterns In this section, we consider the case where the coordinate system is the set N of natural numbers.
De nition 8. A natural pattern is a pattern over the set N of natural numbers.
A natural interpretation for this case is that the coordinate system represents a sequence of time points at which the system can be observed.
The following result allows for a reduction of the sampling problem for natural patterns. First we provide two de nitions.
De nition 9. Let I be a nite set of natural numbers, and let M
For an integer k, let k , f(p + k) mod (M + 1) j p 2 Ig.
I's circular repetition is the collection of sets U , f k j k 2 [0 :: M ]g , max I.
De nition 10. Let P be a natural pattern.
Then a set with non-empty intersection with each element of the circular repetition of dom P is a covering shape of P's.
Theorem 1. Let P be a natural pattern and let M , max dom P.
Let SC be a covering shape of P's.
Then the set C , fq + k(M + 1) j q 2 SC ^ k 2 Ng covers P.
Proof. Consider a generic event e of pattern P and o set . Let R , mod (M + 1). Consider R. By hypothesis, it intersects SC in (at least) a natural number q. Since q 2 R, there exists p 2 dom P such that q = (p + R) mod (M + 1). Since p 2 dom P, + p 2 O(e). Since is equal to R modulo M +1, +p is equal to R+p modulo M +1, which is equal to q modulo M +1. Therefore, 9k j + p = q + k(M + 1). Therefore, also + p 2 C.
Concluding, the observability set of a generic event of pattern P intersects C; that is, C covers P.
Therefore, the sampling problem can be reduced to nding a set that intersects a collection of M + 1 subsets of [0 :: M ]. The periodic repetition of such set, with period (M + 1), covers the pattern. A trivial, and uninteresting, solution is [0 :: M ] itself (which corresponds to observing the system at all time points). However, nding such a set with minimum cardinality is a well known NP-hard problem: the minimum hitting set problem.
For applications, it seems reasonable to consider patterns whose domain contains 0. However, the following result lets us reduce to this case, for generic pattern domains.
De nition 11. Given a natural pattern P, let m , min dom P.
Then the normalization of P is the pattern
P , fhp; P(p + m)i j p + m 2 dom Pg.
Theorem 2. Let P be a natural pattern. Then an event of pattern P is also an event of pattern P.
Proof. EP ( ) , fh + p; P(p)i j p 2 dom Pg which, by substituting q +m for p, is equal to fh + q + m; P(q + m)i j q + m 2 dom Pg = EP ( + m).
Therefore, a set that covers the normalized pattern also covers the original pattern. This lets us solve the sampling problem for the normalized pattern, whose domain's maximum element is in general lesser, and reduce complexity and approximation ratio, if an approximation algorithm is used (see Section 4).
The following de nition gives a measure of how much the number of necessary observation is reduced by observing the system only at a pattern's covering set, instead of at all points.
De nition 12. Given a normalized pattern P and a covering shape SC of P's, the corresponding sampling ratio is RSC;P , 1+majSxCdojm P .
jdom Pj RSC;P
Example 5. Let a pattern P's domain be [0 :: M ]. dom P's circular repetition is U , f 0; : : : ; M g, where for i 2 [0 :: M ] i = [0 :: M ]. A minimum hitting set for U is fig, for any i 2 [0 :: M ]. For each i, a covering set is fi + k(M + 1) j k 2 Ng. The corresponding sampling ratio is M1+1 , con rming the intuitive idea that, if an event lasts M + 1 points, it is su cient to observe every (M + 1)-th point to detect its occurrence. Example 6. Consider a pattern P whose domain is f8; 10; 13g. Then dom P = f0; 2; 5g. dom P's circular repetition is U , f 0; : : : ; 5g, where 0 , f0; 2; 5g, 1 , f0; 1; 3g, 2 , f1; 2; 4g, 3 , f2; 3; 5g, 4 , f0; 3; 4g, and 5 , f1; 4; 5g. P's covering shape SC is required to have non-empty intersection with all the sets in U ; for instance, a possible covering shape is SC , f0; 1; 3g. It can be easily veri ed that its cardinality is minimal. The corresponding covering set of P's is C , fq + 6k j q 2 f0; 1; 3g ^ k 2 Ng = f0; 1; 3; 6; 7; 9; 12; : : :g, which also covers P, and the sampling ratio is RSC;P = 3=6 = 1=2. 4
Algorithms and experimental evaluation In this section, we discuss solution methods for the minimum hitting set problem that the sampling problem reduces to, for natural patterns, as shown in section 3. We describe a complete algorithm, and we discuss reduction to the set cover problem, and its solution by means of a well known approximation polynomial algorithm. We compare experimentally the two algorithms.
Complete algorithm The algorithm is based on a total order of all the elements of 2[0 :: max dom P]; one is returned as the minimum hitting set.
The algorithm tries, as a rst attempt, the full integer interval from 0 to max dom P which obviously hits the pattern domain's circular repetition. Then, at any stage, it tests for hitting the next set with lesser cardinality than the current best, according to the aforementioned order.
Reduction to set cover and approximated solution The minimum hitting set problem is equivalent to the set cover problem: given a collection S 2[1 :: n], nd a subset of S of minimal cardinality whose union is [1 :: n].
Given a collection R , r1 : : : rn of sets, whose union is [1 :: k], the minimum hitting set problem for R can be formulated as a set cover problem as follows. For each e 2 [1 :: k], let se , fi j e 2 rig, and let S be the collection of all such sets. The union of each subset T of S is the set of indices of the sets in R which contain one of the indices of the sets in T . Thus, the indices of a solution T of a set cover problem for S form a minimum hitting set for R, because T 's union is [1 :: n], so all elements of R have non-empty intersection with the set of T 's indices, and the union of no proper subset of T is [1 :: n], or T would not be minimal.
The set cover problems has been widely studied in the literature; in particular, approximation algorithms have been proposed for it. A very simple algorithm is the so-called greedy algorithm: at each step, it chooses the set with higher cardinality, and it deletes such set's elements from the other sets, until the universe is covered.
Its performance (expressed as the ratio between the cardinality of the
output and of the minimal covering collection) is ln n ln ln n + (1) [
Several inapproximability results for set cover have been shown: to the best of our knowledge, the best lower bound for the performance ratio has been proved by Alon et al. [3], who proved that set cover cannot be approximated e ciently to less than c ln n, for a constant c, unless P = N P . Therefore, the greedy algorithm performance is close to the best we can hope for, among polynomial algorithms.
In our case, for the aforementioned reduction of minimum hitting set to set cover, given a natural pattern P, n is max dom P + 1.
jdom Pj
Experimental comparison However, in our case, the greedy algorithm performed better experimentally than the theoretical lower bound.
In order to assess performance for our application, we experimented with the two aforementioned solution methods: the complete algorithm for minimum hitting set, and the translation to set cover and solution with the greedy algorithm.
We xed max dom P = 20; jdom Pj varies. For each parameter value, we generated a random pattern and computed a covering shape with the two methods; we repeated such each computation 50 times. Results are shown in Table 3. In each line, we show the average and maximum performance ratio, as well as the computation times (on a 2:0GHz dual-core CPU).
As expected, computation time for the complete algorithm grows exponentially with max dom P jdom Pj, which makes it inapplicable for bigger problems. The greedy algorithm is obviously faster; and its performance ratio appears to be better than its lower bound which, for M = 20, would be ln 21 ln ln 21 0:31 = 1:62. 5
Runtime veri cation of Linear Temporal Logic
formul
Intuitively, runtime veri cation is the problem of checking if an execution
trace of some system enjoys a property [
Background In this section, we brie y recall standard de nitions for LTL, and some additional de nitions that we use later in the paper.
De nition 13. Let A be a countable set of atomic formul , > represent truth and ? represent falsity. Then a formula is de ned recursively as follows: > and ? are formul ; if ' 2 A, ' is a formula; if ' is a formula, :', X', ', and
' are formul ; if ' and are formul , then ' ^ , ' _ , and 'U are formul .
A formula's truth value is de ned on a path in a Kripke structure.
De nition 14. A Kripke structure is a tuple hS; S0; R; A; V i, where S is a nite set of states, S0 S is a set of initial states, R S S is a transition relation, A is a countable set of atomic propositions, and V : S ! 2A is a labeling function.
De nition 15. Given a Kripke structure K , hS; S0; R; A; V i, a path on K is a sequence of states , s0s1 : : : sn : : : such that 8i 2 N j (si+1 2 ) hsi; si+1i 2 R).
De nition 16. Given a path , s0s1 : : : sn; : : : on a Kripke structure K, the k-th post x of is the sequence k of states sksk+1 : : : sn; : : :.
De nition 17. For LTL formul ' and , a Kripke structure K , hS; S0; R; A; V i and a path , s0s1 : : : sn in K, if ' 2 A [ f>; ?g,
j= ' i ' 2 V (s0) or ' = >; j= ' _ j= ;
i j= ' or j= :' i 6j= ' j= ; j= ' ^ i
j= ' and j= 'U i
1 j= ' j= j= ' i ' i 9k 8k In this section, we de ne partial paths, which formalize the idea of incomplete execution traces.
De nition 19. Given a Kripke structure K, a partial path on K is a sub-sequence of some path on K; is a sub-path of ( @ ). De nition 20. Given a Kripke structure K, a path , s0s1 : : : sn : : : on K, and a nite set I of natural numbers whose maximum is M , 's sampling of shape I, I , is the sequence of states si such that si is a state in and i = q + k(M + 1), for some k 2 N and q 2 I.
Example 7. The sampling of a path is s0s1s3s6s7s8s10s13s14s15.
, s0s1 : : : s16 of shape f0; 1; 3; 6g Graphical representation of paths A path is represented graphically as follows: a state s is represented as a node with label s; the set of atomic propositions satis ed by each state is written above the corresponding node; solid edges represent the sequence in the full path, and dashed edges represent the sequence in the partial path.
For example, in this representation the complete path is composed of the states s0, fag fa; bg fbg s1 and s2, while the partial path is composed of the states s0 and s2. State s0 sat- s0 s1 s2 is es the atomic proposition a, s1 satis es a and b, and s2 satis es b. 5.3
Semantics in partial paths In general, a partial path is not a path in the original Kripke structure (because two consecutive states are not in the transition relation). Therefore, in order to give semantics to formul on the partial path, an associated Kripke structure can be de ned as follows. De nition 21. Let K , hS; S0; R; A; V i be a Kripke structure and a path in K. Then, for each partial path , s0s1 : : : sn, with @ , the associated Kripke structure K , hS ; S0 ; R ; A ; V i is de ned, where S is the set of states in , S0 , fs0g, R , fhsi; si+1i j 0 i < ng, A , A, and V is the restriction of V to S .
The semantics of formul on a partial path can then be de ned as in Defs. 17 and 18, where the relevant Kripke structure is the one associated with the partial path. 5.4
Formula entailment in partial and full paths In this section, we discuss logical relations between entailment of a LTL formula in full and partial paths.
Proof. Let s be a state in ; then, by s j= '. The same holds for any state in .
The opposite does not hold: fag fg s0 s1 fag s2
'. , s 2
. By hypothesis, a, but 6j=
'. such that s j= '(such a state exists by hy; i.e., 9s 2 j s j= '.
Next operator (X) No general result can be proved about X.
fg fag fbg The opposite does not hold: fag fa; bg s0 s0 s1 s1 fag s2 s2 b, but 6j= j= Xa, but j= Xb, but 6j= Xa 6j= Xb.
Until operator (U) In general, no implication can be proved about U. fa; bg fbg fb; cg fdg s0 s1 s2 s3 j= bUd, but j= aUc, but 6j= bUd 6j= aUc The results in Section 5.4 are too weak to be of practical use. However, in an application where (i) it is of interest to detect if a formula ' is entailed by at least one state in a path (that is, to verify '1), and (ii) it is known that ''s truth follows a given pattern (e.g., ' is entailed by a number of consecutive states, or it is entailed by a state, then by the following state, then by the state that comes after four more states), the result of Theorem 1 can be applied.
First, we de ne formally what it means for a LTL formula's truth to follow a given (natural) pattern.
De nition 22. Given a natural pattern P, a formula ' is an LTL-event of pattern P in a Kripke structure K if and only if for any path , s0s1 : : : sn in K, (9k j sk j= ') ) 9i j (8j 2 dom P j si+j j= ').
The following results allows to verify the occurrence of a LTL formula by observing a sampling of a path, rather than the full path. Theorem 5. Let ' be a LTL-event of pattern P on a Kripke structure K. Let SC be a covering shape of P's. Then, for each path , s0s1 : : : sn : : : on K, j= ' if and only if SC j= '.
Proof. If: by Theorem 4, because SC is a subpath of .
Only if: j= ', so 9k j sk j= '. By De nition 22, 9i j (8j 2 dom P j sl j= '; l = i + j). Such ls are the observability set of an event of pattern P and o set i (see De nition 5). Since SC is P's covering shape, by Theorem 1 the set C , fq + k(M + 1) j q 2 SC ^ k 2 Ng, where M , max SC , intersects the observability sets of all the events of shape P, that is, it contains at least one of the aforementioned ls.
Summarizing, there exists some l with the following properties: (i) sl 2 , (ii) l = q + k(M + 1), for some q 2 SC and k 2 N, and (iii) sl j= '. But properties (i) and (ii) de ne indices of states that belong to SC , so sl 2 SC ; and because of property (iii), SC j= '.
1If the formula is understood as a logical represenetation of an event, this amounts to verifying the event's occurrence.
In this paper, we focussed on one-dimensional natural patterns. A rst generalization that comes to mind is to consider multi-dimensional natural coordinate systems.
Another generalization is when events with di erent patterns can occur. In this case, we can distinguish two cases: one where the value sets of the patterns are disjoint (so an event can be immediately recognized), and the other where, once an event is detected, more observations are required in order to determine its pattern.
If more than one event is considered, complex events can be composed from simple ones by conjunction, disjunction, sequence or negation (as in event algebras [4]).
This brings out the opportunity to employ model-based diagnosis techniques in general, namely e cient kernel diagnosis algorithms that detect maximal intersections of hitting sets [6], and allow for detection of multiple persistent and intermittent diagnosis[5].
In case detection of all events is not critical, one may consider further reducing the number of observations, and estimate the probability of missing an event; decision theory can be applied to nd a trade-o between the costs of observation and of failed detection.
Tools and techniques developed in the eld of logic programming can be
used to go beyond event detection, in case of partial execution traces. In
particular, approaches based on abductive logic programming [
A rst extension that comes to mind is to consider more than one type of event. The occurrence of an event would be represented by an abducible predicate. For instance, it can be of interest to express permissible combinations of events, which may be expressed by means of integrity constraints; or to express relations of expectancy of an event depending on the detection of another.
For instance, the SCIFF abductive logic language [1] supports special predicate H(a), meaning that event a happened, and abducible predicates E(a) and EN(a), meaning, respectively, that event a is expected to happen, or expected not to happen. Integrity constraints as H(a) ) E(b) _ E(c) can be used as a guidance mechanism to perform detection: a's occurrence would trigger an attempt to detect the occurrence of b or c, in order to satisfy the integrity constraint.
More generally, events sometimes have tell-tale side-e ects, but which are not guaranteed to happen { i.e., the side-e ects either don't always follow if the event happens, or they may be side-e ects of only a subset of the whole event, so that while the side-e ects may actually happen (and even then with a probability) the complete event might not be there.
Also, if detected they may assure us the event occurred (though not being formally part of the event) or simply allow to hypothesize that event or some other event. The classical example in this case, framed using abduction, is "the grass is wet": did it rain during the night or was the sprinkler left on or both? On the other hand, it may have rained but the grass no longer being wet.
These tell-tale side-e ects can be used heuristically as triggers to direct
attention and speed up event detection by going for the more likely events
rst, given the side-e ects. A Bayes net could be employed to code such
heuristic and probabilistic information. In particular, side-e ects can be
tell-tale signs of intentions, which in turn lead to actions and events. This
connects the event detection issues to intention recognition, combining Bayes
nets with plan recognition, and combining uncertainty KR and rule KR in
general [
Similar to side-e ects, in a mirror-like way, one may have premonitions, that is tell-tale prior-e ects that may be omens of (sub-)events to follow, for which all of the above can likewise be re-stated, with consequences for heuristics leading to faster or priority event recognition.
The importance of the tell-tale signs, prior or posterior, can be evaluated for signi cance and preferential compatibility. A case in point might be the tell-tale signs concerning a possible natural disaster or deliberate attack, with consequences for preventive or palliative measures. This raises the issue of how can events be countered or forestalled. On the other hand, positive events might be leveraged for greater bene t.
In case execution traces are being observed, but there is uncertainty about observations, predictive lookahead can be used to remove uncertainty. Same goes, regarding uncertainty removal, for retrospective hindsight (by making observations about the past, cf. astronomy) in order to con rm or discon rm hypotheses about traces.
If the system being discussed can be controlled (such as a logic program
that can be evolved [
Such problems can have more than one solution. Preferences (now well
understood in the context of logic programming [
Thanks to the recent advances in logic programming technology, one may also think about trying to con rm and discon rm an event at the same time (using multi-threaded computations) and take decisions depending on the rst goal that succeeds.
In summary, the topic of runtime veri cation and event detection can bene t from declarative logic programming because of the natural use of logic programming, abduction, and event calculus for representing observations and actions, as well as and its implementation tools in general, in order to support the topic's rami cations and applications. The latter two concern not just opening declarative programming to the new areas of monitoring and control, but also the very use of runtime veri cation in program correctness and runtime safety.
In this paper, we considered the problem of reducing the number of observations for reliable event detection. We showed that, when the observation space can be modeled as the set of natural numbers, the number of observations can be signi cantly reduced. In this case, the problem can be reduced to a NP-hard problem, but an approximation algorithm with good (theoretical and experimental) performance can be applied. We showed how the result can be applied to runtime veri cation of temporal logic formul . We also discussed possible extensions and generalizations of the problem, and argued for the use of logic programming techniques and systems to handle increased sophistication.
References [1] M. Alberti, F. Chesani, M. Gavanelli, E. Lamma, P. Mello, and P. Torroni. Veri able agent interaction in abductive logic programming: the S CIFF framework. ACM Transactions on Computational Logic (TOCL), 9(4), 2008. [2] J. J. Alferes, L. M. Pereira, and T. Swift. Abduction in well-founded semantics and generalized stable models via tabled dual programs. Theory and Practice of Logic Programming, 4(4):383{428, 2004. [3] N. Alon, D. Moshkovitz, and S. Safra. Algorithmic construction of sets for k-restrictions. ACM Trans. Algorithms, 2(2):153{177, 2006. [4] J. Carlson and B. Lisper. An event detection algebra for reactive systems. In Proceedings of the 4th ACM international conference on Embedded software, pages 147{154, New York, NY, USA, 2004. ACM. [5] J. de Kleer. Diagnosing multiple persistent and intermittent faults. In C. Boutilier, editor, IJCAI 2009, Proceedings of the 21st International Joint Conference on Arti cial Intelligence, Pasadena, California, USA, July 11-17, 2009, pages 733{738, 2009. [6] J. de Kleer, A. K. Mackworth, and R. Reiter. Characterizing diagnoses and systems. Artif. Intell., 56(2-3):197{222, 1992.