Translation of an Allen’s temporal logic variant to RPNL

Abstract

In this paper, we investigate the relationship between Allen’s temporal logic (ATL) and the right propositional neighborhood logic (RPNL). We introduce ATL+B as a variant of ATL that includes Holds and Occurs predicates and its models are interpreted over arbitrary bounded below linearly ordered sets. We show that any ATL+B formula can be translated in linear time into an equisatisfiable RPNL formula. This translation makes the verification techniques of a system whose specification is described using ATL+ B can be performed using RPNL.