A tableau-based decision procedure for a branching-time interval temporal logic

Propositional interval temporal logics are very expressive temporal logics, with simple syntax and semantics, which allow one to naturally express statements that refer to time intervals and continuous processes. Most of them feature temporal operators that only allow one to express properties of a single timeline. In this paper we develop a branching-time interval neighborhood logic that interleaves operators that quantify over possible timelines with operators that quantify over intervals belonging to a given timeline. We define its syntax and semantics, and we provide it with a doubly-exponential tableau-based decision procedure.