Real time logics and reasoning answerset semantics for metric temporal logic

Abstract

Stream Reasoning ist ein neues Forschungsfeld, das sich auf die semantische Auswertung von Datenstreams konzentriert. Für dieses Feld wurde das LARS Framework geschaffen; es benutzt Logik Programmierung und Datenströme der Answerset Semantik.In dieser Arbeit führen wir neue Formalismen für das LARS Framework ein, indem wir die LARS Programmiersprache in Metric Temporal Logic (MTL) übersetzen. Mit dieser Logik lassen sich Formeln sehr prägnant ausdrücken und sie wertet diese Formeln auf Timed State Sequences anstatt auf Datenströmen aus. Diese Timed State Sequences unterscheiden zwischen einer System- und einer Echtzeit.Durch die Übersetzung von LARS auf MTL erhalten wir ein neues MTL Fragment, das wir Metric LARS nennen. Dieses Fragment umfasst alle Formeln, die sich in LARS übersetzen lassen. Für Metric LARS und Timed State Sequences wird auch Answerset Semantik eingeführt.Timed State Sequences werden weiters auch genauer behandelt und wir beschäftigen uns mit verschiedenen Möglichkeiten diese in Datenströme zu übersetzen. Hier gibt es mehrere Optionen, jenachdem wie die temporalen Daten modelliert werden sollen.Wir werfen außerdem noch einen Blick auf andere mit MTL verwandte Real-Time Logics wie Metric Interval Temporal Logic, Signal Temporal Logic und deren semantischen Strukturen, sowie Timed Propositional Temporal Logic, welche die Mutter dieser Familie der Logik ist.

Stream Reasoning is a young field of study that focuses on the high level evaluation of data streams. The LARS framework was created for this task utilizing a logic based approach, modelling data streams and programs in Answer Set Programming fashion. We introduce a new formalism for the LARS framework by translating the LARS logic programming language to Metric Temporal Logic. This logic expresses formulas more succinctly than others and uses timed state sequences instead of streams as semantic structures, which distinguish between system- and real-time. By translating LARS to MTL and back we create a new MTL fragment, called Metric LARS, which describes the LARS-translatable forumlas, and provide answer set semantics for timed state sequences and Metric LARS programs. Timed state sequences are explored in detail on their own and we give various options to translate them to LARS streams and back, with methods that can be chosen depending on the semantics of the data to be modelled. We further create fragments of Metric LARS for Metric Interval Temporal Logic, Signal Temporal Logic and their respective semantic structures and have a look at Timed Propositional Temporal Logic and its relation with Metric LARS.