DROPS

Document

DOI: 10.4230/LIPIcs.MFCS.2026.57

Model Checking with Temporal Graphs and Their Derivative

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

Published in: LIPIcs, Volume 386, 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{buixuan_et_al:LIPIcs.MFCS.2026.57,
  author =	{Bui-Xuan, Binh-Minh and Krasnopol, Florent and Monasson, Bruno and Sznajder, Nathalie},
  title =	{{Model Checking with Temporal Graphs and Their Derivative}},
  booktitle =	{51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026)},
  pages =	{57:1--57:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-442-0},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{386},
  editor =	{Kouck\'{y}, Michal and Petrișan, Daniela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2026.57},
  URN =		{urn:nbn:de:0030-drops-274393},
  doi =		{10.4230/LIPIcs.MFCS.2026.57},
  annote =	{Keywords: temporal graphs, dynamic network, tree decomposition, monadic second order logic, first order logic, derivative}
}

Document

DOI: 10.4230/LIPIcs.ITP.2025.22

Formalizing Splitting in Isabelle/HOL

Authors: Ghilain Bergeron, Florent Krasnopol, and Sophie Tourret

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract

We describe the formalization in Isabelle/HOL of a framework for splitting, a theorem proving technique that extends saturation-based calculi with branching abilities. The framework preserves the completeness of the original calculus. We focus here on the simplest splitting model and provide an extension of the ordered resolution calculus with a variant of splitting called Lightweight AVATAR.

Cite as

Ghilain Bergeron, Florent Krasnopol, and Sophie Tourret. Formalizing Splitting in Isabelle/HOL. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bergeron_et_al:LIPIcs.ITP.2025.22,
  author =	{Bergeron, Ghilain and Krasnopol, Florent and Tourret, Sophie},
  title =	{{Formalizing Splitting in Isabelle/HOL}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{22:1--22:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.22},
  URN =		{urn:nbn:de:0030-drops-246208},
  doi =		{10.4230/LIPIcs.ITP.2025.22},
  annote =	{Keywords: Isabelle/HOL, saturation-based calculi, splitting}
}

Search Results

Documents authored by Krasnopol, Florent

Model Checking with Temporal Graphs and Their Derivative

Abstract

Cite as

Formalizing Splitting in Isabelle/HOL

Abstract

Cite as

Thanks for your feedback!

Could not send message