Translation of an Allen’s temporal logic variant to RPNL

Muhammad Arzaki, Anggha Satya Nugraha


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.

Full Text: PDF

How to Cite this Article:

Muhammad Arzaki, Anggha Satya Nugraha, Translation of an Allen’s temporal logic variant to RPNL, Journal of Mathematical and Computational Science, Vol 3, No 6 (2013), 1405-1429

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.

J. Math. Comput. Sci.

ISSN: 1927-5307

Editorial Office:


Copyright ©2018 JMCS