Search Results

Documents authored by Sevegnani, Michele

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}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.72
Finite Models for a Spatial Logic with Discrete and Topological Path Operators

Authors: Sven Linker, Fabio Papacchini, and Michele Sevegnani

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
This paper analyses models of a spatial logic with path operators based on the class of neighbourhood spaces, also called pretopological or closure spaces, a generalisation of topological spaces. For this purpose, we distinguish two dimensions: the type of spaces on which models are built, and the type of allowed paths. For the spaces, we investigate general neighbourhood spaces and the subclass of quasi-discrete spaces, which closely resemble graphs. For the paths, we analyse the cases of quasi-discrete paths, which consist of an enumeration of points, and topological paths, based on the unit interval. We show that the logic admits finite models over quasi-discrete spaces, both with quasi-discrete and topological paths. Finally, we prove that for general neighbourhood spaces, the logic does not have the finite model property, either for quasi-discrete or topological paths.
Cite as

Sven Linker, Fabio Papacchini, and Michele Sevegnani. Finite Models for a Spatial Logic with Discrete and Topological Path Operators. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 72:1-72:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{linker_et_al:LIPIcs.MFCS.2021.72,
  author =	{Linker, Sven and Papacchini, Fabio and Sevegnani, Michele},
  title =	{{Finite Models for a Spatial Logic with Discrete and Topological Path Operators}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{72:1--72:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.72},
  URN =		{urn:nbn:de:0030-drops-145120},
  doi =		{10.4230/LIPIcs.MFCS.2021.72},
  annote =	{Keywords: spatial logic, topology, finite models}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2020.66
Analysing Spatial Properties on Neighbourhood Spaces

Authors: Sven Linker, Fabio Papacchini, and Michele Sevegnani

Published in: LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

Abstract
We present a bisimulation relation for neighbourhood spaces, a generalisation of topological spaces. We show that this notion, path preserving bisimulation, preserves formulas of the spatial logic SLCS. We then use this preservation result to show that SLCS cannot express standard topological properties such as separation and connectedness. Furthermore, we compare the bisimulation relation with standard modal bisimulation and modal bisimulation with converse on graphs and prove it coincides with the latter.
Cite as

Sven Linker, Fabio Papacchini, and Michele Sevegnani. Analysing Spatial Properties on Neighbourhood Spaces. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 66:1-66:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{linker_et_al:LIPIcs.MFCS.2020.66,
  author =	{Linker, Sven and Papacchini, Fabio and Sevegnani, Michele},
  title =	{{Analysing Spatial Properties on Neighbourhood Spaces}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{66:1--66:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-159-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{170},
  editor =	{Esparza, Javier and Kr\'{a}l', Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.66},
  URN =		{urn:nbn:de:0030-drops-127352},
  doi =		{10.4230/LIPIcs.MFCS.2020.66},
  annote =	{Keywords: spatial logic, topology, bisimulation}
}
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