<?xml version="1.0" encoding="UTF-8"?>
<OAI-PMH xmlns="http://www.openarchives.org/OAI/2.0/" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://www.openarchives.org/OAI/2.0/ http://www.openarchives.org/OAI/2.0/OAI-PMH.xsd">
  <responseDate>2026-10-10T21:18:05Z</responseDate>
  <request identifier="27704" metadataPrefix="oai_dc" verb="GetRecord">https://drops.dagstuhl.de/oai</request>
  <GetRecord>
    <record>
      <header>
        <identifier>oai:drops-oai.dagstuhl.de:27704</identifier>
        <datestamp>2026-10-10T19:48:19Z</datestamp>
        <setSpec>ddc:004</setSpec>
        <setSpec>open_access</setSpec>
      </header>
      <metadata>
        <oai_dc:dc xmlns:oai_dc="http://www.openarchives.org/OAI/2.0/oai_dc/" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://www.openarchives.org/OAI/2.0/oai_dc/ http://www.openarchives.org/OAI/2.0/oai_dc.xsd">
          <dc:title>The Satisfiability Problem of Temporal-Spatial Logics over Quasi-Temporal Graphs</dc:title>
          <dc:creator>Alsmann, Eric</dc:creator>
          <dc:creator>Lange, Martin</dc:creator>
          <dc:creator>Semezies, Igor</dc:creator>
          <dc:subject>linear-time temporal logic</dc:subject>
          <dc:subject>modal logic</dc:subject>
          <dc:subject>temporal graphs</dc:subject>
          <dc:subject>computational complexity</dc:subject>
          <dc:subject>automated reasoning</dc:subject>
          <dc:description>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.</dc:description>
          <dc:publisher>Schloss Dagstuhl – Leibniz-Zentrum für Informatik</dc:publisher>
          <dc:contributor>Eric Alsmann and Martin Lange and Igor Semezies</dc:contributor>
          <dc:date>2026</dc:date>
          <dc:relation>Is Part Of OASIcs, Volume 146, 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)</dc:relation>
          <dc:type>InProceedings</dc:type>
          <dc:type>Text</dc:type>
          <dc:type>doc-type:ResearchArticle</dc:type>
          <dc:type>publishedVersion</dc:type>
          <dc:format>application/pdf</dc:format>
          <dc:identifier>doi:10.4230/OASIcs.TIME.2026.8</dc:identifier>
          <dc:identifier>urn:nbn:de:0030-drops-277049</dc:identifier>
          <dc:identifier>https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.8</dc:identifier>
          <dc:language>eng</dc:language>
          <dc:rights>https://creativecommons.org/licenses/by/4.0/legalcode</dc:rights>
        </oai_dc:dc>
      </metadata>
    </record>
  </GetRecord>
</OAI-PMH>
