Search Results

Temporal Graph Neural Networks (TGNN) are used to detect patterns in so-called temporal graphs (TG): graphs in which edges may be added or removed over time. Sälzer et al. suggested to study the expressive power of TGNNs through temporal-spatial logics, specifically the combination of the linear-time temporal logic LTL and modal logic K. In this paper we investigate the computational complexity of the satisfiability problem for this logic and its natural extension in which the LTL part is replaced by a linear-time μ-calculus, reflecting TGNNs' ability to recognise not just star-free (word) languages. We consider their interpretation over a more natural class of models which we call quasi-temporal graphs (QTG), relaxing certain conditions on the temporal evolutions of nodes that are indifferent to the logic. We formalise this by giving an adjusted notion of bisimulation which preserves satisfaction in these logics. It turns out that satisfiability over the class of QTGs is PSPACE-complete for the temporal-spatial logic based on LTL but becomes EXPTIME-complete when based on the μ-calculus. This is in contrast to the situation on words where both logics are PSPACE-complete. We also discuss consequences for the special satisfiability problems over the class of TGs.