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.
Copyright © 2013 Muhammad Arzaki, Anggha Satya Nugraha. This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
Cite this article
M. Arzaki, A. S. Nugraha, Translation of an Allen’s temporal logic variant to RPNL, J. Math. Comput. Sci. 3 (2013), 1405–1429.
BibTeX
@article{Arzaki2013,
author = {Arzaki, Muhammad and Nugraha, Anggha Satya},
title = {Translation of an Allen’s temporal logic variant to RPNL},
journal = {J. Math. Comput. Sci.},
volume = {3},
year = {2013},
pages = {1405--1429},
doi = {}
}