Observation Strategies for Event Detection with Incidence on Runtime Verification Marco Alberti1 , Pierangelo Dell’Acqua2 , and Luı́s Moniz Pereira1 1 Centro de Inteligência Artificial (CENTRIA), Departamento de Informática Faculdade de Ciências e Tecnologia, Universidade Nova de Lisboa Caparica (Portugal) m.alberti@fct.unl.pt,lmp@di.fct.unl.pt 2 Dept. of Science and Technology, ITN Linköping University Norrköping (Sweden) pierangelo.dellacqua@liu.se Abstract 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 obser- vations, 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 tem- poral 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æ. Fi- nally, we discuss possible generalizations, and how event detection and related applications can benefit from logic programming techniques. 1 Introduction 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 verification, diagnosis, intention recognition, and more [9]). In order to detect events, it is naturally necessary to observe the system where the event may occur. 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 significant 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 prob- lem 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 Proceedings of the 17th International RCRA workshop (RCRA 2010): Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion Bologna, Italy, 10-11 June 2010 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 verification of Linear Temporal Logic formulæ. In Section 6, we discuss possible extensions and generalizations of our ap- proach, and the applications of techniques borrowed from logic programming to problems beyond simple event detection. 2 Event detection in general 2.1 Coordinate system A coordinate system defines points where events can happen. Coordinates can be interpreted, for instance, as spatial, temporal, or both. We only require sum to be defined over coordinates. Definition 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 significant, and the relevant information is the set of points where the pattern is defined. Definition 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 defined. S V P N {1} {h0, 1i, h4, 1i, h5, 1i} R2 R {hh0, 0i, 0i} R2 R {hhx, yi, xi | x ∈ R ∧ y ∈ R} R2 R {hhx, yi, 1i | 0 ≤ x ≤ 1 ∧ 0 ≤ y ≤ 1} Table 1: Example patterns An event is an association of values to points in a coordinate system that follows a given pattern. It is defined as the translation of its pattern by an offset. 2 Definition 3. Given a pattern P and τ ∈ S, the event EP (τ )of pattern P and offset τ is the set {hτ + p, P(p)i | p ∈ dom P}. We call unfolding the set of all possible events of a given pattern. Definition 4. Given a pattern P in a coordinate system S, the unfolding UP of P is the set {EP (τ ) | τ ∈ S}. Definition 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 first pattern in Table 1, the event EP (5) is {h5, 1i, h9, 1i, h10, 1i}, and its observability set is {5, 9, 10}. 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). Definition 6. A set C ⊆ S covers a pattern P if and only if for each τ ∈ S there exists an element of O(EP (τ )) that belongs to C. Example 2. Consider a pattern P, whose domain is {0, 1, 2}. {3n | n ∈ N} covers P. C , {1, 2} does not cover P, because, for instance, 3 belongs to the observability set of the event of pattern P and offset 3 and does not belong to C. For the same reason, {4n | n ∈ N} does not cover P. Example 3. C , Z×Z covers the last pattern in Table 1. Indeed, the observability set of an event of offset τ , hτx , τy i is {hx, yi | τx ≤ x ≤ τx + 1 ∧ τy ≤ y ≤ τy + 1}. It contains hbτx c+1, bτy c+1i (an element of C), because, for any α ∈ 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. Definition 7. Given a pattern P over S, the sampling problem consists of finding a set C ⊆ S that covers P. 3 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 mini- mize a cost function. If the cost of observation is a constant, that translates to minimum cardinality. However, applications can impose more require- ments. 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. Definition 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 rep- resents 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 definitions. Definition 9. Let I be a finite set of natural numbers, and let M , max I. For an integer k, let σk , {(p + k) mod (M + 1) | p ∈ I}. I’s circular repetition is the collection of sets U , {σk | k ∈ [0 .. M ]} Definition 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 , {q + k(M + 1) | q ∈ SC ∧ k ∈ N} covers P. Proof. Consider a generic event e of pattern P and offset τ . Let R , τ mod (M + 1). Consider σR . By hypothesis, it intersects SC in (at least) a natural number q. Since q ∈ σR , there exists p ∈ dom P such that q = (p + R) mod (M + 1). Since p ∈ dom P, τ + p ∈ 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, ∃k | τ + p = q + k(M + 1). Therefore, also τ + p ∈ C. Concluding, the observability set of a generic event of pattern P inter- sects C; that is, C covers P. Therefore, the sampling problem can be reduced to finding a set that intersects a collection of M + 1 subsets of [0 .. M ]. The periodic repetition 4 of such set, with period (M + 1), covers the pattern. A trivial, and uninter- esting, solution is [0 .. M ] itself (which corresponds to observing the system at all time points). However, finding 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. Definition 11. Given a natural pattern P, let m , min dom P. Then the normalization of P is the pattern P , {hp, P(p + m)i | p + m ∈ dom P}. Theorem 2. Let P be a natural pattern. Then an event of pattern P is also an event of pattern P. Proof. EP (τ ) , {hτ + p, P(p)i | p ∈ dom P} which, by substituting q+m for p, is equal to {hτ + q + m, P(q + m)i | q + m ∈ dom P} = EP (τ + m). Therefore, a set that covers the normalized pattern also covers the orig- inal 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 definition 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. Definition 12. Given a normalized pattern P and a covering shape SC of |SC | P’s, the corresponding sampling ratio is RSC ,P , 1+max dom P . |dom P| 2 4 6 8 10 12 14 16 18 20 RSC ,P 0.52 0.32 0.24 0.19 0.15 0.14 0.12 0.1 0.1 0.1 Table 2: Sampling ratios. Example 4. Table 2 shows average sampling ratios computed on random patterns with domain maximum of 20, for different values of the domain cardinality. Example 5. Let a pattern P’s domain be [0 .. M ]. dom P’s circular rep- etition is U , {σ0 , . . . , σM }, where for i ∈ [0 .. M ] σi = [0 .. M ]. A minimum hitting set for U is {i}, for any i ∈ [0 .. M ]. For each i, a cov- ering set is {i + k(M + 1) | k ∈ N}. The corresponding sampling ratio is 1 M +1 , confirming the intuitive idea that, if an event lasts M + 1 points, it is sufficient to observe every (M + 1)-th point to detect its occurrence. 5 Example 6. Consider a pattern P whose domain is {8, 10, 13}. Then dom P = {0, 2, 5}. dom P’s circular repetition is U , {σ0 , . . . , σ5 }, where σ0 , {0, 2, 5}, σ1 , {0, 1, 3}, σ2 , {1, 2, 4}, σ3 , {2, 3, 5}, σ4 , {0, 3, 4}, and σ5 , {1, 4, 5}. 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 , {0, 1, 3}. It can be easily verified that its cardinality is minimal. The corresponding covering set of P’s is C , {q + 6k | q ∈ {0, 1, 3} ∧ k ∈ N} = {0, 1, 3, 6, 7, 9, 12, . . .}, 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 first 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] , find 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 ∈ [1 .. k], let se , {i | e ∈ ri }, 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. 6 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) [17]: in particular, it will not be worse than ln n − ln ln n + 0.78, and it cannot be guaranteed to be better than ln n − ln ln n − 0.31. 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 ap- proximated efficiently 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. Ratio Ratio Time Time |dom P| (average) (max) (complete) (greedy) 2 1.0 1.0 24777.18 2.491 4 1.033 1.333 2023.496 1.915 6 1.02 1.2 296.656 1.83 8 1.0 1.0 48.383 1.73 10 1.033 1.333 21.473 1.787 12 1.0 1.0 7.937 1.716 14 1.0 1.0 6.318 1.675 16 1.0 1.0 1.556 1.614 18 1.0 1.0 1.363 1.843 20 1.0 1.0 1.522 1.668 Table 3: Comparison of the complete and greedy algorithms (times are in milliseconds). 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 min- imum hitting set, and the translation to set cover and solution with the greedy algorithm. We fixed max dom P = 20; |dom P| 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 expo- nentially with max dom P − |dom P|, which makes it inapplicable for bigger problems. The greedy algorithm is obviously faster; and its performance ra- 7 tio 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 verification of Linear Temporal Logic formulæ Intuitively, runtime verification is the problem of checking if an execution trace of some system enjoys a property [12]. A common choice for a for- malism to express properties is temporal logics and, in particular, Linear Temporal Logics (LTL) [16]. In the following, we discuss runtime verifica- tion of (some) LTL formulæ by observing partial execution traces. 5.1 Background In this section, we briefly recall standard definitions for LTL, and some additional definitions that we use later in the paper. Definition 13. Let A be a countable set of atomic formulæ, > represent truth and ⊥ represent falsity. Then a formula is defined recursively as follows: • > and ⊥ are formulæ; if ϕ ∈ 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 defined on a path in a Kripke structure. Definition 14. A Kripke structure is a tuple hS, S0 , R, A, V i, where S is a finite 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. Definition 15. Given a Kripke structure K , hS, S0 , R, A, V i, a path on K is a sequence of states π , s0 s1 . . . sn . . . such that ∀i ∈ N | (si+1 ∈ π ⇒ hsi , si+1 i ∈ R). Definition 16. Given a path π , s0 s1 . . . sn , . . . on a Kripke structure K, the k-th postfix of π is the sequence π k of states sk sk+1 . . . sn , . . .. Definition 17. For LTL formulæ ϕ and ψ, a Kripke structure K , hS, S0 , R, A, V i and a path π , s0 s1 . . . sn in K, • if ϕ ∈ A ∪ {>, ⊥}, π |= ϕ iff ϕ ∈ V (s0 ) or ϕ = >; • π |= ϕ ∨ ψ iff π |= ϕ or π |= ψ; π |= ϕ ∧ ψ iff π |= ϕ and π |= ψ; π |= ¬ϕ iff π 6|= ϕ 8 • π |= Xϕ iff π 1 |= ϕ • π |= ϕUψ iff π |= ψ, or ∃k > 0 | (π k |= ψ ∧ ∀i | 0 ≤ i < k | π i |= ϕ) • π |= ♦ϕ iff ∃k ≥ 0 | π k |= ϕ • π |= ϕ iff ∀k ≥ 0 | π k |= ϕ Definition 18. Given a state s in a Kripke structure and a formula ϕ, s |= ϕ if and only if there exists a path in K whose first state is s and π |= ϕ. 5.2 Partial paths In this section, we define partial paths, which formalize the idea of incom- plete execution traces. Definition 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 π (η @ π). Definition 20. Given a Kripke structure K, a path π , s0 s1 . . . sn . . . on K, and a finite set I of natural numbers whose maximum is M , π’s sam- pling 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 ∈ N and q ∈ I. Example 7. The sampling of a path π , s0 s1 . . . s16 of shape {0, 1, 3, 6} is s0 s1 s3 s6 s7 s8 s10 s13 s14 s15 . 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 satisfied by each state is written above the corresponding node; solid edges represent the sequence in the full path, and dashed edges repre- sent the sequence in the partial path. For example, in this representation the complete path is composed of the states s0 , {a} {a, b} {b} s1 and s2 , while the partial path is com- posed of the states s0 and s2 . State s0 sat- s0 s1 s2 isfies the atomic proposition a, s1 satisfies a and b, and s2 satisfies b. 5.3 Semantics in partial paths In general, a partial path is not a path in the original Kripke structure (be- cause 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 defined as follows. 9 Definition 21. Let K , hS, S0 , R, A, V i be a Kripke structure and π a path in K. Then, for each partial path η , s0 s1 . . . sn , with η @ π, the as- sociated Kripke structure Kη , hSη , S0η , Rη , Aη , Vη i is defined, where Sη is the set of states in η, S0η , {s0 }, Rη , {hsi , si+1 i | 0 ≤ i < n}, Aη , A, and Vη is the restriction of V to Sη . The semantics of formulæ on a partial path can then be defined 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. Box operator () Theorem 3. If η @ π, then π |= ϕ ⇒ η |= ϕ. Proof. Let s be a state in η; then, by η @ π, s ∈ π. By hypothesis, s |= ϕ. The same holds for any state in η. The opposite does not hold: {a} {} {a} s0 s1 s2 η |= a, but π 6|= a. Diamond operator (♦) Theorem 4. If η @ π, then π |= ♦ϕ ⇐ η |= ♦ϕ. Proof. Let s be the state in η such that s |= ϕ(such a state exists by hy- pothesis). Since η @ π, s ∈ π; i.e., ∃s ∈ π | s |= ϕ. The opposite does not hold: {a} {a, b} {a} s0 s1 s2 π |= ♦b, but η 6|= ♦b. Next operator (X) No general result can be proved about X. {} {a} {b} • π |= Xa, but η 6|= Xa s0 s1 s2 • η |= Xb, but π 6|= Xb. 10 Until operator (U) In general, no implication can be proved about U. {a, b} {b} {b, c} {d} • π |= bUd, but η 6|= bUd s0 s1 s2 s3 • η |= aUc, but π 6|= aUc 5.5 Event detection in LTL 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 define formally what it means for a LTL formula’s truth to follow a given (natural) pattern. Definition 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 π , s0 s1 . . . sn in K, (∃k | sk |= ϕ) ⇒ ∃i | (∀j ∈ dom P | si+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 π , s0 s1 . . . sn . . . on K, π |= ♦ϕ if and only if πSC |= ♦ϕ. Proof. If: by Theorem 4, because πSC is a subpath of π. Only if: π |= ♦ϕ, so ∃k | sk |= ϕ. By Definition 22, ∃i | (∀j ∈ dom P | sl |= ϕ, l = i + j). Such ls are the observability set of an event of pattern P and offset i (see Definition 5). Since SC is P’s cover- ing shape, by Theorem 1 the set C , {q + k(M + 1) | q ∈ SC ∧ k ∈ N}, 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 ∈ π, (ii) l = q + k(M + 1), for some q ∈ SC and k ∈ N, and (iii) sl |= ϕ. But properties (i) and (ii) define indices of states that belong to πSC , so sl ∈ πSC ; and because of property (iii), πSC |= ♦ϕ. 1 If the formula is understood as a logical represenetation of an event, this amounts to verifying the event’s occurrence. 11 6 Discussion In this paper, we focussed on one-dimensional natural patterns. A first generalization that comes to mind is to consider multi-dimensional natural coordinate systems. Another generalization is when events with different 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 tech- niques in general, namely efficient 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 find a trade-off between the costs of observation and of failed detection. Tools and techniques developed in the field 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 [10] and its efficient implementation [2] appear appropriate, as abduction can be used to formulate hypotheses on the state of the system in the time points not subject to observation. A first 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 combi- nations 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-effects, but which are not guaranteed to happen – i.e., the side-effects either don’t always follow if the event happens, or they may be side-effects of only a subset of the whole event, so that while the side-effects may actually happen (and 12 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-effects can be used heuristically as triggers to direct attention and speed up event detection by going for the more likely events first, given the side-effects. A Bayes net could be employed to code such heuristic and probabilistic information. In particular, side-effects 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 [14, 13]. [11] reports on a logic programming based system which infers team of agents’ intentions from traces of agents’ action events and observations. Similar to side-effects, in a mirror-like way, one may have premonitions, that is tell-tale prior-effects 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 significance 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 benefit. 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 confirm or disconfirm hypotheses about traces. If the system being discussed can be controlled (such as a logic program that can be evolved [7]), the problem can be viewed in the other direction, i.e., how to update the system in order to have it generate the desired traces. Such problems can have more than one solution. Preferences (now well understood in the context of logic programming [15]) can be used to rank among solutions, or as a heuristics along with abduction or evolution [8]. Thanks to the recent advances in logic programming technology, one may also think about trying to confirm and disconfirm an event at the same time (using multi-threaded computations) and take decisions depending on the first goal that succeeds. In summary, the topic of runtime verification and event detection can benefit from declarative logic programming because of the natural use of 13 logic programming, abduction, and event calculus for representing obser- vations and actions, as well as and its implementation tools in general, in order to support the topic’s ramifications and applications. The latter two concern not just opening declarative programming to the new areas of mon- itoring and control, but also the very use of runtime verification in program correctness and runtime safety. 7 Conclusions In this paper, we considered the problem of reducing the number of obser- vations for reliable event detection. We showed that, when the observation space can be modeled as the set of natural numbers, the number of observa- tions can be significantly reduced. In this case, the problem can be reduced to a NP-hard problem, but an approximation algorithm with good (theo- retical and experimental) performance can be applied. We showed how the result can be applied to runtime verification 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. Tor- roni. Verifiable 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. The- ory 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 sys- tems. In Proceedings of the 4th ACM international conference on Em- bedded 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 Artificial 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. 14 [7] P. Dell’Acqua, A. Lombardi, and L. M. Pereira. Modelling adaptive controllers with evolving logic programs. In J. Andrade-Cetto, J.-L. Ferrier, J. D. Pereira, and J. Filipe, editors, ICINCO 2006, Setúbal, Portugal. INSTICC Press, 2006. [8] P. Dell’Acqua and L. M. Pereira. Preferential theory revision. J. Applied Logic, 5(4):586–601, 2007. [9] A. Hinze, K. Sachs, and A. Buchmann. Event-based applications and enabling technologies. In DEBS ’09: Proceedings of the Third ACM International Conference on Distributed Event-Based Systems, pages 1–15, New York, NY, USA, 2009. ACM. [10] A. C. Kakas, R. A. Kowalski, and F. Toni. Abductive Logic Program- ming. Journal of Logic and Computation, 2(6):719–770, 1993. [11] T. Kanno, K. Nakata, and K. Furuta. A method for team intention inference. Int. J. Hum.-Comput. Stud., 58(4):393–413, 2003. [12] M. Leucker and C. Schallhart. A brief account of runtime verification. Journal of Logic and Algebraic Programming, 78(5):293 – 303, 2009. [13] L. M. Pereira and H. T. Anh. Intention recognition via causal bayes networks plus plan generation. In L. S. Lopes, N. Lau, P. Mariano, and L. Rocha, editors, 14th Portuguese Intl.Conf. on Artificial Intelligence, volume 5816 of LNAI, pages 138–149. Springer, October 2009. [14] L. M. Pereira and H. T. Anh. Intention recognition with evolution prospection and causal bayesian networks. In A. Madureira, J. Fer- reira, and Z. Vale, editors, Computational Intelligence for Engineering Systems 3: Emergent Applications, Intelligent Systems, Control and Automation: Science and Engineering Book Series. Springer, 2010. To appear. [15] L. M. Pereira, P. Dell’Acqua, and G. Lopes. On preferring and inspect- ing abductive models. In A. Gill and T. Swift, editors, Practical Aspects of Declarative Languages, 11th International Symposium, PADL 2009, Savannah, GA, USA, January 19-20, 2009. Proceedings, volume 5418 of Lecture Notes in Computer Science, pages 1–15. Springer, 2009. [16] A. Pnueli. The temporal logics of programs. In Proceedings of the 18th Symposium on the Foundations of Computer Science, pages 46– 57, 1977. [17] P. Slavı́k. A tight analysis of the greedy algorithm for set cover. In STOC ’96: Proceedings of the twenty-eighth annual ACM symposium on Theory of computing, pages 435–441, New York, NY, USA, 1996. ACM. 15