Propositional interval temporal logics are quite expressive temporal logics that allow one to naturally express statements that refer to time intervals. Unfortunately, most such logics turned out to be (highly) undecidable. To get decidability, severe syntactic and/or semantic restrictions have been imposed to interval-based temporal logics that make it possible to reduce them to point-based ones. The problem of identifying expressive enough, yet decidable, new interval logics or fragments of existing ones which are genuinely interval-based is still largely unexplored. In this paper, we focus our attention on interval logics of temporal neighborhood. We address the decision problem for the future fragment of Neighborhood Logic (Right Propositional Neighborhood Logic, RPNL for short) and we positively solve it by showing that the satisfiability problem for RPNL over natural numbers is NEXPTIME-complete. Then, we develop a sound and complete tableau-based decision procedure and we prove its optimality.

An Optimal Decision Procedure for Right Propositional Neighborhood Logic

SCIAVICCO, Guido
2007

Abstract

Propositional interval temporal logics are quite expressive temporal logics that allow one to naturally express statements that refer to time intervals. Unfortunately, most such logics turned out to be (highly) undecidable. To get decidability, severe syntactic and/or semantic restrictions have been imposed to interval-based temporal logics that make it possible to reduce them to point-based ones. The problem of identifying expressive enough, yet decidable, new interval logics or fragments of existing ones which are genuinely interval-based is still largely unexplored. In this paper, we focus our attention on interval logics of temporal neighborhood. We address the decision problem for the future fragment of Neighborhood Logic (Right Propositional Neighborhood Logic, RPNL for short) and we positively solve it by showing that the satisfiability problem for RPNL over natural numbers is NEXPTIME-complete. Then, we develop a sound and complete tableau-based decision procedure and we prove its optimality.
2007
Bresolin, Davide; Montanari, Angelo; Sciavicco, Guido
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in SFERA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11392/2326672
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 37
  • ???jsp.display-item.citation.isi??? 29
social impact