Automated Reasoning in Temporal DL-Lite

TL;DR

This paper explores automated reasoning over temporal DL-Lite knowledge bases using existing LTL reasoners, analyzing their performance and scalability, and introduces a graphical tool for designing such KBs.

Contribution

It demonstrates the feasibility of using off-the-shelf LTL reasoners for TDL-Lite reasoning and provides a user-friendly interface for KB design.

Findings

Reasoners' robustness and scalability tested with random TDL-Lite KBs

Performance measured by running time and translation size

A graphical interface for designing TDL-Lite KBs developed

Abstract

This paper investigates the feasibility of automated reasoning over temporal DL-Lite (TDL-Lite) knowledge bases (KBs). We test the usage of off-the-shelf LTL reasoners to check satisfiability of TDL-Lite KBs. In particular, we test the robustness and the scalability of reasoners when dealing with TDL-Lite TBoxes paired with a temporal ABox. We conduct various experiments to analyse the performance of different reasoners by randomly generating TDL-Lite KBs and then measuring the running time and the size of the translations. Furthermore, in an effort to make the usage of TDL-Lite KBs a reality, we present a fully fledged tool with a graphical interface to design them. Our interface is based on conceptual modelling principles and it is integrated with our translation tool and a temporal reasoner.