Model Checking Linear Temporal Logic with Standpoint Modalities

Standpoint linear temporal logic (SLTL) is a recently

introduced extension of classical linear temporal logic

(LTL) with standpoint modalities. Intuitively, these

modalities allow to express that, from agent a's

standpoint, it is conceivable that a given formula holds.

Besides the standard interpretation of the standpoint

modalities we introduce four new semantics, which differ

in the information an agent can extract from the history.

We provide a general model checking algorithm applicable to

SLTL under any of the five semantics. Furthermore we

analyze the computational complexity of the corresponding

model checking problems, obtaining PSPACE-completeness in

three cases, which stands in contrast to the known

EXPSPACE-completeness of the SLTL satisfiability problem.