Search Results

Documents authored by Castelnovo, Davide

Document
DOI: 10.4230/LIPIcs.CONCUR.2024.11
Left-Linear Rewriting in Adhesive Categories

Authors: Paolo Baldan, Davide Castelnovo, Andrea Corradini, and Fabio Gadducci

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
When can two sequential steps performed by a computing device be considered (causally) independent? This is a relevant question for concurrent and distributed systems, since independence means that they could be executed in any order, and potentially in parallel. Equivalences identifying rewriting sequences which differ only for independent steps are at the core of the theory of concurrency of many formalisms. We investigate the issue in the context of the double pushout approach to rewriting in the general setting of adhesive categories. While a consolidated theory exists for linear rules, which can consume, preserve and generate entities, this paper focuses on left-linear rules which may also "merge" parts of the state. This is an apparently minimal, yet technically hard enhancement, since a standard characterisation of independence that - in the linear case - allows one to derive a number of properties, essential in the development of a theory of concurrency, no longer holds. The paper performs an in-depth study of the notion of independence for left-linear rules: it introduces a novel characterisation of independence, identifies well-behaved classes of left-linear rewriting systems, and provides some fundamental results including a Church-Rosser property and the existence of canonical equivalence proofs for concurrent computations. These results properly extends the class of formalisms that can be modelled in the adhesive framework.
Cite as

Paolo Baldan, Davide Castelnovo, Andrea Corradini, and Fabio Gadducci. Left-Linear Rewriting in Adhesive Categories. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 11:1-11:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{baldan_et_al:LIPIcs.CONCUR.2024.11,
  author =	{Baldan, Paolo and Castelnovo, Davide and Corradini, Andrea and Gadducci, Fabio},
  title =	{{Left-Linear Rewriting in Adhesive Categories}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{11:1--11:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.11},
  URN =		{urn:nbn:de:0030-drops-207835},
  doi =		{10.4230/LIPIcs.CONCUR.2024.11},
  annote =	{Keywords: Adhesive categories, double-pushout rewriting, left-linear rules, switch equivalence, local Church-Rosser property}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.13
Fuzzy Algebraic Theories

Authors: Davide Castelnovo and Marino Miculan

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
In this work we propose a formal system for fuzzy algebraic reasoning. The sequent calculus we define is based on two kinds of propositions, capturing equality and existence of terms as members of a fuzzy set. We provide a sound semantics for this calculus and show that there is a notion of free model for any theory in this system, allowing us (with some restrictions) to recover models as Eilenberg-Moore algebras for some monad. We will also prove a completeness result: a formula is derivable from a given theory if and only if it is satisfied by all models of the theory. Finally, leveraging results by Milius and Urbat, we give HSP-like characterizations of subcategories of algebras which are categories of models of particular kinds of theories.
Cite as

Davide Castelnovo and Marino Miculan. Fuzzy Algebraic Theories. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{castelnovo_et_al:LIPIcs.CSL.2022.13,
  author =	{Castelnovo, Davide and Miculan, Marino},
  title =	{{Fuzzy Algebraic Theories}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{13:1--13:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.13},
  URN =		{urn:nbn:de:0030-drops-157332},
  doi =		{10.4230/LIPIcs.CSL.2022.13},
  annote =	{Keywords: categorical logic, fuzzy sets, algebraic reasoning, equational axiomatisations, monads, Eilenberg-Moore algebras}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2021.12
Closure Hyperdoctrines

Authors: Davide Castelnovo and Marino Miculan

Published in: LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

Abstract
(Pre)closure spaces are a generalization of topological spaces covering also the notion of neighbourhood in discrete structures, widely used to model and reason about spatial aspects of distributed systems. In this paper we present an abstract theoretical framework for the systematic investigation of the logical aspects of closure spaces. To this end, we introduce the notion of closure (hyper)doctrines, i.e. doctrines endowed with inflationary operators (and subject to suitable conditions). The generality and effectiveness of this concept is witnessed by many examples arising naturally from topological spaces, fuzzy sets, algebraic structures, coalgebras, and covering at once also known cases such as Kripke frames and probabilistic frames (i.e., Markov chains). By leveraging general categorical constructions, we provide axiomatisations and sound and complete semantics for various fragments of logics for closure operators. Hence, closure hyperdoctrines are useful both for refining and improving the theory of existing spatial logics, and for the definition of new spatial logics for new applications.
Cite as

Davide Castelnovo and Marino Miculan. Closure Hyperdoctrines. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 12:1-12:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{castelnovo_et_al:LIPIcs.CALCO.2021.12,
  author =	{Castelnovo, Davide and Miculan, Marino},
  title =	{{Closure Hyperdoctrines}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{12:1--12:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.12},
  URN =		{urn:nbn:de:0030-drops-153678},
  doi =		{10.4230/LIPIcs.CALCO.2021.12},
  annote =	{Keywords: categorical logic, topological semantics, closure operators, spatial logic}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact