Search Results

Documents authored by Gadducci, Fabio


Document
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
Effect Semantics for Quantum Process Calculi

Authors: Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, and Gabriele Tedeschi

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


Abstract
The development of quantum communication protocols sparked the interest in quantum extensions of process calculi and behavioural equivalences, but defining a bisimilarity that matches the observational properties of a quantum-capable system is a surprisingly difficult task. The two proposals explicitly addressing this issue, qCCS and lqCCS, do not define an algorithmic verification scheme: the bisimilarity of two processes is proven by comparing their behaviour under all input states. We introduce a new semantic model based on effects, i.e. probabilistic predicates on quantum states that represent their observable properties. We define and investigate the properties of effect distributions and effect labelled transition systems (eLTSs), generalizing probability distributions and probabilistic labelled transition systems (pLTSs), respectively. As a proof of concept, we provide an eLTS-based semantics for a minimal quantum process algebra, which we prove sound and complete with respect to the observable probabilistic behaviour of quantum processes. To the best of our knowledge, ours is the first algorithmically verifiable proposal that abides to the properties of quantum theory.

Cite as

Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, and Gabriele Tedeschi. Effect Semantics for Quantum Process Calculi. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 16:1-16:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{ceragioli_et_al:LIPIcs.CONCUR.2024.16,
  author =	{Ceragioli, Lorenzo and Gadducci, Fabio and Lomurno, Giuseppe and Tedeschi, Gabriele},
  title =	{{Effect Semantics for Quantum Process Calculi}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{16:1--16:22},
  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.16},
  URN =		{urn:nbn:de:0030-drops-207886},
  doi =		{10.4230/LIPIcs.CONCUR.2024.16},
  annote =	{Keywords: Quantum process calculi, probabilistic LTSs, effect LTSs}
}
Document
Weakly Markov Categories and Weakly Affine Monads

Authors: Tobias Fritz, Fabio Gadducci, Paolo Perrone, and Davide Trotta

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)


Abstract
Introduced in the 1990s in the context of the algebraic approach to graph rewriting, gs-monoidal categories are symmetric monoidal categories where each object is equipped with the structure of a commutative comonoid. They arise for example as Kleisli categories of commutative monads on cartesian categories, and as such they provide a general framework for effectful computation. Recently proposed in the context of categorical probability, Markov categories are gs-monoidal categories where the monoidal unit is also terminal, and they arise for example as Kleisli categories of commutative affine monads, where affine means that the monad preserves the monoidal unit. The aim of this paper is to study a new condition on the gs-monoidal structure, resulting in the concept of weakly Markov categories, which is intermediate between gs-monoidal categories and Markov ones. In a weakly Markov category, the morphisms to the monoidal unit are not necessarily unique, but form a group. As we show, these categories exhibit a rich theory of conditional independence for morphisms, generalising the known theory for Markov categories. We also introduce the corresponding notion for commutative monads, which we call weakly affine, and for which we give two equivalent characterisations. The paper argues that these monads are relevant to the study of categorical probability. A case at hand is the monad of finite non-zero measures, which is weakly affine but not affine. Such structures allow to investigate probability without normalisation within an elegant categorical framework.

Cite as

Tobias Fritz, Fabio Gadducci, Paolo Perrone, and Davide Trotta. Weakly Markov Categories and Weakly Affine Monads. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{fritz_et_al:LIPIcs.CALCO.2023.16,
  author =	{Fritz, Tobias and Gadducci, Fabio and Perrone, Paolo and Trotta, Davide},
  title =	{{Weakly Markov Categories and Weakly Affine Monads}},
  booktitle =	{10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
  pages =	{16:1--16:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-287-7},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{270},
  editor =	{Baldan, Paolo and de Paiva, Valeria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.16},
  URN =		{urn:nbn:de:0030-drops-188133},
  doi =		{10.4230/LIPIcs.CALCO.2023.16},
  annote =	{Keywords: String diagrams, gs-monoidal and Markov categories, categorical probability, affine monads}
}
Document
Complete Volume
LIPIcs, Volume 211, CALCO 2021, Complete Volume

Authors: Fabio Gadducci and Alexandra Silva

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


Abstract
LIPIcs, Volume 211, CALCO 2021, Complete Volume

Cite as

9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 1-384, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@Proceedings{gadducci_et_al:LIPIcs.CALCO.2021,
  title =	{{LIPIcs, Volume 211, CALCO 2021, Complete Volume}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{1--384},
  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},
  URN =		{urn:nbn:de:0030-drops-153544},
  doi =		{10.4230/LIPIcs.CALCO.2021},
  annote =	{Keywords: LIPIcs, Volume 211, CALCO 2021, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Fabio Gadducci and Alexandra Silva

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


Abstract
Front Matter, Table of Contents, Preface, Conference Organization

Cite as

9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{gadducci_et_al:LIPIcs.CALCO.2021.0,
  author =	{Gadducci, Fabio and Silva, Alexandra},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{0:i--0:x},
  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.0},
  URN =		{urn:nbn:de:0030-drops-153559},
  doi =		{10.4230/LIPIcs.CALCO.2021.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
A Categorical Account of Replicated Data Types

Authors: Fabio Gadducci, Hernán Melgratti, Christian Roldán, and Matteo Sammartino

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)


Abstract
Replicated Data Types (RDTs) have been introduced as a suitable abstraction for dealing with weakly consistent data stores, which may (temporarily) expose multiple, inconsistent views of their state. In the literature, RDTs are commonly specified in terms of two relations: visibility, which accounts for the different views that a store may have, and arbitration, which states the logical order imposed on the operations executed over the store. Different flavours, e.g., operational, axiomatic and functional, have recently been proposed for the specification of RDTs. In this work, we propose an algebraic characterisation of RDT specifications. We define categories of visibility relations and arbitrations, show the existence of relevant limits and colimits, and characterize RDT specifications as functors between such categories that preserve these additional structures.

Cite as

Fabio Gadducci, Hernán Melgratti, Christian Roldán, and Matteo Sammartino. A Categorical Account of Replicated Data Types. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 42:1-42:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{gadducci_et_al:LIPIcs.FSTTCS.2019.42,
  author =	{Gadducci, Fabio and Melgratti, Hern\'{a}n and Rold\'{a}n, Christian and Sammartino, Matteo},
  title =	{{A Categorical Account of Replicated Data Types}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{42:1--42:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.42},
  URN =		{urn:nbn:de:0030-drops-116042},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.42},
  annote =	{Keywords: Replicated data type, Specification, Functorial characterisation}
}
Document
Verification of Evolving Graph Structures (Dagstuhl Seminar 15451)

Authors: Parosh Aziz Abdulla, Fabio Gadducci, Barbara König, and Viktor Vafeiadis

Published in: Dagstuhl Reports, Volume 5, Issue 11 (2016)


Abstract
This report documents the programme and the outcome of Dagstuhl Seminar 15451 "Verification of Evolving Graph Structures". The aim was to bring together researchers from different communities (shape analysis, separation logic, graph transformation, verification of infinite-state systems) who are interested in developing techniques for the analysis of graph manipulations, i.e., methods that are able to handle the challenges that arise in current verification problems. Apart from scientific talks, the programme also included four tutorial talks and four working groups, which are summarized in this report.

Cite as

Parosh Aziz Abdulla, Fabio Gadducci, Barbara König, and Viktor Vafeiadis. Verification of Evolving Graph Structures (Dagstuhl Seminar 15451). In Dagstuhl Reports, Volume 5, Issue 11, pp. 1-28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@Article{azizabdulla_et_al:DagRep.5.11.1,
  author =	{Aziz Abdulla, Parosh and Gadducci, Fabio and K\"{o}nig, Barbara and Vafeiadis, Viktor},
  title =	{{Verification of Evolving Graph Structures (Dagstuhl Seminar 15451)}},
  pages =	{1--28},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{5},
  number =	{11},
  editor =	{Aziz Abdulla, Parosh and Gadducci, Fabio and K\"{o}nig, Barbara and Vafeiadis, Viktor},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.11.1},
  URN =		{urn:nbn:de:0030-drops-57614},
  doi =		{10.4230/DagRep.5.11.1},
  annote =	{Keywords: dynamic systems, graph transformation, graphs, heap analysis, separation logic, shape analysis, static analysis, verification}
}
Document
Categorical Methods at the Crossroads (Dagstuhl Perspectives Workshop 14182)

Authors: Samson Abramsky, John C. Baez, Fabio Gadducci, and Viktor Winschel

Published in: Dagstuhl Reports, Volume 4, Issue 4 (2014)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 14182 "Perspectives Workshop: Categorical Methods at the Crossroads". The aim of the meeting was to investigate the potential of category theory as a paradigm for mathematical modeling and applied science. The envisaged application areas included computation, physics, biology, complex systems, social and cognitive science and linguistics. Many of these areas were indeed tackled in the variety of topics dealt with during the workshop. Each working day followed the same structure: two survey lectures during the morning, followed by two/three shorter talks in the afternoon, and closed by a working group session. During these sessions the attendants split into several groups according to the main thematic areas that had been identified on the first day. Both surveys and talks are reported in the "Overview" section of the report, while a wrap-up of the discussions that occurred inside the working groups is reported in the "Working Groups" section.

Cite as

Samson Abramsky, John C. Baez, Fabio Gadducci, and Viktor Winschel. Categorical Methods at the Crossroads (Dagstuhl Perspectives Workshop 14182). In Dagstuhl Reports, Volume 4, Issue 4, pp. 49-63, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)


Copy BibTex To Clipboard

@Article{abramsky_et_al:DagRep.4.4.49,
  author =	{Abramsky, Samson and Baez, John C. and Gadducci, Fabio and Winschel, Viktor},
  title =	{{Categorical Methods at the Crossroads (Dagstuhl Perspectives Workshop 14182)}},
  pages =	{49--63},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{4},
  number =	{4},
  editor =	{Abramsky, Samson and Baez, John C. and Gadducci, Fabio and Winschel, Viktor},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.4.4.49},
  URN =		{urn:nbn:de:0030-drops-46189},
  doi =		{10.4230/DagRep.4.4.49},
  annote =	{Keywords: Category theory, concurrency, economics, game theory, logics, quantum computing, semantics}
}
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