DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2026.7

Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations

Authors: Ricardo Almeida, Blair Archibald, Basile Pesin, and Michele Sevegnani

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract

Commutative regular expressions describe sets of unordered words, and are used, for example, when building type systems for process calculi. In these applications, an important operation is finding the intersection of two expressions, but no algorithm currently exists. We remedy this by proposing an algorithm for computing intersections of commutative regular expressions, which we implement and prove correct in the Rocq prover. The algorithm encodes the intersection of two expressions as systems of linear Diophantine equations, and extracts from their solution an intersection expression. To solve these systems we implement and verify the algorithm proposed by Contejean and Devie. We detail the implementation of the intersection algorithm, highlight essential aspects of the proofs (including the complex proof of termination of the equation system solver), and evaluate the OCaml-extracted solver on random and real-world commutative regular expressions.

Cite as

Ricardo Almeida, Blair Archibald, Basile Pesin, and Michele Sevegnani. Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{almeida_et_al:LIPIcs.ITP.2026.7,
  author =	{Almeida, Ricardo and Archibald, Blair and Pesin, Basile and Sevegnani, Michele},
  title =	{{Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{7:1--7:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.7},
  URN =		{urn:nbn:de:0030-drops-269813},
  doi =		{10.4230/LIPIcs.ITP.2026.7},
  annote =	{Keywords: commutative regular expressions, linear Diophantine equations, interactive theorem provers, Rocq}
}

Document

DOI: 10.4230/LIPIcs.CP.2021.15

Practical Bigraphs via Subgraph Isomorphism

Authors: Blair Archibald, Kyle Burns, Ciaran McCreesh, and Michele Sevegnani

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract

Bigraphs simultaneously model the spatial and non-spatial relationships between entities, and have been used for systems modelling in areas including biology, networking, and sensors. Temporal evolution can be modelled through a rewriting system, driven by a matching algorithm that identifies instances of bigraphs to be rewritten. The previous state-of-the-art matching algorithm for bigraphs with sharing is based on Boolean satisfiability (SAT), and suffers from a large encoding that limits scalability and makes it hard to support extensions. This work instead adapts a subgraph isomorphism solver that is based upon constraint programming to solve the bigraph matching problem. This approach continues to support bigraphs with sharing, is more open to other extensions and side constraints, and improves performance by over two orders of magnitude on a range of problem instances drawn from real-world mixed-reality, protocol, and conference models.

Cite as

Blair Archibald, Kyle Burns, Ciaran McCreesh, and Michele Sevegnani. Practical Bigraphs via Subgraph Isomorphism. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{archibald_et_al:LIPIcs.CP.2021.15,
  author =	{Archibald, Blair and Burns, Kyle and McCreesh, Ciaran and Sevegnani, Michele},
  title =	{{Practical Bigraphs via Subgraph Isomorphism}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{15:1--15:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.15},
  URN =		{urn:nbn:de:0030-drops-153068},
  doi =		{10.4230/LIPIcs.CP.2021.15},
  annote =	{Keywords: bigraphs, subgraph isomorphism, constraint programming, rewriting systems}
}

Search Results

Documents authored by Archibald, Blair

Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations

Abstract

Cite as

Practical Bigraphs via Subgraph Isomorphism

Abstract

Cite as

Thanks for your feedback!

Could not send message