ABSTRACT. Despite the importance of graph theory in mathematics and computer science, there are relatively few machine-checked proofs of graph theory results and even fewer general purpose libraries. After the formalization of some basic concepts in HOL [1] and a formalization of Euler’s theorem in Mizar [12] during the 90s, the 2000s saw several results on planar graphs: Gonthier’s celebrated formal proof of the four-color theorem [9] in Coq, the formalization of tame graphs as part of the Flyspeck project [13] in Isabelle/HOL, and a study on Delaunay triangulations [8] by Dufourd and Bertot. More recently, Noschinski developed a library for both simple and multigraphs in Isabelle/HOL [14].

Over the past couple of years, Damien Pous and I have developed a graph theory library [a] for the interactive theorem prover Coq [b] based on the Mathematical Components Library [c]. The initial goal was to formalize soundness and completeness of a finite axiomatization of isomorphism for the class of labeled treewidth-two multigraphs [10], a new result answering positively – for this particular class of graphs – a question posed by Courcelle [2, page 118]. Since none of the available libraries suited our needs, we started to develop a new graph theory library [3,6,7]. Since then, there has been some renewed interest in the formalization of graph theory, both in Coq [16,15] and in other systems [11].

The development of our library and the aforementioned axiomatizability result that guided the development process highlight the fruitful interplay be- tween the development of pen-and-paper proofs and the development of machine-checked mathematical libraries. While the initial design of the library allowed us to formally verify [4] parts of the original proofs, formalizing the full proof seemed out of reach. This prompted us to develop a new pen-and-paper proof [5] that was significantly simpler and written with formalization in mind. In addition, we revised and extended the library [7], allowing us to overcome those difficulties that could not be sidestepped using the new proof. This allowed us to finally verify [6] the completeness result we initially set out to prove.

Despite the use of a graph rewrite system, the completeness proof and its formalization in Coq are elementary in the sense that we do not employ results from graph transformation theory. This is due, at least in part, to us not being familiar with these techniques and there not being any preexisting graph transformation

libraries, in particular none that would interface well with the Mathematical Components library. Further, our simple 4-rule rewrite system could still be reasoned about directly, However, for reasoning about more complex graph rewrite systems, using a more abstract approach appears necessary.

References

[a] https://coq-community.org/graph-theory/ (with contributions from Daniel Severín, Guillaume Combette and Guillaume Ambal)

[b] https://coq.inria.fr

[c] https://math-comp.github.io

1. Chou, C.: A formal theory of undirected graphs in higher-order logic. In: TPHOL. LNCS, vol. 859, pp. 144–157. Springer (1994). https://doi.org/10. 1007/3-540-58450-1_40

2. Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-Order Logic - A Language-Theoretic Approach, Encyclopedia of mathematics and its applications, vol. 138. Cambridge University Press (2012)

3. Doczkal, C.: A variant of Wagner’s theorem based on combinatorial hypermaps. In: ITP. LIPIcs, vol. 193, pp. 17:1–17:17. Dagstuhl (2021). https://doi.org/10. 4230/LIPIcs.ITP.2021.17

4. Doczkal, C., Combette, G., Pous, D.: A formal proof of the minor-exclusion prop- erty for treewidth-two graphs. In: ITP. pp. 178–195 (2018). https://doi.org/10. 1007/978-3-319-94821-8_11

5. Doczkal, C., Pous, D.: Treewidth-two graphs as a free algebra. In: MFCS. LIPIcs, vol. 117, pp. 60:1–60:15. Dagstuhl (2018). https://doi.org/10.4230/LIPIcs. MFCS.2018.60

6. Doczkal, C., Pous, D.: Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq. In: CPP. pp. 325–33. ACM (2020). https://doi.org/ 10.1145/3372885.3373831

7. Doczkal, C., Pous, D.: Graph theory in Coq: Minors, treewidth, and isomor- phisms. J. Autom. Reason. 64(5), 795–825 (2020). https://doi.org/10.1007/ s10817- 020- 09543- 2

8. Dufourd, J., Bertot, Y.: Formal study of plane Delaunay triangulation. In: ITP. LNCS, vol. 6172, pp. 211–226. Springer (2010). https://doi.org/10.1007/ 978-3-642-14052-5_16

9. Gonthier, G.: Formal proof — the four-color theorem. Notices Amer. Math. Soc. 55(11), 1382–1393 (2008)

10. Llo ́pez, E.C., Pous, D.: K4-free graphs as a free algebra. In: MFCS. LIPIcs, vol. 83, pp. 76:1–76:14. Dagstuhl (2017). https://doi.org/10.4230/LIPIcs.MFCS.2017. 76

11. Lochbihler, A.: A mechanized proof of the max-flow min-cut theorem for countable networks. In: ITP. LIPIcs, vol. 193, pp. 25:1–25:18. Dagstuhl (2021). https://doi. org/10.4230/LIPIcs.ITP.2021.25

12. Nakamura, Y., Rudnicki, P.: Euler circuits and paths. Formalized Mathematics 6(3), 417–425 (1997)

13. Nipkow, T., Bauer, G., Schultz, P.: Flyspeck I: tame graphs. In: IJCAR. LNCS, vol. 4130, pp. 21–35. Springer (2006). https://doi.org/10.1007/11814771_4

14. Noschinski, L.: A graph library for Isabelle. Mathematics in Computer Science

9(1), 23–39 (2015). https://doi.org/10.1007/s11786-014-0183-z

15. Sever ́ın, D.E.: Formalization of the Domination Chain with Weighted Parameters (Short Paper). In: ITP. LIPIcs, vol. 141, pp. 36:1–36:7. Dagstuhl (2019). https://doi.org/10.4230/LIPIcs.ITP.2019.36

16. Singh, A.K., Natarajan, R.: A constructive formalization of the weak perfect graph theorem. In: CPP. ACM (2020). https://doi.org/10.1145/3372885.3373819

ABSTRACT. We introduce a component model for graph rewriting systems that allows to represent a global system as a network of components with interfaces representing shared views of internal states and transformations, and such that their composition reconstructs the global system.

Formally and conceptually our model represents the convergence of three main ingredients: Distributed graph transformations introduced distributed graphs and their synchronised transformations. Morphisms between graph transformation systems support the modularisation of types and rules. Algebraic representations of (network) graphs as arrows in a symmetric monoidal category (and their visualisation by string diagrams) provide a syntax to describe and reason about graph rewriting components in a compositional way.

ABSTRACT. Cyber-physical systems often encompass complex concurrent behavior with timing constraints and probabilistic failures on demand. The analysis whether such systems with probabilistic timed behavior adhere to a given specification is essential. When the states of the system can be represented by graphs, the rule-based formalism of Probabilistic Timed Graph Transformation Systems (PTGTSs) can be used to suitably capture structure dynamics as well as probabilistic and timed behavior of the system. The model checking support for PTGTSs w.r.t. properties specified using Probabilistic Timed Computation Tree Logic (PTCTL) has been already presented. Moreover, for timed graph-based runtime monitoring, Metric Temporal Graph Logic (MTGL) has been developed for stating metric temporal properties on identified subgraphs and their structural changes over time.

In this paper, we (a) extend MTGL to the Probabilistic Metric Temporal Graph Logic (PMTGL) by allowing for the specification of probabilistic properties, (b) adapt our MTGL satisfaction checking approach to PTGTSs, and (c) combine the approaches for PTCTL model checking and MTGL satisfaction checking to obtain a Bounded Model Checking (BMC) approach for PMTGL. In our evaluation, we apply an implementation of our BMC approach in AutoGraph to a running example.

ABSTRACT. Reverse derivative categories (RDCs) have recently been shown to be a suitable semantic framework for studying machine learning algorithms. Whereas emphasis has been put on training methodologies, less attention has been devoted to particular model classes: the concrete categories whose morphisms represent machine learning models. In this paper we study presentations by generators and equations of classes of RDCs. In particular, we propose polynomial circuits as a suitable machine learning model. We give an axiomatisation for these circuits and prove a functional completeness result. Finally, we discuss the use of polynomial circuits over specific semirings to perform machine learning with discrete values.

ABSTRACT. Graph grammars based on contextual hyperedge replacement (CHR) extend the generative power of the well-known hyperedge replacement (HR) grammars to an extent that makes them useful for practical modeling. Recent work has shown that acyclicity is a key condition for parsing CHR grammars efficiently. In this paper we show that acyclicity of CHR grammars is decidable and that the generative power of acyclic CHR grammars lies strictly between that of HR grammars and unrestricted CHR grammars.

ABSTRACT. Resilience is a concept of rising interest in computer science and software engineering. For systems in which correctness w.r.t. a safety condition is unachievable, fast recovery is demanded. We ask whether we can reach a safe state in a bounded number of steps whenever we reach a bad state. In a well-structured framework, we investigate problems of this kind where the bad and safety condition are given as upward/downward-closed sets. We obtain decidability results for graph transformation systems by applying our results for subclasses of well-structured transition systems. Moreover, we develop sufficient criteria of graph transformation systems for the applicability of our results.