An Interval Temporal Logic for Time Series Specification and Data Integration

The analysis of temporal series—in particular, analysis of multisensor data—is a complex problem. It depends on the application domain, the way the data have to be used, and sensors available, among other factors. Various models, algorithms, and technologies have been designed for this goal. Temporal logics are used to describe temporal properties of systems. The properties may specify the occurrence and the order of events in time, recurring patterns, complex behaviors, and processes. In this paper, a new interval logic, called duration calculus for functions (DC4F), is proposed for the specification of temporal series corresponding to multisensor data. DC4F is a natural extension of the well-known duration calculus, an interval temporal logic for the specification of process duration. The adequacy of the proposed logic is analyzed in the case of multisensor data concerning volcanic eruption monitoring. It turns out that the relevant behavior concerns time intervals, not only accumulated history as it is described in other kinds of temporal logics. The examples analyzed demonstrate that a description language is required to specify time series of various kind relative to time intervals. The duration calculus cannot be successfully applied for this task. The proposed calculus allows one to specify temporal series and complex interval-dependent behaviors, and to evaluate the corresponding data within a unifying logical framework. It allows to formulate hypotheses concerning volcano eruption phenomena. However, the expressivity of DC4F comes at the cost of its decidability.

Anatomy of Alternating Quantifier Satisfiability (Work in progress)

We report on work in progress to generalize an algorithm recently introduced in [10] for checkingsatisfiability of formulas with quantifier alternation. The algorithm uses two auxiliary procedures:a procedure for producing a candidate formula for quantifier elimination and a procedure for eliminatingor partially eliminating quantifiers. We also apply the algorithm for Presburger Arithmeticformulas and evaluate it on formulas from a model checker for Duration Calculus [8]. We report onexperiments on different variants of the auxiliary procedures. So far, there is an edge to applyingSMT-TEST proposed in [10], while we found that a simpler approach which just eliminates quantifiedvariables per round is almost as good. Both approaches offer drastic improvements to applyingdefault quantifier elimination.