Standpoint Linear Temporal Logic

Many complex scenarios require the coordination of agents holding different points of view, possibly cooperating and not necessarily agreeing. For this reason, standpoint logic (SL) has been recently introduced in the context of knowledge integration, allowing one to reason with diverse and potentially conflicting viewpoints held by different agents. Linear temporal logic (LTL) is the most widely known formalism to express temporal properties of systems and processes, both in formal methods and artificial intelligence related fields. In this paper, we present 'standpoint linear temporal logic' (SLTL), a new logic that combines the temporal features of LTL with the multi-perspective modelling capacity of SL. We define the logic SLTL, its syntax, its semantics, establish its decidability and complexity, and provide a terminating tableau calculus to automate SLTL reasoning. Conveniently, this offers a clear path to extend existing LTL reasoners to provide practical reasoning support for temporal reasoning in multi-perspective settings.