Document Open Access Logo

Model Checking with Temporal Graphs and Their Derivative

Authors Binh-Minh Bui-Xuan, Florent Krasnopol , Bruno Monasson , Nathalie Sznajder

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2026.57.pdf
  • Filesize: 1 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Fixed parameter tractability
  • Mathematics of computing → Graph theory
Keywords
  • temporal graphs
  • dynamic network
  • tree decomposition
  • monadic second order logic
  • first order logic
  • derivative

Metrics

Abstract

Temporal graphs are graphs where the presence or properties of their vertices and edges change over time. When time is discrete, a temporal graph can be defined as a sequence of static graphs over a discrete time span, called lifetime, or as a single graph where each edge is associated with a specific set of time instants where the edge is alive. For static graphs, Courcelle’s Theorem asserts that any graph problem expressible in monadic second-order logic can be solved in linear time on graphs of bounded tree-width. We propose the first adaptation of Courcelle’s Theorem for monadic second-order logic on temporal graphs that does not explicitly rely on a parameter proportional to the lifetime, or defined as the maximum number of time-edges incident with any vertex which in the worst case is higher than the lifetime. We then introduce the notion of derivative over a sliding time window of a chosen size, and define the tree-width and twin-width of the temporal graph’s derivative. We exemplify its usefulness with meta-theorems with respect to a temporal variant of first-order logic. The resulting logic expresses a wide range of temporal graph problems including a version of temporal cliques, an important notion when querying time series databases for community structures.

Cite As Get BibTex

Binh-Minh Bui-Xuan, Florent Krasnopol, Bruno Monasson, and Nathalie Sznajder. Model Checking with Temporal Graphs and Their Derivative. In 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 386, pp. 57:1-57:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.MFCS.2026.57

Author Details

Binh-Minh Bui-Xuan
  • LIP6, CNRS, Sorbonne Université, Paris, France
Florent Krasnopol
  • Université de Lorraine, CNRS, Inria, LORIA, Nancy, France
Bruno Monasson
  • ENS de Lyon, France
Nathalie Sznajder
  • LIP6, CNRS, Sorbonne Université, Paris, France

Acknowledgements

We are grateful to the anonymous reviewers of all our submissions for their helpful comments which greatly improved the paper.

References

  1. Eleni C. Akrida, George B. Mertzios, Paul G. Spirakis, and Christoforos Raptopoulos. The temporal explorer who returns to the base. Journal of Computer and System Sciences, 120:179-193, September 2021. URL: https://doi.org/10.1016/j.jcss.2021.04.001.
  2. Suman Banerjee and Bithika Pal. On the enumeration of maximal (Δ, γ)-cliques of a temporal network. In Raghu Krishnapuram and Parag Singla, editors, Proceedings of the ACM India Joint International Conference on Data Science and Management of Data, COMAD/CODS 2019, Kolkata, India, January 3-5, 2019, pages 112-120. ACM, 2019. URL: https://doi.org/10.1145/3297001.3297015.
  3. Julien Baste and Binh-Minh Bui-Xuan. Temporal matching in link stream: kernel and approximation. In 16th Cologne-Twente Workshop on Graphs and Combinatorial Optimization, 2018. Google Scholar
  4. Julien Baste, Binh-Minh Bui-Xuan, and Antoine Roux. Temporal matching. Theor. Comput. Sci., 806:184-196, 2020. URL: https://doi.org/10.1016/J.TCS.2019.03.026.
  5. Pierre Bergé, Édouard Bonnet, and Hugues Déprés. Deciding Twin-Width at Most 4 Is NP-Complete. In Mikołaj Bojańczyk, Emanuela Merelli, and David P. Woodruff, editors, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022), volume 229 of Leibniz International Proceedings in Informatics (LIPIcs), pages 18:1-18:20, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2022.18.
  6. Benjamin Bergougnoux, Jan Dreier, and Lars Jaffke. A logic-based algorithmic meta-theorem for mim-width. In Nikhil Bansal and Viswanath Nagarajan, editors, Proceedings of the 2023 ACM-SIAM Symposium on Discrete Algorithms, SODA 2023, Florence, Italy, January 22-25, 2023, pages 3282-3304. SIAM, 2023. URL: https://doi.org/10.1137/1.9781611977554.CH125.
  7. Sandeep Bhadra and Afonso Ferreira. Complexity of connected components in evolving graphs and the computation of multicast trees in dynamic networks. In Samuel Pierre, Michel Barbeau, and Evangelos Kranakis, editors, Ad-Hoc, Mobile, and Wireless Networks, Second International Conference, ADHOC-NOW 2003 Montreal, Canada, October 8-10, 2003, Proceedings, volume 2865 of Lecture Notes in Computer Science, pages 259-270. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-39611-6_23.
  8. Hans L. Bodlaender. A linear-time algorithm for finding tree-decompositions of small treewidth. SIAM Journal on Computing, 25(6):1305-1317, 1996. URL: https://doi.org/10.1137/S0097539793251219.
  9. Hans L. Bodlaender, Fedor V. Fomin, Daniel Lokshtanov, Eelko Penninkx, Saket Saurabh, and Dimitrios M. Thilikos. (Meta) kernelization. J. ACM, 63(5):44:1-44:69, 2016. URL: https://doi.org/10.1145/2973749.
  10. Hans L. Bodlaender and Tom C. van der Zanden. On exploring always-connected temporal graphs of small pathwidth. Information Processing Letters, 142:68-71, February 2019. URL: https://doi.org/10.1016/j.ipl.2018.10.016.
  11. J. Adrian Bondy and Uppaluri S. R. Murty. Graph Theory. Graduate Texts in Mathematics. Springer, 2008. URL: https://doi.org/10.1007/978-1-84628-970-5.
  12. Édouard Bonnet. Coloring hardness on low twin-width graphs. CoRR, abs/2512.23680, 2025. URL: https://doi.org/10.48550/arXiv.2512.23680.
  13. Édouard Bonnet, Jan Dreier, Jakub Gajarský, Stephan Kreutzer, Nikolas Mählmann, Pierre Simon, and Szymon Toruńczyk. Model checking on interpretations of classes of bounded local cliquewidth. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '22, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3531130.3533367.
  14. Édouard Bonnet, Eun Jung Kim, Stéphan Thomassé, and Rémi Watrigant. Twin-width I: tractable FO model checking. J. ACM, 69(1):3:1-3:46, 2022. URL: https://doi.org/10.1145/3486655.
  15. Binh-Minh Bui-Xuan, Afonso Ferreira, and Aubin Jarry. Computing shortest, fastest, and foremost journeys in dynamic networks. Int. J. Found. Comput. Sci., 14(2):267-285, 2003. URL: https://doi.org/10.1142/S0129054103001728.
  16. Binh-Minh Bui-Xuan, Florent Krasnopol, Bruno Monasson, and Nathalie Sznajder. Model checking with temporal graphs and their derivative. CoRR, abs/2602.12446, 2026. URL: https://doi.org/10.48550/arXiv.2602.12446.
  17. Arnaud Casteigts, Timothée Corsini, and Writika Sarkar. Simple, strict, proper, happy: A study of reachability in temporal graphs. Theor. Comput. Sci., 991:114434, 2024. URL: https://doi.org/10.1016/J.TCS.2024.114434.
  18. Linda Cook, Eun Jung Kim, and Tomás Masarík. A tight meta-theorem for LOCAL certification of MSO2 properties within bounded treewidth graphs. In Alkida Balliu and Fabian Kuhn, editors, Proceedings of the ACM Symposium on Principles of Distributed Computing, PODC 2025, Hotel Las Brisas Huatulco, Huatulco, Mexico, June 16-20, 2025, pages 110-120. ACM, 2025. URL: https://doi.org/10.1145/3732772.3733562.
  19. Bruno Courcelle. Chapter 5 - graph rewriting: An algebraic and logic approach. In Jan Van Leeuwen, editor, Formal Models and Semantics, Handbook of Theoretical Computer Science, pages 193-242. Elsevier, Amsterdam, 1990. URL: https://doi.org/10.1016/B978-0-444-88074-1.50010-X.
  20. Bruno Courcelle and Joost Engelfriet. Graph Structure and Monadic Second-Order Logic - A Language-Theoretic Approach, volume 138 of Encyclopedia of mathematics and its applications. Cambridge University Press, 2012. URL: http://www.cambridge.org/fr/knowledge/isbn/item5758776/?site_locale=fr_FR.
  21. Bruno Courcelle, Joost Engelfriet, and Grzegorz Rozenberg. Handle-rewriting hypergraph grammars. J. Comput. Syst. Sci., 46(2):218-270, 1993. URL: https://doi.org/10.1016/0022-0000(93)90004-G.
  22. Bruno Courcelle, Johann A. Makowsky, and Udi Rotics. Linear time solvable optimization problems on graphs of bounded clique-width. Theory Comput. Syst., 33(2):125-150, 2000. URL: https://doi.org/10.1007/S002249910009.
  23. Pierluigi Crescenzi, Clémence Magnien, and Andrea Marino. Finding top-k nodes for temporal closeness in large temporal graphs. Algorithms, 13(9):211, 2020. URL: https://doi.org/10.3390/A13090211.
  24. Marek Cygan, Fedor V. Fomin, Lukasz Kowalik, Daniel Lokshtanov, Dániel Marx, Marcin Pilipczuk, Michal Pilipczuk, and Saket Saurabh. Parameterized Algorithms. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21275-3.
  25. David P. Dailey. Uniqueness of colorability and colorability of planar 4-regular graphs are np-complete. Discrete Mathematics, 30(3):289-293, 1980. URL: https://doi.org/10.1016/0012-365X(80)90236-8.
  26. Reinhard Diestel. Graph Theory, volume 173 of Graduate Texts in Mathematics. Springer Berlin Heidelberg, Berlin, Heidelberg, 6th edition, 2025. URL: https://doi.org/10.1007/978-3-662-70107-2.
  27. Michelle Döring, Jessica A. Enright, Laura Larios-Jones, and George Skretas. FO and MSO model checking on temporal graphs. In George B. Mertzios and Andréa W. Richa, editors, 5th Symposium on Algorithmic Foundations of Dynamic Networks, SAND 2026, Le Havre, France, July 1-3, 2026, volume 373 of LIPIcs, pages 9:1-9:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. URL: https://doi.org/10.4230/LIPIcs.SAND.2026.9.
  28. Rodney G. Downey and Michael R. Fellows. Parameterized Complexity. Monographs in Computer Science. Springer, 1999. URL: https://doi.org/10.1007/978-1-4612-0515-9.
  29. Jessica A. Enright, Kitty Meeks, George B. Mertzios, and Viktor Zamaraev. Deleting edges to restrict the size of an epidemic in temporal networks. J. Comput. Syst. Sci., 119:60-77, 2021. URL: https://doi.org/10.1016/J.JCSS.2021.01.007.
  30. Jörg Flum and Martin Grohe. Parameterized Complexity Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2006. URL: https://doi.org/10.1007/3-540-29953-X.
  31. 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 - Essays Dedicated to Hans L. Bodlaender on the Occasion of His 60th Birthday, volume 12160 of Lecture Notes in Computer Science, pages 49-77. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-42071-0_6.
  32. Pierre Fraigniaud, Pedro Montealegre, Ivan Rapaport, and Ioan Todinca. A meta-theorem for distributed certification. Algorithmica, 86(2):585-612, 2024. URL: https://doi.org/10.1007/S00453-023-01185-1.
  33. Markus Frick and Martin Grohe. Deciding first-order properties of locally tree-decomposable graphs. In Jirí Wiedermann, Peter van Emde Boas, and Mogens Nielsen, editors, Automata, Languages and Programming, pages 331-340, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-48523-6_30.
  34. Haim Gaifman. On Local and Non-Local Properties. In J. Stern, editor, Studies in Logic and the Foundations of Mathematics, volume 107 of Proceedings of the Herbrand Symposium, pages 105-135. Elsevier, January 1982. URL: https://doi.org/10.1016/S0049-237X(08)71879-2.
  35. Petr A. Golovach, Giannos Stamoulis, and Dimitrios M. Thilikos. Model-checking for first-order logic with disjoint paths predicates in proper minor-closed graph classes. In Nikhil Bansal and Viswanath Nagarajan, editors, Proceedings of the 2023 ACM-SIAM Symposium on Discrete Algorithms, SODA 2023, Florence, Italy, January 22-25, 2023, pages 3684-3699. SIAM, 2023. URL: https://doi.org/10.1137/1.9781611977554.CH141.
  36. Martin Grohe. Logic, graphs, and algorithms. In Jörg Flum, Erich Grädel, and Thomas Wilke, editors, Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas], volume 2 of Texts in Logic and Games, pages 357-422. Amsterdam University Press, 2008. Google Scholar
  37. Martin Grohe, Stephan Kreutzer, and Sebastian Siebertz. Deciding first-order properties of nowhere dense graphs. J. ACM, 64(3), June 2017. URL: https://doi.org/10.1145/3051095.
  38. Anne-Sophie Himmel, Hendrik Molter, Rolf Niedermeier, and Manuel Sorge. Adapting the Bron-Kerbosch algorithm for enumerating maximal cliques in temporal graphs. Soc. Netw. Anal. Min., 7(1):35:1-35:16, 2017. URL: https://doi.org/10.1007/S13278-017-0455-0.
  39. Alon Itai, Christos H. Papadimitriou, and Jayme Luiz Szwarcfiter. Hamilton paths in grid graphs. SIAM Journal on Computing, 11(4):676-686, 1982. URL: https://doi.org/10.1137/0211056.
  40. Hugo Jacob and Marcin Pilipczuk. Bounding twin-width for bounded-treewidth graphs, planar graphs, and bipartite graphs. In Michael A. Bekos and Michael Kaufmann, editors, Graph-Theoretic Concepts in Computer Science - 48th International Workshop, WG 2022, Tübingen, Germany, June 22-24, 2022, Revised Selected Papers, volume 13453 of Lecture Notes in Computer Science, pages 287-299. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-15914-5_21.
  41. Jon M. Kleinberg and Éva Tardos. Algorithm design. Addison-Wesley, 2006. Google Scholar
  42. Dusan Knop, Martin Koutecký, Tomás Masarík, and Tomás Toufar. Simplified algorithmic metatheorems beyond MSO: treewidth and neighborhood diversity. Log. Methods Comput. Sci., 15(4), 2019. URL: https://doi.org/10.23638/LMCS-15(4:12)2019.
  43. Stephan Kreutzer. Algorithmic meta-theorems. In Javier Esparza, Christian Michaux, and Charles Steinhorn, editors, Finite and Algorithmic Model Theory, volume 379 of London Mathematical Society Lecture Note Series, pages 177-270. Cambridge University Press, 2011. Google Scholar
  44. Leonid Libkin. Elements of Finite Model Theory. Springer Berlin Heidelberg, Berlin, Heidelberg, 2004. URL: https://doi.org/10.1007/978-3-662-07003-1.
  45. George B. Mertzios, Hendrik Molter, Rolf Niedermeier, Viktor Zamaraev, and Philipp Zschoche. Computing maximum matchings in temporal graphs. In Christophe Paul and Markus Bläser, editors, 37th International Symposium on Theoretical Aspects of Computer Science, STACS 2020, Montpellier, France, March 10-13, 2020, volume 154 of LIPIcs, pages 27:1-27:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.STACS.2020.27.
  46. George B. Mertzios, Hendrik Molter, Rolf Niedermeier, Viktor Zamaraev, and Philipp Zschoche. Computing maximum matchings in temporal graphs. J. Comput. Syst. Sci., 137:1-19, 2023. URL: https://doi.org/10.1016/J.JCSS.2023.04.005.
  47. Jayadev Misra and David Gries. A Constructive Proof of Vizing’s Theorem. Inf. Process. Lett., 41(3):131-133, 1992. URL: https://doi.org/10.1016/0020-0190(92)90041-S.
  48. Mehdi Naima. Temporal betweenness centrality on shortest walks variants. Appl. Netw. Sci., 10(1):11, 2025. URL: https://doi.org/10.1007/S41109-024-00685-5.
  49. Rolf Niedermeier. Invitation to Fixed-Parameter Algorithms. Oxford University Press, 2006. URL: https://doi.org/10.1093/ACPROF:OSO/9780198566076.001.0001.
  50. Sang-il Oum and Paul D. Seymour. Approximating clique-width and branch-width. J. Comb. Theory B, 96(4):514-528, 2006. URL: https://doi.org/10.1016/J.JCTB.2005.10.006.
  51. Michal Pilipczuk, Nicole Schirrmacher, Sebastian Siebertz, Szymon Torunczyk, and Alexandre Vigny. Algorithms and data structures for first-order logic with connectivity under vertex failures. In Mikolaj Bojanczyk, Emanuela Merelli, and David P. Woodruff, editors, 49th International Colloquium on Automata, Languages, and Programming, ICALP 2022, July 4-8, 2022, Paris, France, volume 229 of LIPIcs, pages 102:1-102:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.ICALP.2022.102.
  52. Neil Robertson and Paul D. Seymour. Graph minors. XIII. the disjoint paths problem. J. Comb. Theory B, 63(1):65-110, 1995. URL: https://doi.org/10.1006/JCTB.1995.1006.
  53. Sylvain Schmitz and Hugo Buffière. Locally bounded treewidth and δ-differential treewidth. Personal communication, December 2025. Google Scholar
  54. Massinissa Tighilt, Lina Azerouk, Camille Palisoc, Binh-Minh Bui-Xuan, and Maria Potop-Butucaru. Distributed computation of temporal twins in periodic undirected time-varying graphs. In Networked Systems - 13th International Conference, NETYS 2025, Proceedings, 2025, to appear. Google Scholar
  55. Tiphaine Viard, Matthieu Latapy, and Clémence Magnien. Computing maximal cliques in link streams. Theor. Comput. Sci., 609:245-252, 2016. URL: https://doi.org/10.1016/J.TCS.2015.09.030.
  56. Juan Villacis-Llobet, Binh-Minh Bui-Xuan, and Maria Potop-Butucaru. Foremost non-stop journey arrival in linear time. In Merav Parter, editor, Structural Information and Communication Complexity - 29th International Colloquium, SIROCCO 2022, Paderborn, Germany, June 27-29, 2022, Proceedings, volume 13298 of Lecture Notes in Computer Science, pages 283-301. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-09993-9_16.
  57. Philipp Zschoche, Till Fluschnik, Hendrik Molter, and Rolf Niedermeier. The complexity of finding small separators in temporal graphs. J. Comput. Syst. Sci., 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