Abstract: Linear Temporal Logic (LTL), proposed in 1977 by Amir Pnueli for reasoning about ongoing programs, was defined over infinite traces. The motivation for this was the desire to model arbitrarily long computations. While this approach has been highly successful in the context of model checking, it has been less successful in the context of reactive synthesis, due to the challenging algorithmics of infinite-horizon temporal synthesis. In this talk we show that focusing on finite-horizon temporal synthesis offers enough algorithmic advantages to compensate for the loss in expressiveness. In fact, finite-horizon reasonings is useful even in the context of infinite-horizon applications. |
Abstract: Visual Analytics integrates the outstanding capabilities of humans in terms of visual information exploration with the enormous processing power of computers to form powerful information and knowledge discovery environments. In other words, Visual Analytics is the science of analytical reasoning facilitated by interactive interfaces and captures the information discovery process keeping the human in the loop as well as gaining deeper insights into huge heterogeneous and complex data sources. Time is an important data dimension with distinct characteristics. Time is common across many application domains (e.g., medical records, planning, or project management). In contrast to other quantitative data dimensions, which are usually “flat”, time has an inherent semantic structure, which increases time’s complexity substantially. The hierarchical structure of granularities in time (e.g., minutes, hours, days, weeks, or months), is unlike that of most other quantitative dimensions. Specifically, time comprises different forms of divisions (e.g., 60 minutes correspond to one hour, while 24 hours make up one day), and granularities are combined to form calendar systems (e.g., Gregorian, Julian, business, or academic calendars). Moreover, time contains natural cycles and re-occurrences, as for example seasons, but also social (often irregular) cycles, like holidays or school breaks. Therefore, time-oriented data, i.e., data that are inherently linked to time, need to be treated differently than other kinds of data and require appropriate visual, interactive, and analytical methods to explore and analyze them.
In this talk, I will illustrate the concepts of Visualization and Visual Analytics. I will characterize the dimension of time as well as time-oriented data as well as describe tasks that users seek to accomplish using temporal Visual Analytics methods. I will address three key questions: “what” is visualized, “why” is it visualized, and “how” it is visualized. Various examples will illustrate what has been achieved so far and show possible future directions and challenges. |
Abstract: Complex Event Recognition (CER for short) refers to the activity of processing high-velocity streams of primitive events by evaluating queries that detect complex events: collections of primitive events that satisfy some pattern. In particular, CER queries match incoming events on the basis of their content; where they occur in the input stream; and how this order relates to other events in the stream. CER has been successfully applied in diverse domains such as maritime monitoring, network intrusion detection, industrial control systems and real-time analytics.
In this talk, I will survey our recent work on developing a formal framework for specifying and evaluating CER queries and will explain in particular a novel CER evaluation algorithm whose complexity is provably asymptotically optimal. The implementation of this algorithm in the CORE COmplex event Recognition Engine shows that in practice the algorithm exhibits stable query performance, even for long sequence queries and large time windows, and outperforms existing systems by up to five orders of magnitude on different workloads.
I will discuss the essential ideas behind both the supported query language and evaluation algorithm, as well as their limitations, and from these limitations discuss open questions relevant for the TIME community. |