16 Search Results for "Montanari, Ugo"

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.MFCS.2024.7
Quantum Polynomial Hierarchies: Karp-Lipton, Error Reduction, and Lower Bounds

Authors: Avantika Agarwal, Sevag Gharibian, Venkata Koppula, and Dorian Rudolph

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract
The Polynomial-Time Hierarchy (PH) is a staple of classical complexity theory, with applications spanning randomized computation to circuit lower bounds to "quantum advantage" analyses for near-term quantum computers. Quantumly, however, despite the fact that at least four definitions of quantum PH exist, it has been challenging to prove analogues for these of even basic facts from PH. This work studies three quantum-verifier based generalizations of PH, two of which are from [Gharibian, Santha, Sikora, Sundaram, Yirka, 2022] and use classical strings (QCPH) and quantum mixed states (QPH) as proofs, and one of which is new to this work, utilizing quantum pure states (QPHpure) as proofs. We first resolve several open problems from [GSSSY22], including a collapse theorem and a Karp-Lipton theorem for QCPH. Then, for our new class QPHpure, we show one-sided error reduction QPHpure, as well as the first bounds relating these quantum variants of PH, namely QCPH ⊆ QPHpure ⊆ EXP^PP.
Cite as

Avantika Agarwal, Sevag Gharibian, Venkata Koppula, and Dorian Rudolph. Quantum Polynomial Hierarchies: Karp-Lipton, Error Reduction, and Lower Bounds. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{agarwal_et_al:LIPIcs.MFCS.2024.7,
  author =	{Agarwal, Avantika and Gharibian, Sevag and Koppula, Venkata and Rudolph, Dorian},
  title =	{{Quantum Polynomial Hierarchies: Karp-Lipton, Error Reduction, and Lower Bounds}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{7:1--7:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.7},
  URN =		{urn:nbn:de:0030-drops-205632},
  doi =		{10.4230/LIPIcs.MFCS.2024.7},
  annote =	{Keywords: Quantum complexity, polynomial hierarchy}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.143
Forcing, Transition Algebras, and Calculi

Authors: Go Hashimoto, Daniel Găină, and Ionuţ Ţuţu

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
We bring forward a logical system of transition algebras that enhances many-sorted first-order logic using features from dynamic logics. The sentences we consider include compositions, unions, and transitive closures of transition relations, which are treated similarly to the actions used in dynamic logics in order to define necessity and possibility operators. This leads to a higher degree of expressivity than that of many-sorted first-order logic. For example, one can finitely axiomatize both the finiteness and the reachability of models, neither of which are ordinarily possible in many-sorted first-order logic. We introduce syntactic entailment and study basic properties such as compactness and completeness, showing that the latter does not hold when standard finitary proof rules are used. Consequently, we define proof rules having both finite and countably infinite premises, and we provide conditions under which completeness can be proved. To that end, we generalize the forcing method introduced in model theory by Robinson from a single signature to a category of signatures, and we apply it to obtain a completeness result for signatures that are at most countable.
Cite as

Go Hashimoto, Daniel Găină, and Ionuţ Ţuţu. Forcing, Transition Algebras, and Calculi. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 143:1-143:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{hashimoto_et_al:LIPIcs.ICALP.2024.143,
  author =	{Hashimoto, Go and G\u{a}in\u{a}, Daniel and \c{T}u\c{t}u, Ionu\c{t}},
  title =	{{Forcing, Transition Algebras, and Calculi}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{143:1--143:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.143},
  URN =		{urn:nbn:de:0030-drops-202868},
  doi =		{10.4230/LIPIcs.ICALP.2024.143},
  annote =	{Keywords: Forcing, institution theory, calculi, algebraic specification, transition systems}
}
Document
DOI: 10.4230/DagSemProc.05081.1
05081 Abstracts Collection – Foundations of Global Computing

Authors: José Luiz Fiadeiro, Ugo Montanari, and Martin Wirsing

Published in: Dagstuhl Seminar Proceedings, Volume 5081, Foundations of Global Computing (2006)

Abstract
From 20.02.05 to 25.02.05, the Dagstuhl Seminar 05081 on ``Foundations of Global Computing'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

José Luiz Fiadeiro, Ugo Montanari, and Martin Wirsing. 05081 Abstracts Collection – Foundations of Global Computing. In Foundations of Global Computing. Dagstuhl Seminar Proceedings, Volume 5081, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{fiadeiro_et_al:DagSemProc.05081.1,
  author =	{Fiadeiro, Jos\'{e} Luiz and Montanari, Ugo and Wirsing, Martin},
  title =	{{05081 Abstracts Collection – Foundations of Global Computing}},
  booktitle =	{Foundations of Global Computing},
  pages =	{1--16},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5081},
  editor =	{Jos\'{e} Luiz Fiadeiro and Ugo Montanari and Martin Wirsing},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05081.1},
  URN =		{urn:nbn:de:0030-drops-4590},
  doi =		{10.4230/DagSemProc.05081.1},
  annote =	{Keywords: Global Computing}
}
Document
DOI: 10.4230/DagSemProc.05081.2
Architectural Views for CommUnity

Authors: Cristóvão Oliveira and Michel Wermelinger

Published in: Dagstuhl Seminar Proceedings, Volume 5081, Foundations of Global Computing (2006)

Abstract
CommUnity and its categorical foundations provide a formal approach to Software Architecture (SA). Several concepts such as (re) configuration and (higher-order) connector have been given precise definitions in this setting. One of the cornerstones of the approach is the separation between computation, coordination and distribution. In this paper, we take this separation one step further and define explicit architectural views, one for each concern. They will be used to help to detect errors made while building the architecture. Moreover they will be a support to improve the design of the system by focusing on one concern at a time and/or by combining them with each other.
Cite as

Cristóvão Oliveira and Michel Wermelinger. Architectural Views for CommUnity. In Foundations of Global Computing. Dagstuhl Seminar Proceedings, Volume 5081, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{oliveira_et_al:DagSemProc.05081.2,
  author =	{Oliveira, Crist\'{o}v\~{a}o and Wermelinger, Michel},
  title =	{{Architectural Views for CommUnity}},
  booktitle =	{Foundations of Global Computing},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5081},
  editor =	{Jos\'{e} Luiz Fiadeiro and Ugo Montanari and Martin Wirsing},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05081.2},
  URN =		{urn:nbn:de:0030-drops-2967},
  doi =		{10.4230/DagSemProc.05081.2},
  annote =	{Keywords: Software Architecture, views, computation, coordination, distribution}
}
Document
DOI: 10.4230/DagSemProc.05081.3
Data Handover: Reconciling Message Passing and Shared Memory

Authors: Jens Gustedt

Published in: Dagstuhl Seminar Proceedings, Volume 5081, Foundations of Global Computing (2006)

Abstract
Data Handover (DHO) is a programming paradigm and interface that aims to handle data between parallel or distributed processes that mixes aspects of message passing and shared memory. It is designed to overcome the potential problems in terms of efficiency of both: (1) memory blowup and forced copies for message passing and (2) data consistency and latency problems for shared memory. Our approach attempts to be simple and easy to understand. It contents itself with just a handful of functions to cover the main aspects of coarse grained inter-operation upon data.
Cite as

Jens Gustedt. Data Handover: Reconciling Message Passing and Shared Memory. In Foundations of Global Computing. Dagstuhl Seminar Proceedings, Volume 5081, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{gustedt:DagSemProc.05081.3,
  author =	{Gustedt, Jens},
  title =	{{Data Handover: Reconciling Message Passing and Shared Memory}},
  booktitle =	{Foundations of Global Computing},
  pages =	{1--13},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5081},
  editor =	{Jos\'{e} Luiz Fiadeiro and Ugo Montanari and Martin Wirsing},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05081.3},
  URN =		{urn:nbn:de:0030-drops-2977},
  doi =		{10.4230/DagSemProc.05081.3},
  annote =	{Keywords: Efficient data management, message passing, shared memory}
}
Document
DOI: 10.4230/DagSemProc.05081.4
Injecting Distribution in CASL

Authors: Maura Cerioli and Matteo Dell'Amico

Published in: Dagstuhl Seminar Proceedings, Volume 5081, Foundations of Global Computing (2006)

Abstract
We present a first attempt at the development of a library in the specification language Casl providing primitives to represent connectivity and communication in a distributed system. The focus, in particular, is on peer-to-peer, which presents more challanges than the client-server paradigm, because of the higher degree of anarchy and the large amount of middleware providing similar but different features in support of it. From our experience on the definition of this library, we draw some methodological lessons on how to deal with the capture of complex software systems, as opposite to classical libraries representing standard or mathematical datatypes.
Cite as

Maura Cerioli and Matteo Dell'Amico. Injecting Distribution in CASL. In Foundations of Global Computing. Dagstuhl Seminar Proceedings, Volume 5081, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{cerioli_et_al:DagSemProc.05081.4,
  author =	{Cerioli, Maura and Dell'Amico, Matteo},
  title =	{{Injecting Distribution in CASL}},
  booktitle =	{Foundations of Global Computing},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5081},
  editor =	{Jos\'{e} Luiz Fiadeiro and Ugo Montanari and Martin Wirsing},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05081.4},
  URN =		{urn:nbn:de:0030-drops-2981},
  doi =		{10.4230/DagSemProc.05081.4},
  annote =	{Keywords: P2P, CASL, algebraic specification language, specification library}
}
Document
DOI: 10.4230/DagSemProc.05081.5
Insights emerged while comparing three models for global computing

Authors: Ivan Lanese and Ugo Montanari

Published in: Dagstuhl Seminar Proceedings, Volume 5081, Foundations of Global Computing (2006)

Abstract
In this paper we outline the main ideas emerged while studying a chain of mappings from emph{Fusion Calculus} to emph{logic programming}, using emph{Synchronized Hyperedge Replacement} (with both Hoare and Milner synchronizations) as intermediate step. We aim more at discussing the ideas behind the mappings than at presenting their technical details.
Cite as

Ivan Lanese and Ugo Montanari. Insights emerged while comparing three models for global computing. In Foundations of Global Computing. Dagstuhl Seminar Proceedings, Volume 5081, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{lanese_et_al:DagSemProc.05081.5,
  author =	{Lanese, Ivan and Montanari, Ugo},
  title =	{{Insights emerged while comparing three models for global computing}},
  booktitle =	{Foundations of Global Computing},
  pages =	{1--20},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5081},
  editor =	{Jos\'{e} Luiz Fiadeiro and Ugo Montanari and Martin Wirsing},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05081.5},
  URN =		{urn:nbn:de:0030-drops-2955},
  doi =		{10.4230/DagSemProc.05081.5},
  annote =	{Keywords: Fusion Calculus, graph transformation, synchronized hyperedge replacement, logic programming, mobility}
}
Document
DOI: 10.4230/DagSemProc.05081.6
MiKO---Mikado Koncurrent Objects

Authors: Francisco Martins, Liliana Salvador, Vasco T. Vasconcelos, and Luís Lopes

Published in: Dagstuhl Seminar Proceedings, Volume 5081, Foundations of Global Computing (2006)

Abstract
The motivation for the Mikado migration model is to provide programming constructs for controlling code mobility that are as independent as possible from the particular programming language used to program the code. The main idea is to regard a domain (or site, or locality), where mobile code may enter or exit, as a membrane enclosing running processes, and offering services that have to be called for entering or exiting the domain. MiKO---Mikado Koncurrent Objects is a particular instance of this model, where the membrane is explicitly split in two parts: the methods defining the interface, and a process part describing the data for, and the behavior of, the interface. The talk presents the syntax, operational semantics, and type system of MiKO, together with an example. It concludes by briefly mentioning the implementation of a language based on the calculus.
Cite as

Francisco Martins, Liliana Salvador, Vasco T. Vasconcelos, and Luís Lopes. MiKO---Mikado Koncurrent Objects. In Foundations of Global Computing. Dagstuhl Seminar Proceedings, Volume 5081, pp. 1-43, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{martins_et_al:DagSemProc.05081.6,
  author =	{Martins, Francisco and Salvador, Liliana and Vasconcelos, Vasco T. and Lopes, Lu{\'\i}s},
  title =	{{MiKO---Mikado Koncurrent Objects}},
  booktitle =	{Foundations of Global Computing},
  pages =	{1--43},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5081},
  editor =	{Jos\'{e} Luiz Fiadeiro and Ugo Montanari and Martin Wirsing},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05081.6},
  URN =		{urn:nbn:de:0030-drops-3014},
  doi =		{10.4230/DagSemProc.05081.6},
  annote =	{Keywords: Global computing, code migration, administrative domains, process calculus}
}
Document
DOI: 10.4230/DagSemProc.05081.7
Practical Techniques for Language Design and Prototyping

Authors: Mark-Oliver Stehr and Carolyn Talcott L.

Published in: Dagstuhl Seminar Proceedings, Volume 5081, Foundations of Global Computing (2006)

Abstract
Global computing involves the interplay of a vast variety of languages, but practially useful foundations for language specification and prototyping at the semantic level are lacking. In this talk we present a systematic approach consisting of three techniques: 1. A generic calculus of explicit substitutions with names (called CINNI) that allows us give a first-order representation of syntax to uniformly deal with all binding aspects. 2. An executable representation of Felleisen-style operational semantics in terms of first-order rewrite rules. 3. A logical framework, namely rewriting logic, that allows us to express (1) and (2) and, in addition, language aspects such as concurrency and non-determinism. We illustrate the use of these techniques in two applications: 1. A formal specification and analysis of PLAN, a Packet Language for Active Networks, that has been developed in the Switchware project at UPenn. This work was conducted in the scope of the DARPA Active Network Program. 2. The development of CIAO, a Calculus of Imperative Active Objects, a core language for concurrent object-oriented programming. It is especially designed to allow a the representation of practically relevant sublanguages of common object-oriented languages such as Java, C#, and C++. This second application is subject of ongoing work.
Cite as

Mark-Oliver Stehr and Carolyn Talcott L.. Practical Techniques for Language Design and Prototyping. In Foundations of Global Computing. Dagstuhl Seminar Proceedings, Volume 5081, pp. 1-38, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{stehr_et_al:DagSemProc.05081.7,
  author =	{Stehr, Mark-Oliver and Talcott L., Carolyn},
  title =	{{Practical Techniques for Language Design and Prototyping}},
  booktitle =	{Foundations of Global Computing},
  pages =	{1--38},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5081},
  editor =	{Jos\'{e} Luiz Fiadeiro and Ugo Montanari and Martin Wirsing},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05081.7},
  URN =		{urn:nbn:de:0030-drops-3006},
  doi =		{10.4230/DagSemProc.05081.7},
  annote =	{Keywords: Rewriting logic, explicit substitutions, operational semantics, active networks, active objects}
}
Document
DOI: 10.4230/DagSemProc.05081.8
Probabilistic Anonymity

Authors: Catuscia Palamidessi and Mohit Bhargava

Published in: Dagstuhl Seminar Proceedings, Volume 5081, Foundations of Global Computing (2006)

Abstract
The concept of anonymity comes into play in a wide range of situations, varying from voting and anonymous donations to postings on bulletin boards and sending mails. A formal definition of this concept has been given in literature in terms of nondeterminism. In this paper, we investigate a notion of anonymity based on probability theory, and we we discuss the relation with the nondeterministic one. We then formulate this definition in terms of observables for processes in the probabilistic $pi$-calculus, and propose a method to verify automatically the anonymity property. We illustrate the method by using the example of the dining cryptographers.
Cite as

Catuscia Palamidessi and Mohit Bhargava. Probabilistic Anonymity. In Foundations of Global Computing. Dagstuhl Seminar Proceedings, Volume 5081, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{palamidessi_et_al:DagSemProc.05081.8,
  author =	{Palamidessi, Catuscia and Bhargava, Mohit},
  title =	{{Probabilistic Anonymity}},
  booktitle =	{Foundations of Global Computing},
  pages =	{1--25},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5081},
  editor =	{Jos\'{e} Luiz Fiadeiro and Ugo Montanari and Martin Wirsing},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05081.8},
  URN =		{urn:nbn:de:0030-drops-2992},
  doi =		{10.4230/DagSemProc.05081.8},
  annote =	{Keywords: Anonymity, probability theory, process calculi}
}
Document
DOI: 10.4230/DagSemProc.04241.1
04241 Abstracts Collection – Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems

Authors: Barbara König, Ugo Montanari, and Philippa Gardner

Published in: Dagstuhl Seminar Proceedings, Volume 4241, Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems (2005)

Abstract
Recently there has been a lot of research, combining concepts of process algebra with those of the theory of graph grammars and graph transformation systems. Both can be viewed as general frameworks in which one can specify and reason about concurrent and distributed systems. There are many areas where both theories overlap and this reaches much further than just using graphs to give a graphic representation to processes. Processes in a communication network can be seen in two different ways: as terms in an algebraic theory, emphasizing their behaviour and their interaction with the environment, and as nodes (or edges) in a graph, emphasizing their topology and their connectedness. Especially topology, mobility and dynamic reconfigurations at runtime can be modelled in a very intuitive way using graph transformation. On the other hand the definition and proof of behavioural equivalences is often easier in the process algebra setting. Also standard techniques of algebraic semantics for universal constructions, refinement and compositionality can take better advantage of the process algebra representation. An important example where the combined theory is more convenient than both alternatives is for defining the concurrent (noninterleaving), abstract semantics of distributed systems. Here graph transformations lack abstraction and process algebras lack expressiveness. Another important example is the work on bigraphical reactive systems with the aim of deriving a labelled transitions system from an unlabelled reactive system such that the resulting bisimilarity is a congruence. Here, graphs seem to be a convenient framework, in which this theory can be stated and developed. So, although it is the central aim of both frameworks to model and reason about concurrent systems, the semantics of processes can have a very different flavour in these theories. Research in this area aims at combining the advantages of both frameworks and translating concepts of one theory into the other. The Dagsuthl Seminar, which took place from 06.06. to 11.06.2004, was aimed at bringing together researchers of the two communities in order to share their ideas and develop new concepts. These proceedings4 of the do not only contain abstracts of the talks given at the seminar, but also summaries of topics of central interest. We would like to thank all participants of the seminar for coming and sharing their ideas and everybody who has contributed to the proceedings.
Cite as

Barbara König, Ugo Montanari, and Philippa Gardner. 04241 Abstracts Collection – Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems. In Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems. Dagstuhl Seminar Proceedings, Volume 4241, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{konig_et_al:DagSemProc.04241.1,
  author =	{K\"{o}nig, Barbara and Montanari, Ugo and Gardner, Philippa},
  title =	{{04241 Abstracts Collection – Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems}},
  booktitle =	{Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{4241},
  editor =	{Barbara K\"{o}nig and Ugo Montanari and Philippa Gardner},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.04241.1},
  URN =		{urn:nbn:de:0030-drops-279},
  doi =		{10.4230/DagSemProc.04241.1},
  annote =	{Keywords: graph transformation , process calculi}
}
Document
DOI: 10.4230/DagSemProc.04241.2
Summary 1: Adhesivity, Bigraphs and Bisimulation Congruences

Authors: Pawel Sobocinski

Published in: Dagstuhl Seminar Proceedings, Volume 4241, Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems (2005)

Abstract
This paper is intended as a short informal summary of some of the topics which arose at the Dagstuhl meeting held 6/06/04-11/06/04. In particular, we shall summarise some of the content of talks by H. Ehrig, F. Gadducci, O. H. Jensen, R. Milner, B. K�¶nig, V. Sassone and the author. The general areas include adhesive categories and generalisations, contextual labelled transition semantics for graph transformation systems via borrowed-contexts and GIPOs, and bigraphs. We shall conclude with a summary of some of the discussions which followed the aforementioned presentations.
Cite as

Pawel Sobocinski. Summary 1: Adhesivity, Bigraphs and Bisimulation Congruences. In Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems. Dagstuhl Seminar Proceedings, Volume 4241, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{sobocinski:DagSemProc.04241.2,
  author =	{Sobocinski, Pawel},
  title =	{{Summary 1: Adhesivity, Bigraphs and Bisimulation Congruences}},
  booktitle =	{Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems},
  pages =	{1--12},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{4241},
  editor =	{Barbara K\"{o}nig and Ugo Montanari and Philippa Gardner},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.04241.2},
  URN =		{urn:nbn:de:0030-drops-286},
  doi =		{10.4230/DagSemProc.04241.2},
  annote =	{Keywords: graph transformation , category theory , bisimulation}
}
Document
DOI: 10.4230/DagSemProc.04241.3
Summary 2: Graph Grammar Verification through Abstraction

Authors: Paolo Baldan, Barbara König, and Arend Rensink

Published in: Dagstuhl Seminar Proceedings, Volume 4241, Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems (2005)

Abstract
Until now there have been few contributions concerning the verification of graph grammars, specifically of infinite-state graph grammars. This paper compares two existing approaches, based on abstractions of graph transformation systems. While in the unfolding approach graph grammars are approximated by Petri nets, in the partitioning approach graphs are abstracted according to their local structure. We describe differences and similarities of the two approaches and explain the underlying ideas.
Cite as

Paolo Baldan, Barbara König, and Arend Rensink. Summary 2: Graph Grammar Verification through Abstraction. In Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems. Dagstuhl Seminar Proceedings, Volume 4241, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{baldan_et_al:DagSemProc.04241.3,
  author =	{Baldan, Paolo and K\"{o}nig, Barbara and Rensink, Arend},
  title =	{{Summary 2: Graph Grammar Verification through Abstraction}},
  booktitle =	{Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems},
  pages =	{1--9},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{4241},
  editor =	{Barbara K\"{o}nig and Ugo Montanari and Philippa Gardner},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.04241.3},
  URN =		{urn:nbn:de:0030-drops-291},
  doi =		{10.4230/DagSemProc.04241.3},
  annote =	{Keywords: graph transformation , verification}
}
Document
DOI: 10.4230/DagSemProc.04241.4
Summary 3: On Graph(ic) Encodings

Authors: Roberto Bruni and Ivan Lanese

Published in: Dagstuhl Seminar Proceedings, Volume 4241, Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems (2005)

Abstract
This paper is an informal summary of different encoding techniques from process calculi and distributed formalisms to graphic frameworks. The survey includes the use of solo diagrams, term graphs, synchronized hyperedge replacement systems, bigraphs, tile models and interactive systems, all presented at the Dagstuhl Seminar 04241. The common theme of all techniques recalled here is having a graphic presentation that, at the same time, gives both an intuitive visual rendering (of processes, states, etc.) and a rigorous mathematical framework.
Cite as

Roberto Bruni and Ivan Lanese. Summary 3: On Graph(ic) Encodings. In Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems. Dagstuhl Seminar Proceedings, Volume 4241, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{bruni_et_al:DagSemProc.04241.4,
  author =	{Bruni, Roberto and Lanese, Ivan},
  title =	{{Summary 3: On Graph(ic) Encodings}},
  booktitle =	{Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{4241},
  editor =	{Barbara K\"{o}nig and Ugo Montanari and Philippa Gardner},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.04241.4},
  URN =		{urn:nbn:de:0030-drops-303},
  doi =		{10.4230/DagSemProc.04241.4},
  annote =	{Keywords: graph transformation , process calculi , encodings}
}
  • Refine by Author
  • 4 Montanari, Ugo
  • 2 Baldan, Paolo
  • 2 König, Barbara
  • 2 Lanese, Ivan
  • 1 Agarwal, Avantika
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Equational logic and rewriting
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Models of computation
  • 1 Theory of computation → Proof theory
  • 1 Theory of computation → Quantum complexity theory
  • Show More...

  • Refine by Keyword
  • 5 graph transformation
  • 3 process calculi
  • 1 Adhesive categories
  • 1 Anonymity
  • 1 CASL
  • Show More...

  • Refine by Type
  • 16 document

  • Refine by Publication Year
  • 8 2006
  • 4 2005
  • 3 2024
  • 1 1996

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