Document Open Access Logo

FO and MSO Model Checking on Temporal Graphs

Authors Michelle Döring , Jessica Enright , Laura Larios-Jones , George Skretas

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAND.2026.9.pdf
  • Filesize: 1.14 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Mathematics of computing → Graph algorithms
  • Theory of computation → Fixed parameter tractability
Keywords
  • temporal graphs
  • dynamic graphs
  • time-varying graphs
  • parameterized complexity
  • logic
  • meta-theorems
  • monadic second-order logic
  • first-order logic
  • treewidth
  • planar
  • nowhere dense
  • lifetime
  • temporal total degree
  • vertex-interval membership width
  • tree-interval membership width

Metrics

Abstract

Algorithmic meta-theorems provide an important tool for showing tractability of graph problems on graph classes defined by structural restrictions. While such results are well established for static graphs, corresponding frameworks for temporal graphs are comparatively limited.
In this work, we revisit past applications of logical meta-theorems to temporal graphs and develop an extended unifying logical framework. Our first contribution is the introduction of logical encodings for the parameters vertex-interval-membership width (vim) and tree-interval-membership width (tim), parameters that capture the signature of vertex and component activity over time. Building on this, we extend existing monadic second-order (MSO) meta-theorems for bounded lifetime and temporal total degree to the parameters vim and tim, and establish novel first-order (FO) meta-theorems for all four parameters.
Finally, we signpost a modular lexicon of reusable FO and MSO formulas for a broad range of temporal graph problems, and give an example. This lexicon allows new problems to be expressed compositionally and directly yields fixed-parameter tractability results across the four parameters we consider.

Cite As Get BibTex

Michelle Döring, Jessica Enright, Laura Larios-Jones, and George Skretas. FO and MSO Model Checking on Temporal Graphs. In 5th Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 373, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAND.2026.9

Author Details

Michelle Döring
  • Hasso Plattner Institute, University of Potsdam, Germany
Jessica Enright
  • School of Computing Science, University of Glasgow, UK
Laura Larios-Jones
  • School of Computing Science, University of Glasgow, UK
George Skretas
  • Hasso Plattner Institute, University of Potsdam, Germany

Acknowledgements

We thank Sebastian Siebertz for his valuable feedback.

References

  1. Stefan Arnborg, Jens Lagergren, and Detlef Seese. Easy problems for tree-decomposable graphs. Journal of Algorithms, 12(2):308-340, 1991. URL: https://doi.org/10.1016/0196-6774(91)90006-K.
  2. Binh-Minh Bui-Xuan, Florent Krasnopol, Bruno Monasson, and Nathalie Sznajder. Model checking with temporal graphs and their derivative, 2026. URL: https://doi.org/10.48550/arXiv.2602.12446.
  3. Benjamin Merlin Bumpus and Kitty Meeks. Edge Exploration of Temporal Graphs. Algorithmica, 85(3):688-716, 2023. URL: https://doi.org/10.1007/s00453-022-01018-7.
  4. Arnaud Casteigts, Timothée Corsini, and Writika Sarkar. Simple, Strict, Proper, Happy: A Study of Reachability in Temporal Graphs. Theoretical Computer Science, 991:114434, 2024. URL: https://doi.org/10.1016/j.tcs.2024.114434.
  5. Arnaud Casteigts, Anne-Sophie Himmel, Hendrik Molter, and Philipp Zschoche. Finding Temporal Paths Under Waiting Time Constraints. Algorithmica, 83(9):2754-2802, 2021. URL: https://doi.org/10.1007/s00453-021-00831-w.
  6. Arnaud Casteigts, Nils Morawietz, and Petra Wolf. Distance to Transitivity: New Parameters for Taming Reachability in Temporal Graphs. In Rastislav Královič and Antonín Kučera, editors, 49th International Symposium on Mathematical Foundations of Computer Science, volume 306, pages 36:1-36:17, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. ISSN: 1868-8969. URL: https://doi.org/10.4230/LIPIcs.MFCS.2024.36.
  7. Justine Cauvi and Laurent Viennot. Parameterized Restless Temporal Path, 2025. URL: https://doi.org/10.48550/arXiv.2507.05760.
  8. Dibyayan Chakraborty, Antoine Dailly, Florent Foucaud, and Ralf Klasing. Algorithms and Complexity for Path Covers of Temporal Dags, 2024. URL: https://hal.science/hal-04493029.
  9. Bruno Courcelle. Graph Rewriting: An Algebraic and Logic Approach. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pages 193-242. Elsevier, 1990. URL: https://doi.org/10.1016/B978-0-444-88074-1.50010-X.
  10. Professor Bruno Courcelle and Dr Joost Engelfriet. Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach. Cambridge University Press, USA, 1st edition, 2012. Google Scholar
  11. Marek Cygan, Fedor V. Fomin, Łukasz Kowalik, Daniel Lokshtanov, Daniel Marx, Marcin Pilipczuk, and Michał Pilipczuk. Parameterized Algorithms, volume 5. Springer, a edition, 2015. Google Scholar
  12. Tom Davot, Jessica Enright, and Laura Larios-Jones. Parameterised algorithms for temporally satisfying reconfiguration problems. In International Symposium on Algorithmics of Wireless Networks, pages 89-103. Springer, 2025. URL: https://doi.org/10.1007/978-3-032-09120-8_7.
  13. Argyrios Deligkas, Michelle Döring, Eduard Eiben, Tiger-Lily Goldsmith, George Skretas, and Georg Tennigkeit. Parameterized Complexity of Temporal Connected Components: Treewidth and Temporal Path Number, 2025. URL: https://doi.org/10.48550/arXiv.2510.05806.
  14. Argyrios Deligkas, Eduard Eiben, and George Skretas. Minimizing Reachability Times on Temporal Graphs via Shifting Labels. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China, volume 5, pages 5333-5340, 2023. URL: https://doi.org/10.24963/ijcai.2023/592.
  15. Michelle Döring. Simple, Strict, Proper, and Directed: Comparing Reachability in Directed and Undirected Temporal Graphs. In The 36th International Symposium on Algorithms and Computation, ISAAC 2025, volume 359, pages 27:1-27:21, Tainan, Taiwan, 2025. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2025). URL: https://doi.org/10.4230/LIPIcs.ISAAC.2025.27.
  16. H.-D. Ebbinghaus, J. Flum, and W. Thomas. Mathematical Logic. Springer, New York, NY, 1994. URL: https://doi.org/10.1007/978-1-4757-2355-7.
  17. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite Model Theory. Springer Science & Business Media, 1999. Google Scholar
  18. Jessica Enright, Samuel D. Hand, Laura Larios-Jones, and Kitty Meeks. Structural Parameters for Dense Temporal Graphs. LIPIcs, Volume 306, MFCS 2024, 306:52:1-52:15, 2024. URL: https://doi.org/10.4230/LIPIcs.MFCS.2024.52.
  19. Jessica Enright, Samuel D. Hand, Laura Larios-Jones, and Kitty Meeks. Families of Tractable Problems with Respect to Vertex-Interval-Membership Width and Its Generalisations, 2025. URL: https://doi.org/10.48550/arXiv.2505.15699.
  20. Jessica Enright, Kitty Meeks, George B. Mertzios, and Viktor Zamaraev. Deleting Edges to Restrict the Size of an Epidemic in Temporal Networks. Journal of Computer and System Sciences, 119:60-77, 2021. URL: https://doi.org/10.1016/j.jcss.2021.01.007.
  21. Jessica Enright, Kitty Meeks, and Hendrik Molter. Counting Temporal Paths. Algorithmica, 87(5):736-782, 2025. URL: https://doi.org/10.1007/s00453-025-01301-3.
  22. Thomas Erlebach, Nils Morawietz, and Petra Wolf. Parameterized Algorithms for Multi-Label Periodic Temporal Graph Realization. Theoretical Computer Science, page 115412, 2025. Publisher: Elsevier. URL: https://doi.org/10.1016/j.tcs.2025.115412.
  23. Thomas Erlebach and Jakob T. Spooner. Parameterised Temporal Exploration Problems. Journal of Computer and System Sciences, 135:73-88, 2023. URL: https://doi.org/10.1016/j.jcss.2023.01.003.
  24. Till Fluschnik, Hendrik Molter, Rolf Niedermeier, Malte Renken, and Philipp Zschoche. As Time Goes By: Reflections on Treewidth for Temporal Graphs. In Fedor V. Fomin, Stefan Kratsch, and Erik Jan Van Leeuwen, editors, Treewidth, Kernels, and Algorithms, volume 12160 of Lecture Notes in Computer Science, pages 49-77. Springer International Publishing, Cham, 2020. URL: https://doi.org/10.1007/978-3-030-42071-0_6.
  25. Martin Grohe. Logic, Graphs, and Algorithms. Logic and Automata, pages 2 : 357-422, 2008. Google Scholar
  26. Martin Grohe, Stephan Kreutzer, and Sebastian Siebertz. Deciding First-Order Properties of Nowhere Dense Graphs. J. ACM, 64(3):17:1-17:32, 2017. URL: https://doi.org/10.1145/3051095.
  27. Roman Haag, Hendrik Molter, Rolf Niedermeier, and Malte Renken. Feedback Edge Sets in Temporal Graphs. Discrete Applied Mathematics, 307:65-78, 2022. Publisher: Elsevier. URL: https://doi.org/10.1016/j.dam.2021.09.029.
  28. Anton Herrmann, Christian Komusiewicz, Nils Morawietz, and Frank Sommer. Timeline Problems in Temporal Graphs: Vertex Cover vs. Dominating Set. In Akanksha Agrawal and Erik Jan van Leeuwen, editors, 20th International Symposium on Parameterized and Exact Computation (IPEC 2025), volume 358 of Leibniz International Proceedings in Informatics (LIPIcs), pages 12:1-12:18, Dagstuhl, Germany, 2025. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.IPEC.2025.12.
  29. David Kempe, Jon Kleinberg, and Amit Kumar. Connectivity and Inference Problems for Temporal Networks. Journal of Computer and System Sciences, 64(4):820-842, 2002. URL: https://doi.org/10.1006/jcss.2002.1829.
  30. Stephan Kreutzer. Algorithmic meta-theorems. In Finite and Algorithmic Model Theory, London Mathematical Society Lecture Note Series, pages 177-270. Cambridge University Press, 2011. editors: J. Esparza, C. Michaux, and C. Steinhorn. Google Scholar
  31. David C. Kutner and Laura Larios-Jones. Temporal Reachability Dominating Sets: Contagion in Temporal Graphs. Journal of Computer and System Sciences, 155:101-116, 2023. URL: https://doi.org/10.1007/978-3-031-48882-5_8.
  32. Bernard Mans and Luke Mathieson. On the Treewidth of Dynamic Graphs. Theoretical Computer Science, 554:217-228, 2014. URL: https://doi.org/10.1016/j.tcs.2013.12.024.
  33. George B. Mertzios, Hendrik Molter, Nils Morawietz, and Paul G. Spirakis. Temporal Graph Realization With Bounded Stretch. In 50th International Symposium on Mathematical Foundations of Computer Science, volume 345, pages 75:1-75:19, Dagstuhl, Germany, 2025. Leibniz International Proceedings in Informatics (LIPIcs). URL: https://doi.org/10.4230/LIPIcs.MFCS.2025.75.
  34. Jaroslav Nešetřil and Patrice Ossona De Mendez. Sparsity: Graphs, Structures, and Algorithms, volume 28 of Algorithms and Combinatorics. Springer Berlin Heidelberg, Berlin, Heidelberg, 2012. URL: https://doi.org/10.1007/978-3-642-27875-4.
  35. Philipp Zschoche, Till Fluschnik, Hendrik Molter, and Rolf Niedermeier. The Complexity of Finding Small Separators in Temporal Graphs. Journal of Computer and System Sciences, 107:72-92, 2020. URL: https://doi.org/10.1016/j.jcss.2019.07.006.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact