Finite Satisfiability of Interval Temporal Logic Formulas with Multi-Objective Metaheuristics

Interval temporal logics provide a natural framework for reasoning about interval structures over linearly ordered domains. Despite being relevant for a broad spectrum of application domains, ranging from temporal databases to artificial intelligence and verification of reactive systems, interval temporal logics still miss tools capable of efficiently supporting them. We approach the finite satisfiability problem for one of the simplest meaningful interval temporal logic, namely A (also known as Right Propositional Neighborhood Logic) and we propose three different multi-objective evolutionary algorithms to solve it by means of a metaheuristic for multi-objective optimization. The resulting semi-decision procedure, although incomplete, turns out to be easier to implement and more scalable with respect to classical complete algorithms.