Publications by Roberto Bruni

As a contributing author of the documents listed in this page, I have made available our work electronically to ensure timely dissemination of scientific and technical contributions on a non-commercial basis. Nevertheless, copyright and all rights therein are maintained by the authors or by other copyright holders (e.g., the publisher). It is understood that all persons accessing this information will adhere to the appropriate copyright rules. In particular, these works may not be reposted without the explicit permission of the copyright holder.

Note: This page has been generated on-the-fly from a search page.

© Springer Verlag - DOI http://dx.doi.org/10.1007/978-3-642-17322-6_4

"On gs-monoidal theories for graphs with nesting",
Roberto Bruni, Andrea Corradini, Fabio Gadducci, Alberto Lluch-Lafuente, and Ugo Montanari,
in Proceedings of FMN 2009, Graph Transformations and Model-Driven Engineering: Essays Dedicated to Manfred Nagl on the Occasion of his 65th Birthday,
(Gregor Engels, Claus Lewerentz, Wilhelm Schafer, Andy Schurr and Bernhard Westfechtel, Editors),
Lecture Notes in Computer Science 5765, pages 59-86, Springer Verlag, 2010.
ISBN 978-3-642-17321-9.

Keywords: Hierarchical graphs, gs-monoidal theories, term-graphs

(Postscript) (PDF)

Abstract
We propose a sound and complete axiomatisation of a class of graphs with nesting and either locally or globally restricted nodes. Such graphs allow to represent explicitly and at the right level of abstraction some relevant topological and logical features of models and systems, including nesting, hierarchies, sharing of resources, and pointers or links. We also provide an encoding of the proposed algebra into terms of a gs-monoidal theory, and through these into a suitable class of well-scoped term graphs, showing that this encoding is sound and complete with respect to the axioms of the algebra.

"An Algebra of Hierarchical Graphs and its Application to Structural Encoding",
Roberto Bruni, Fabio Gadducci, and Alberto Lluch-Lafuente,
Scientific Annals of Computer Science XX:pages 53-96, Alexandru Ioan Cuza University of Iasi, Romania, 2010.
ISSN 1843-8121 (October 2010).
Extends the WS-FM09 and the TGC10 papers.
Open access availability at http://www.info.uaic.ro/bin/download/Annals/XX/XX_2.pdf.

Keywords: Hierarchical graphs, process calculi

Abstract
We define an algebraic theory of hierarchical graphs, whose axioms characterise graph isomorphism: two terms are equated exactly when they represent the same graph. Our algebra can be understood as a high-level language for describing graphs with a node-sharing, embedding structure, and it is then well suited for defining graphical representations of software models where nesting and linking are key aspects. In particular, we propose the use of our graph formalism as a convenient way to describe configurations in process calculi equipped with inherently hierarchical features such as sessions, locations, transactions, membranes or ambients. The graph syntax can be seen as an intermediate representation language, that facilitates the encodings of algebraic specifications, since it provides primitives for nesting, name restriction and parallel composition. In addition, proving soundness and correctness of an encoding (i.e. proving that structurally equivalent processes are mapped to isomorphic graphs) becomes easier as it can be done by induction over the graph syntax.

© EASST

"Modeling a Service and Session Calculus with Hierarchical Graph Transformation",
Roberto Bruni, Andrea Corradini, and Ugo Montanari,
in Proceedings of GraMoT 2010, International Colloquium on Graph and Model Transformation, On the occasion of the 65th birthday of Hartmut Ehrig,
(Claudia Ermel, Hartmut Ehrig, Fernando Orejas, Gabriele Taentzer, Editors), 11-12 February 2010, Berlin, Germany,
Electronic Communications of the EASST 30, 18 pages, European Association of Software Science and Technology (EASST), 2010.
ISSN 1863-2122.
Transparencies Part 1: power point.
Transparencies Part 2: power point.

Keywords: Hierarchical graphs, service oriented architecture, process calculi, CaSPiS

(Postscript) (PDF)

Abstract
Graph transformation techniques have been applied successfully to the modelling of process calculi, for example for equipping them with a truly concurrent semantics. Recently, there has been an increasing interest towards hierarchical structures both at the level of graph-based models, in order to represent explicitly the interplay between linking and containment (like in Milner's bigraphs), and at the level of process calculi, in order to deal with several logical notions of scoping (ambients, sessions and transactions, among others). In this paper we show how to encode a sophisticated calculus of services and nested sessions by exploiting a suitable flavour of hierarchical graphs. For the encoding of the processes of this calculus we benefit from a recently proposed algebra of graphs with nesting.

© Springer Verlag - DOI http://dx.doi.org/10.1007/978-3-642-15640-3_14

"An algebra of hierarchical graphs",
Roberto Bruni, Fabio Gadducci and Alberto Lluch-Lafuente,
in Proceedings of TGC 2010, 5th Symposium on Trustworthy Global Computing,
(Martin Hofmann, Martin Wirsing, Axel Rauschmayer, Editors), 22-25 February 2010, Munich, Germany,
Lecture Notes in Computer Science 6084, pages 205-221, Springer Verlag, 2010.
ISBN 978-3-642-15639-7.
Transparencies: PDF.

Keywords: Hierarchical graphs, process calculi

(Postscript) (PDF)

Abstract
We define an algebraic theory of hierarchical graphs, whose axioms characterise graph isomorphism: two terms are equated exactly when they represent the same graph. Our algebra can be understood as a high-level language for describing graphs with a node-sharing, embedding structure, and it is then well suited for defining graphical representations of software models where nesting and linking are key aspects.

© Springer Verlag - DOI http://dx.doi.org/10.1007/978-3-642-14458-5_3

"A Graph Syntax for Processes and Services",
Roberto Bruni, Fabio Gadducci and Alberto Lluch-Lafuente,
in Proceedings of WS-FM 2009, 6th International Workshop on Web Services and Formal Methods,
(Cosimo Laneve, Jianwen Su, Editors), 4-5 September 2009, Bologna, Italy,
Lecture Notes in Computer Science 6194, pages 46-60, Springer Verlag, 2010.
ISBN 978-3-642-14457-8.
Transparencies: PDF.

Keywords: Hierarchical graphs, process calculi

(Postscript) (PDF)

Abstract
We propose a class of hierarchical graphs equipped with a simple algebraic syntax as a convenient way to describe configurations in languages with inherently hierarchical features such as sessions, fault-handling scopes or transactions. The graph syntax can be seen as an intermediate representation language, that facilitates the encoding of structured specifications and, in particular, of process calculi, since it provides primitives for nesting, name restriction and parallel composition. The syntax is based on an algebraic presentation that faithfully characterises families of hierarchical graphs, meaning that each term of the language uniquely identifies an equivalence class of graphs (modulo graph isomorphism). Proving soundness and correctness of an encoding (i.e. proving that structurally equivalent processes are mapped to isomorphic graphs) is then facilitated and can be done by structural induction. Summing up, the graph syntax facilitates the definition of faithful encodings, yet allowing a precise visual representation. We illustrate our work with an application to a workflow language and a service-oriented calculus.

"Rewriting nested graphs, through term graphs (abstract)",
Roberto Bruni, Andrea Corradini, Fabio Gadducci, Alberto Lluch Lafuente and Ugo Montanari,
in Proceedings of WADT 2010, 20th International Workshop on Algebraic Development Techniques,
1-4 July 2010, Schloss Etelsen, Germany,
pages 54-56, 2010.
Pre-Proceedings.
Transparencies: PDF / Open Office Impress.

Keywords: Hierarchical graphs, service oriented architecture, process calculi, gs-monoidal theories, term graphs, mobile ambients

(Postscript) (PDF)

Abstract
We present an algebra for graphs with nesting and restriction features as a handy linear syntax for denoting a class of hierarchical graphs. We discuss how such graphs can be encoded into term graphs, showing that through this translation we can borrow definitions and results from the established theory of term graph rewriting.

"On the Semantics of Distributed Compensations with Interruption (abstract)",
Roberto Bruni, Anne Kersten and Ivan Lanese,
in Proceedings of WADT 2010, 20th International Workshop on Algebraic Development Techniques,
1-4 July 2010, Schloss Etelsen, Germany,
pages 47-48, 2010.
Pre-Proceedings.
Transparencies: PDF.

Keywords: Sagas, cCSP, concurrent semantics, compensations, long-running transactions

(Postscript) (PDF)

Abstract
We propose new, optimal, operational and denotational semantics for parallel Sagas with interruption and prove the correspondence between the two. The new semantics guarantees that distributed compensations may only be observed after a fault actually occurred.

© Springer Verlag - DOI http://dx.doi.org/10.1007/978-3-642-13464-7_2

"Exploiting the hierarchical structure of rule-based specifications for decision planning",
Artur Boronat, Roberto Bruni, Alberto Lluch-Lafuente, Ugo Montanari, and Generoso Paolillo,
in Proceedings of FMOODS & FORTE 2010, IFIP International Conference on Formal Techniques for Distributed Systems,
(John Hatcliff, Elena Zucca, Editors), 7-10 June 2010, Amsterdam, The Netherlands,
Lecture Notes in Computer Science 6117, pages 2-16, Springer Verlag, 2010.
ISBN 978-3-642-13463-0.
Transparencies: PDF / Open Office Impress.

Keywords: Rule-based specifications, hierarchical models, MOF, multi-criteria optimisation, Maude

(Postscript) (PDF)

Abstract
Rule-based specifications have been very successful as a declarative approach in many domains, due to the handy yet solid foundations offered by rule-based machineries like term and graph rewriting. Realistic problems, however, call for suitable techniques to guarantee scalability. For instance, many domains exhibit a hierarchical structure that can be exploited conveniently. This is particularly evident for composition associations of models. We propose an explicit representation of such structured models and a methodology that exploits it for the description and analysis of model- and rule-based systems. The approach is presented in the framework of rewriting logic and its efficient implementation in the rewrite engine Maude and is illustrated with a case study.

© Springer Verlag - DOI http://dx.doi.org/10.1007/978-3-642-10383-4_34

"A service-oriented UML profile with formal support",
Roberto Bruni, Matthias Hoelzl, Nora Koch, Alberto Lluch-Lafuente, Philip Mayer, Ugo Montanari and Andreas Schroeder,
in Proceedings of ICSOC/ServiceWave 2009, 7th International Joint Conference on Service-Oriented Computing,
(Luciano Baresi, Chi-Hung Chi, Jun Suzuki, Editors), 23-27 November 2009, Stockholm, Sweden,
Lecture Notes in Computer Science 5900, pages 455-469, Springer Verlag, 2009.
ISBN 978-3-642-10382-7.
Transparencies: PDF.

Keywords: Service oriented systems, Software engineering, UML4SOA, ADR

(Postscript) (PDF)

Abstract
We present a UML Profile for the description of service oriented applications. The profile focuses on style-based design and reconfiguration aspects at the architectural level. Moreover, it has formal support in terms of an approach called Architectural Design Rewriting, which enables formal analysis of the UML specifications. We show how our prototypical implementation can be used to analyse and verify properties of a service oriented application.

© EASST

"Ten virtues of structured graphs",
Roberto Bruni, Alberto Lluch-Lafuente,
in Proceedings of GT-VMT 2009, 8th International Workshop on Graph Transformation and Visual Modeling Techniques,
(Reiko Heckel, Artur Boronat, Editors), 28-29 March 2009, York, UK,
Electronic Communications of the EASST 18, 20 pages, European Association of Software Science and Technology (EASST), 2009.
ISSN 1863-2122.
Transparencies: PDF.

Keywords: Hierarchical graphs, software architectures, ADR

(Postscript) (PDF)

Abstract
This paper extends the invited talk by the first author about the virtues of structured graphs. The motivation behind the talk and this paper relies on our experience on the development of ADR, a formal approach for the design of style-conformant, reconfigurable software systems. ADR is based on hierarchical graphs with interfaces and it has been conceived in the attempt of reconciling software architectures and process calculi by means of graphical methods. We have tried to write an ADR agnostic paper where we raise some drawbacks of flat, unstructured graphs for the design and analysis of software systems and we argue that hierarchical, structured graphs can alleviate such drawbacks.

"Models for Open Transactions (extended abstract)",
Roberto Bruni and Ugo Montanari,
Technical Report Research Report n. 358, Department of Informatics, University of Oslo, 2009.
Pre-proceedings of FLACOS 2009, 3rd Workshop on Formal Languages and Analysis of Contract-Oriented Software, 24-45 September 2009, Toledo, Spain (Gordon J. Pace, Gerardo Schneider, Editors).
Published September 2009.
ISBN 82-7368-345-1.
ISSN 0806-3036.

Keywords: Petri nets, Workflow nets, Zero-safe nets, Contracts, Unfolding, Non-deterministic processes

(Postscript) (PDF)

Abstract
Loosely coupled interactions permeate modern distributed systems, where autonomous applications need to collaborate by dynamical assembly. We can single out three different phases occurring in every collaboration: 1) negotiation of some sort of contracts, mediating the needs of prospective participants; 2) acceptance or rejection of the contract; 3) contract-guarantee execution. The above scheme, called NCE for short (Negotiation, Commit, Execution), covers a wide range of situations, ranging from sessions and transactions to proof-carrying code. In the paper we concentrate on the notion of open transaction and on Zero-Safe Nets, a model developed by the authors for modelling long transactions. We extend the latter to cover the three-phase process above.

© Springer Verlag - DOI http://dx.doi.org/10.1007/978-3-642-03459-6_5

"Static Detection of Logic Flaws in Service-Oriented Applications",
Chiara Bodei, Linda Brodo, Roberto Bruni,
in Proceedings of ARSPA-WITS 2009, Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security,
(Pierpaolo Degano, Luca Viganò, Editors), 28-29 March 2009, York, UK,
Lecture Notes in Computer Science 5511, pages 70-87, Springer Verlag, 2009.
ISBN 978-3-642-03458-9.
Transparencies: PDF.

Keywords: Control Flow Analysis, Service Oriented Computing, CaSPiS

(Postscript) (PDF)

Abstract
Application or business logic, used in the development of services, has to do with the operations that define the application functionalities and not with the platform ones. Often security problems can be found at this level, because circumventing or misusing the required operations can lead to unexpected behaviour or to attacks, called {em application logic attacks}. We investigate this issue, by using the CaSPiS calculus to model services, and by providing a Control Flow Analysis able to detect and prevent some possible misuses.

© Springer Verlag - DOI http://dx.doi.org/10.1007/978-3-642-03429-9_4

"Tiles for Reo",
Farhad Arbab, Roberto Bruni, Dave Clarke, Ivan Lanese, and Ugo Montanari,
in Proceedings of WADT 2008, 19th International Workshop on Algebraic Development Techniques,
(Andrea Corradini, Ugo Montanari, Editors), 13-16 June 2008, Pisa, Italy,
Lecture Notes in Computer Science 5486, pages 37-55, Springer Verlag, 2009.
ISBN 978-3-642-03428-2.
Transparencies: power point.

Keywords: Reo, Tile model

(Postscript) (PDF)

Abstract
Reo is an exogenous coordination model for software components. The informal semantics of Reo has been matched by several proposals of formalization, exploiting co-algebraic techniques, constraint-automata, and coloring tables. We aim to show that the Tile Model offers a flexible and adequate semantic setting for Reo, such that: (i) it is able to capture context-aware behavior; (ii) it is equipped with a natural notion of behavioral equivalence which is compositional; (iii) it offers a uniform setting for representing not only the ordinary execution of Reo systems but also dynamic reconfiguration strategies.

© Springer Verlag - DOI http://dx.doi.org/10.1007/978-3-642-01918-0_1

"Calculi for Service Oriented Computing",
Roberto Bruni,
in Proceedings of SFM-WS 2009, 9th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Web Services,
(Marco Bernardo, Luca Padovani, Gianluigi Zavattaro, Editors), 1-6 June 2009, Bertinoro, Italy,
Lecture Notes in Computer Science 5569, pages 1-41, Springer Verlag, 2009.
ISBN 978-3-642-01917-3.
Transparencies: PDF.

Keywords: CCS, pi-calculus, Orc, CaSPiS, services, sessions, transactions

(Postscript) (PDF)

Abstract
It is widely recognised that process calculi stay to concurrent computing as lambda-calculus stays to sequential computing; in fact, they lay abstract, rigorous foundations for the analysis of interactive, communicating systems. Nowadays, the increasing popularity of Service-Oriented Computing (SOC) challenges the quest for novel abstractions tailored to the well-disciplined handling of specific issues, like long running interactions, orchestration, and unexpected events. In fact, these features emerge neatly in most SOC applications and need to be studied as first-class aspects, whereas they would be obfuscated if dealt with by sophisticated encoding in traditional process calculi. This paper overviews some of the most recent proposals emerged in the literature, pointing out their main characteristics and presents in more detail one such proposal, called caspis, by providing several examples to give evidence of its flexibility. No prior acquaintance with process calculi is assumed, indeed a gentle introduction to their basics is provided before the more advanced material be presented.

© Springer Verlag - DOI http://dx.doi.org/10.1007/978-3-642-00945-7_5

"Provably correct implementations of services",
Roberto Bruni, Rocco De Nicola, Michele Loreti and Leonardo Gaetano Mezzina,
in Proceedings of TGC 2008, 4th Symposium on Trustworthy Global Computing,
(Christos Kaklamanis, Flemming Nielson, Editors), 3-4 November 2008, Barcelona, Spain,
Lecture Notes in Computer Science 5474, pages 69-86, Springer Verlag, 2008.
ISBN 978-3-642-00944-0.
Transparencies: PDF.

Keywords: Concurrency, abstract machine, process calculi, services, sessions

(Postscript) (PDF)

Abstract
A number of formalisms have been defined to support the specification and analysis of service oriented applications. These formalisms have been equipped with tools (types or logics) to guarantee the correct behavior of the specified services. Due to the semantic gap between the specification formalism and the programming languages of service oriented overlay computers a critical issue is guaranteeing that correctness is preserved when running the specified systems over available implementations. We have defined a service oriented abstract machine, equipped with a formal structural semantics, that can be used to implement service specification formalisms. We use our abstract machine to implement different service oriented formalisms that have been recently proposed, each posing specific challenges that we can address successfully. By exploiting the SOS semantics of the abstract machine and those of the considered service oriented formalisms we do prove that our implementations are correct (sound and complete). We also discuss possible implementations of other formalisms.

© Elsevier Science - DOI http://dx.doi.org/10.1016/j.entcs.2009.06.038

"On symbolic semantics for name-decorated contexts",
Andrea Bracciali, Roberto Bruni, and Alberto Lluch-Lafuente,
in Proceedings of ICE 2008, 1st Interaction and Concurrency Experience,
(Filippo Bonchi, David Grohmann, Paola Spoletini, Angelo Troina, Emilio Tuosto, Editors), 6 July 2008, Reykjavik, Iceland,
Electronic Notes in Theoretical Computer Science 229.3, pages 37-58, Elsevier Science, 2009.
ISSN 1571-0661 (published July 2009).
Transparencies: PDF.

Keywords: Open systems, Abstract Semantics, Nominal Calculi, Type Systems

(Postscript) (PDF)

Abstract
Under several regards, various of the recently proposed computational paradigms are open-ended, i.e. they may comprise components whose behaviour is not or cannot be fully specified. For instance, applications can be distributed across different administration domains that do not fully disclose their internal business processes to each other, or the dynamics of the system may allow reconfigurations and dynamic bindings whose specification is not available at design time. While a large set of mature design and analysis techniques for closed systems have been developed, their lifting to the open case is not always straightforward. Some existing approaches in the process calculi community are based on the need of proving properties for components that may hold in any, or significantly many, execution environments. Dually, frameworks describing the dynamics of systems with unspecified components have also been presented. In this paper we lay some preliminary ideas on how to extend a symbolic semantics model for open systems in order to deal with name-based calculi. Moreover, we also discuss how the use of a simple type system based on name-decoration for unknown components can improve the expressiveness of the framework. The approach is illustrated on a simple, paradigmatic calculus of web crawlers, which can be understood as a term representation of a simple class of graphs.

© Elsevier Science - DOI http://dx.doi.org/10.1016/j.entcs.2009.05.012

"Hierarchical Design Rewriting with Maude",
Roberto Bruni, Alberto Lluch-Lafuente, and Ugo Montanari,
in Proceedings of WRLA 2008, 7th International Workshop on Rewriting Logic and its Applications,
(Grigore Rosu, Editor), 29-30 March 2008, Budapest, Hungary,
Electronic Notes in Theoretical Computer Science 238.3, pages 45-62, Elsevier Science, 2009.
ISSN 1571-0661 (published June 2009).
Transparencies: PDF.

Keywords: Maude, Rewriting Logic, SOS, Graphs, Software Architectures, ADR

(Postscript) (PDF)

Abstract
Architectural Design Rewriting (ADR) is a rule-based approach for the design of dynamic software architectures. The key features that make ADR a suitable and expressive framework are the algebraic presentation and the use of conditional rewrite rules. These features enable, e.g. hierarchical (top-down, bottom-up or composition-based) design and inductively-defined reconfigurations. The contribution of this paper is twofold: we define Hierarchical Design Rewriting (HDR) and present our prototypical tool support. HDR is a flavour of ADR that exploits the concept of hierarchical graph to deal with system specifications combining both symbolic and interpreted parts. Our prototypical implementation is based on Maude and its presentation serves several purposes. First, we show that HDR is not only a well-founded formal approach but also a tool-supported framework for the design and analysis of software architectures. Second, our illustration tailored to a particular algebra of designs and a particular scenario traces a general methodology for the reuse and exploitation of ADR concepts in other scenarios.

© Springer Verlag - DOI http://dx.doi.org/10.1007/978-3-540-79980-1_8

"Types and deadlock freedom in a calculus of services, sessions and pipelines",
Roberto Bruni and Leonardo Gaetano Mezzina,
in Proceedings of AMAST 2008, 12th International Conference on Algebraic Methodology and Software Technology,
(Grigore Rosu, José Meseguer, Editors), 28-31 July 2008, Urbana, Illinois, USA,
Lecture Notes in Computer Science 5140, pages 100-115, Springer Verlag, 2008.
ISBN 978-3-540-79979-5.
Transparencies: PDF.
Talk given at the Workshop on Calculi for Service Oriented Computing: PDF.

Keywords: Behavioural type systems, Deadlock freedom, Dyadic sessions, Service oriented calculi, SCC

(Postscript) (PDF)

Abstract
The notion of a session is fundamental in service-oriented applications, as it serves to separate interactions between clients and different instances of the same service, and to group together logical units of work. Recently, the Service Centered Calculus (SCC) has been proposed as a process calculus designed around the concept of a dyadic session between a service side and an invoker side, where interaction protocols and service orchestration can be conveniently expressed. In this paper we propose a generic type system to collect services' behaviours and then we fix a class of well-typed processes that are guaranteed to be deadlock free, in the sense that they either diverge by invoking new service instances or reach a normal form. The type system is based on previous research on traditional mobile calculi, here conveniently extended and simplified thanks to the neat discipline imposed by the linguistic primitives of SCC.

© Elsevier Science - DOI http://dx.doi.org/10.1016/j.tcs.2008.04.029

"Parametric Synchronizations in Mobile Nominal Calculi",
Roberto Bruni and Ivan Lanese,
Theoretical Computer Science 402(2-3):pages 102-119, Elsevier Science, 2008.
ISSN 0304-3975 (August 2008).
Extends a TGC 2006 paper.
Contact the author(s) for a free reprint.

Keywords: Process calculi, name mobility, synchronization algebra with mobility, operational semantics, bisimulation congruences, pi-calculus, Fusion calculus.

Abstract
We present and compare P-PRISMA and F-PRISMA, two parametric calculi that can be instantiated with different interaction policies, defined as synchronization algebras with mobility of names (SAMs). In particular, P-PRISMA is based on name transmission (P-SAM), like pi-calculus, and thus exploits directional (input-output) communication only, while F-PRISMA is based on name fusion (F-SAM), like Fusion calculus, and thus exploits a more symmetric form of communication. However, P-PRISMA and F-PRISMA can easily accommodate many other high-level synchronization mechanisms than the basic ones available in pi-calculus and Fusion, hence allowing for the development of a general meta-theory of mobile calculi. We define for both the labeled operational semantics and a form of strong bisimilarity, showing that the latter is compositional for any SAM. We also discuss reduction semantics and weak bisimilarity. We give several examples based on heterogeneous SAMs, we investigate the case studies of pi-calculus and Fusion calculus giving correspondence theorems, and we show how P-PRISMA can be encoded in F-PRISMA. Finally, we show that basic categorical tools can help to relate and to compose SAMs and PRISMA processes in an elegant way.

© Elsevier Science - DOI http://dx.doi.org/10.1016/j.entcs.2008.04.073

"Modelling Dynamic Software Architectures using Typed Graph Grammars",
Roberto Bruni, Antonio Bucchiarone, Stefania Gnesi and Hernán Melgratti,
in Proceedings of GT-VC 2007, 3rd Workshop on Graph Transformation for Verification and Concurrency,
(Barbara Koenig, Reiko Heckel, Arend Rensink, Editors), 3 September 2007, Lisbon, Portugal,
Electronic Notes in Theoretical Computer Science 213.1, pages 39-53, Elsevier Science, 2008.
ISSN 1571-0661 (published May 2008).

Keywords: Dynamic software architectures, graph grammars, automotive software systems

(Postscript) (PDF)

Abstract
Several recent research efforts have focused on the dynamic aspects of software architectures providing suitable models and techniques for handling the run-time modification of the structure of a system. A large number of heterogeneous proposals for addressing dynamic architectures at many different levels of abstraction have been provided, such as programmable, ad-hoc, self-healing and self-repairing among others. It is then important to have a clear picture of the relations among these proposals by formulating them into a uniform framework and contrasting the different verification aspects that can be reasonably addressed by each proposal. Our work is a contribution in this line. In particular, we map several notions of dynamicity into the same formal framework in order to distill the similarities and differences among them. As a result we explain different styles of architectural dynamisms in term of graph grammars and get some better insights on the kinds of formal properties that can be naturally associated to such different specification styles. We take a simple automotive scenario as a running example to illustrate main ideas.

© Springer Verlag - DOI http://dx.doi.org/10.1007/978-3-540-68679-8_4

"Graph-Based Design and Analysis of Dynamic Software Architectures",
Roberto Bruni, Antonio Bucchiarone, Stefania Gnesi, Dan Hirsch, and Alberto Lluch-Lafuente,
in Proceedings of Colloquium in Honour of Ugo Montanari, Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday,
(Rocco De Nicola, Pierpaolo Degano, José Meseguer, Editors), 12 June 2008, Pisa, Italy,
Lecture Notes in Computer Science 5065, pages 37-56, Springer Verlag, 2008.
ISBN 978-3-540-68676-7.

Keywords: Maude, Alloy, Rewriting Logic, SOS, Graphs, Software Architectures, ADR

(Postscript) (PDF)

Abstract
We illustrate two ways to address the specification, modelling and analysis of dynamic software architectures using: i) ordinary typed graph transformation techniques implemented in Alloy; ii) a process algebraic presentation of graph transformation implemented in Maude. The two approaches are compared by showing how different aspects can be tackled, including representation issues, modelling phases, property specification and analysis.

"Tiles for Reo (extended abstract)",
Farhad Arbab, Roberto Bruni, Dave Clarke, Ivan Lanese, and Ugo Montanari,
Technical Report TR-08-15, Computer Science Department, University of Pisa, 2008.
Pre-proceedings of WADT 2008, 19th International Workshop on Algebraic Development Techniques, 13-16 June 2008, Pisa, Italy (Andrea Corradini, Fabio Gadducci, Editors).
Published 9 June 2008.
Transparencies: power point.

Keywords: Reo, Tile model

(Postscript) (PDF)

Abstract
Reo is an exogenous coordination model for software components. The informal Reo's semantics has been matched by several proposals of formalisation, exploiting co-algebraic techniques, constraint-automata, and colouring tables. We aim to show that the Tile Model offers a flexible and adequate semantic setting for Reo. The definition of a tile semantics for Reo has specific features: (i) concurrency aspects can be taken into account; (ii) tile bisimilarity and tile trace equivalence offer standard abstract equivalences; and (iii) meta-theoretical results can be exploited to guarantee that tile bisimilarity is a congruence, thus reconciling the algebraic and co-algebraic views of connectors. Finally, we observe that the Tile Model can offer a uniform setting for representing not only the ordinary execution of Reo systems but also dynamic reconfiguration strategies.

© Springer Verlag - DOI http://dx.doi.org/10.1007/978-3-540-68863-1_3

"Sessions and Pipelines for Structured Service Programming",
Michele Boreale, Roberto Bruni, Rocco De Nicola, and Michele Loreti,
in Proceedings of FMOODS 2008, 10th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems,
(Gilles Barthe, Frank de Boer, Editors), 4-6 June 2008, Oslo, Norway,
Lecture Notes in Computer Science 5051, pages 19-38, Springer Verlag, 2008.
ISBN 978-3-540-68862-4.
Transparencies: PDF.

Keywords: Service oriented calculi, pipelines, nested sessions, process calculi, SCC, CaSPiS

(Postscript) (PDF)

Abstract
Service-oriented computing is calling for novel computational models and languages with primitives for client-server interaction, orchestration and unexpected events handling. We present CaSPiS, a process calculus where the notions of session and pipelining play a central role. Sessions are two-sided and can be equipped with protocols executed by each side. Pipelining permits orchestrating the flow of data produced by different sessions. The calculus is also equipped with operators for handling (unexpected) termination of the partner's side of a session. Several examples are presented to provide evidence for the flexibility of the chosen set of primitives. Our main result shows that in CaSPiS it is possible to program a graceful termination of nested sessions, which guarantees that no session is forced to hang forever after the loss of its partner.

"Towards trustworthy multiparty sessions (extended abstract)",
Roberto Bruni, Ivan Lanese, Hernán Melgratti, Leonardo Gaetano Mezzina, and Emilio Tuosto,
Technical Report TR-08-14, Departamento de Informatica, Universidade Nova de Lisboa, 2008.
Pre-proceedings PLACES 2008, 1st Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, 7 June 2008, Oslo, Norway (Nobuko Yoshida, Vasco T. Vaconcelos, Editors).
Transparencies: PDF.

Keywords: Multiparty sessions, Process calculi, Service composition, Type system, Compatibility

(Postscript) (PDF)

Abstract
Muse (after MUltiparty SEssions) is a process calculus for expressing computations where endpoints dynamically join existing multiparty sessions. We consider muse without name passing and intra-site communication and sketch a type system aimed to guarantee a weak form of compatibility, in the sense that all the interactions required by each local task can be provided either by endpoints currently participating to its session or by endpoints that can join that session later.

© Springer Verlag - DOI http://dx.doi.org/10.1007/978-3-540-68265-3_5

"Multiparty sessions in SOC",
Roberto Bruni, Ivan Lanese, Hernán Melgratti, and Emilio Tuosto,
in Proceedings of COORDINATION 2008, 10th International Conference on Coordination Models and Languages,
(Doug Lea, Gianluigi Zavattaro, Editors), 4-6 June 2008, Oslo, Norway,
Lecture Notes in Computer Science 5052, pages 67-82, Springer Verlag, 2008.
ISBN 978-3-540-68264-6.

Keywords: Multiparty sessions, Process calculi, Service composition

(Postscript) (PDF)

Abstract
Service oriented applications feature interactions among several participants over the network. Mechanisms such as correlation sets and two-party sessions have been proposed in the literature to separate messages sent to different instances of the same service. This paper presents a process calculus featuring dynamically evolving multiparty sessions to model interactions that spread over several participants. The calculus also provides primitives for service definition/invocation and for structured communication in order to highlight the interactions among the different concepts. Several examples from the SOC area show the suitability of our approach.

"Architectural Design Rewriting as an Architecture Description Language",
Roberto Bruni, Alberto Lluch-Lafuente, Ugo Montanari, and Emilio Tuosto,
in Proceedings of R2D2 2008, The Rise and Rise of the Declarative Datacentre,
(Karthik Bhargavan, Andy Gordon, Tim Harris, Peter Toft, Editors), 12-13 May 2008, Cambridge, UK,
pages 15-16, Technical Report Microsoft Research MSR-TR-2008-61, Microsoft Research Cambridge, 2008.
Transparencies: PDF.

Keywords: Hierarchical Design, Software Architectures, Style-preserving Reconfigurations, ADR

(Postscript) (PDF)

Abstract
Architectural Design Rewriting (ADR) is a declarative rule-based approach for the design of dynamic software architectures. The key features that make ADR a suitable and expressive framework are the algebraic presentation of graph-based structures and the use of conditional rewrite rules. These features enable the modelling of, e.g. hierarchical design, inductively defined reconfigurations and ordinary computation. Here, we promote ADR as an Architectural Description Language.

"Types and deadlock free sessions for SCC",
Roberto Bruni and Leonardo Gaetano Mezzina,
Technical Report TR-08-05, Computer Science Department, University of Pisa, 2008.
Published 3 April 2008.

Keywords: Behavioural type systems, Deadlock freedom, Dyadic sessions, Service oriented calculi, SCC

(Postscript) (PDF)

Abstract
The notion of a session is fundamental in service oriented applications, as it serves to separate interactions between different instances of the same services, and to group together logical units of work. Recently, SCC has been proposed as a calculus centered around the concept of a dyadic session, where service interaction protocols and service orchestration can be conveniently expressed. In this paper we propose a generic type system to collect services' behaviors and then we fix a class of well typed processes that are guaranteed to be deadlock free. The type system is based on previous research on traditional mobile calculi, here conveniently extended and simplified thanks to the neat discipline imposed by the linguistic primitives of SCC.

© Springer Verlag - DOI http://dx.doi.org/10.1007/978-3-540-78663-4_14

"Service Oriented Architectural Design",
Roberto Bruni, Alberto Lluch-Lafuente, Ugo Montanari, and Emilio Tuosto,
in Proceedings of TGC 2007, 3rd Symposium on Trustworthy Global Computing,
(Gilles Barthe, Cédric Fournet, Editors), 5-6 November 2007, Sophia-Antipolis, France,
Lecture Notes in Computer Science 4912, pages 186-203, Springer Verlag, 2008.
ISBN 978-3-540-78662-7.
Transparencies: PDF.

Keywords: Hierarchical Design, Software Architectures, Style-preserving Reconfigurations, ADR

(Postscript) (PDF)

Abstract
We propose Architectural Design Rewriting (ADR), an approach to formalise the development and reconfiguration of software architectures based on term-rewriting. An architectural style consists of a set of architectural elements and operations called productions which define the well-formed compositions of architectures. Roughly, a term built out of such ingredients constitutes the proof that a design was constructed according to the style, and the value of the term is the constructed software architecture. A main advantage of ADR is that it naturally supports style-preserving reconfigurations. The usefulness of our approach is shown by applying ADR to SRML, an emergent paradigm inspired by the Service Component Architecture. We model the complex operation that composes several SRML modules in a single one by means of suitable rewrite rules. Our approach guarantees that the resulting module respects SRML's metamodel.

© European Association for Theoretical Computer Science

"Style-Based Architectural Reconfigurations",
Roberto Bruni, Alberto Lluch-Lafuente, Ugo Montanari, and Emilio Tuosto,
Bulletin of the EATCS 94:pages 161-180, 2008.
ISSN 0252-9742 (February 2008).
Several PDF presentations on ADR are available:

• June 2007
• September 2007
• January 2008
• March 2008

Keywords: Software Architectures, Architectural Styles, Reconfiguration, Graphs, Term Rewriting, ADR

(Postscript) (PDF)

Abstract
We introduce Architectural Design Rewriting (ADR), an approach to the design of reconfigurable software architectures whose key features are: (i) rule-based approach (over graphs); (ii) hierarchical design; (iii) algebraic presentation; and (iv) inductively-defined reconfigurations. Architectures are modelled by graphs whose edges and nodes represent components and connection ports. Architectures are designed hierarchically by a set of edge replacement rules that fix the architectural style. Depending on their reading, productions allow: (i) top-down design by refinement, (ii) bottom-up typing of actual architectures, and (iii) well-formed composition of architectures. The key idea is to encode style proofs as terms and to exploit such information at run-time for guiding reconfigurations. The main advantages of ADR are that: (i) instead of reasoning on flat architectures, ADR specifications provide a convenient hierarchical structure, by exploiting the architectural classes introduced by the style, (ii) complex reconfiguration schemes can be defined inductively, and (iii) style-preservation is guaranteed.

© Springer Verlag - DOI http://dx.doi.org/10.1007/978-3-540-75336-0_9

"PRISMA: A mobile calculus with parameterized synchronization",
Roberto Bruni and Ivan Lanese,
in Proceedings of TGC 2006, 2nd Symposium on Trustworthy Global Computing,
(Ugo Montanari, Don Sannella, Roberto Bruni, Editors), 7-9 November 2006, Lucca, Italy,
Lecture Notes in Computer Science 4661, pages 132-149, Springer Verlag, 2006.
ISBN 978-3-540-75333-9.
Transparencies: power point.

Keywords: Synchronization algebras, mobile calculi, bisimilarity congruences, fusion calculus, category theory

(Postscript) (PDF)

Abstract
We present PRISMA, a parametric calculus that can be instantiated with different interaction policies, defined as synchronization algebras with mobility of names (SAMs). We define both operational semantics and observational semantics of PRISMA, showing that the second one is compositional for any SAM. We give examples based on heterogeneous SAMs, a case study on Fusion Calculus and some simple applications. Finally, we show that basic categorical tools can help to relate and to compose SAMs and PRISMA processes in an elegant way.

© Elsevier Science - DOI http://dx.doi.org/10.1016/j.tcs.2007.09.004

"A Semantic Framework for Open Processes",
Paolo Baldan, Andrea Bracciali, and Roberto Bruni,
Theoretical Computer Science 389(3):pages 446-483, Elsevier Science, 2007.
ISSN 0304-3975 (December 2007).
Extends an AMAST 2002 paper.
Contact the author(s) for a free reprint.

Keywords: Open systems, symbolic bisimulation, unification

Abstract
We propose a general methodology for analysing the behaviour of open systems modelled as coordinators, i.e., open terms of suitable process calculi. A coordinator is understood as a process with holes or place-holders where other coordinators and components (i.e., closed terms) can be plugged in, thus influencing its behaviour. The operational semantics of coordinators is given by means of a symbolic transition system, where states are coordinators and transitions are labelled by spatial/modal formulae expressing the potential interaction that plugged components may enable. Behavioural equivalences for coordinators, like strong and weak bisimilarities, can be straightforwardly defined over such a transition system. Differently from other approaches based on universal closures, i.e., where two coordinators are considered equivalent when all their closed instances are equivalent, our semantics preserves the openness of the system during its evolution, thus allowing dynamic instantiation to be accounted for in the semantics. To further support the adequacy of the construction, we show that our symbolic equivalences provide correct approximations of their universally closed counterparts, coinciding with them over closed components. For process calculi in suitable formats, we show how tractable symbolic semantics can be defined constructively using unification.

"Style-based architectural reconfigurations",
Roberto Bruni, Alberto Lluch-Lafuente, Ugo Montanari and Emilio Tuosto,
Technical Report TR-07-17, Computer Science Department, University of Pisa, 2007.
Published 31 July 2007.

Keywords: Software Architectures, Architectural Styles, Reconfiguration, Graphs, Term Rewriting, ADR

(Postscript) (PDF)

Abstract
We introduce Architectural Design Rewriting (ADR), an approach to deal with the design of reconfigurable software architectures. The key features we promote are: (i) rule-based approach (over graphs); (ii) hierarchical design; (iii) algebraic presentation; and (iv) inductively-defined reconfigurations. Architectures are suitably modeled by graphs whose edges and nodes respectively represent components and connection ports. Architectures are designed hierarchically by a set of edge replacement rules that fix the architectural style. Depending on their reading, productions allow: (i) top-down design by refinement, (ii) bottom-up typing of actual architectures, and (iii) well-formed composition of architectures. The key idea is to encode style proofs as terms and to exploit such information at run-time for guiding reconfigurations. The main advantages of ADR are that: (i) instead of reasoning on flat architectures, ADR specifications provide a convenient hierarchical structure, by exploiting the architectural classes introduced by the style, (ii) complex reconfiguration schemes can be defined inductively, and (iii) style-preservation is guaranteed.

© Springer Verlag - DOI http://dx.doi.org/10.1007/978-3-540-73433-8_19

"Deducing Interactions in Partially Unspecified Biological Systems",
Paolo Baldan, Andrea Bracciali, Linda Brodo and Roberto Bruni,
in Proceedings of AB 2007, 2nd International Conference on Algebraic Biology,
(Hirokazu Anai, Katsuhisa Horimoto, Temur Kutsia, Editors), 2-4 July 2007, Hagenberg (Linz), Austria,
Lecture Notes in Computer Science 4545, pages 262-276, Springer Verlag, 2007.
ISBN 978-3-540-73432-1.
Transparencies: PDF.

Keywords: Biological systems, Brane calculus, symbolic evolution

(Postscript) (PDF)

Abstract
We show how a symbolic approach to the semantics of process algebras can be fruitfully applied to the modeling and analysis of partially unspecified biological systems, i.e., systems whose components are not fully known, cannot be described entirely, or whose functioning is not completely understood. This adds a novel deductive perspective to the use of process algebras within systems biology: the investigation of the behavioural or structural properties that unspecified components must satisfy to interact within the system. These can be computationally inferred, extending the effectiveness of the in silico experiments. The use of the approach is illustrated by means of case studies.

© Elsevier Science - DOI http://dx.doi.org/10.1016/j.entcs.2006.10.044

"Prototype platforms for distributed agreements",
Alberto Baragatti, Roberto Bruni, Hernán Melgratti, Ugo Montanari and Giorgio Spagnolo,
in Proceedings of FOCLASA 2004, 3rd International Workshop on Foundations of Coordination Languages and Software Architectures,
(Antonio Brogi, Jean-Marie Jacquet, Ernesto Pimentel, Editors), 30 August 2004, London, UK,
Electronic Notes in Theoretical Computer Science 180.2, pages 21-40, Elsevier Science, 2007.
ISSN 1571-0661 (published 26 June 2007).
Transparencies: open office or power point or PDF.

Keywords: Distributed negotiations, mobile ad-hoc networks, JoCaml, Polyphonic C#, D2PC

(Postscript) (PDF)

Abstract
We present a prototype application for coordinating distributed agreements in multi-parties negotiations, where participants can dynamically join ongoing negotiations and where participants know only those parties they have interacted with. Our prototype is tailored to Ad-Hoc network scenarios involving the assignment of tasks for a rescue team operating over disaster areas. Our application is based on asynchronous communication and it exploits the D2PC protocol for committing or aborting a negotiation. Parties have been developed both in Jocaml+Perl and Polyphonic C#. The implementation of the commit protocol allows components of both types to participate within the same negotiation.

© EASST

"Event Structure Semantics for Dynamic Graph Grammars",
Roberto Bruni, Hernán Melgratti and Ugo Montanari,
in Proceedings of PNGT 2006, Workshop on Petri Nets and Graph Transformation,
(Paolo Baldan, Hartmut Ehrig, Julia Padberg, Grzegorz Rozenberg), 21-22 September 2006, Natal, Brasil,
Electronic Communications of the EASST 2, 20 pages, European Association of Software Science and Technology (EASST), 2007.
ISSN 1863-2122.

Keywords: Dynamic graph grammars, event structures, join calculus

(PDF)

Abstract
Dynamic graph grammars (DGGs) are a reflexive extension of Graph Grammars that have been introduced to represent mobile reflexive systems and calculi at a convenient level of abstraction. Persistent graph grammars (PGGs) are a class of graph grammars that admits a fully satisfactory concurrent semantics thanks to the fact that all so-called asymmetric conflicts (between items that are read by some productions and consumed by other) are avoided. In this paper we introduce a slight variant of DGGs, called persistent dynamic graph grammars (PDGGs), that can be encoded in PGGs preserving concurrency. Finally, PDGGs are exploited to define a concurrent semantics for the join calculus enriched with persistent messaging (if preferred, the latter can be naively seen as dynamic nets with read arcs).

© Elsevier Science - DOI http://dx.doi.org/10.1016/j.tcs.2006.07.005

"A Basic Algebra of Stateless Connectors",
Roberto Bruni, Ivan Lanese, and Ugo Montanari,
Theoretical Computer Science 366(1-2):pages 98-120, Elsevier Science, 2006.
ISSN 0304-3975 (November 2006).
Extends a CALCO 2005 paper.
Contact the author(s) for a free reprint.

Keywords: Connectors, synchronization, axiomatization, normal form

Abstract
The conceptual separation between computation and coordination in distributed computing systems motivates the use of peculiar entities commonly called connectors, whose task is managing the interaction among distributed components. Different kinds of connectors exist in the literature at different levels of abstraction. We focus on an algebra of connectors that exploits five kinds of basic connectors (plus their duals), namely symmetry, synchronization, mutual exclusion, hiding and inaction. Basic connectors can be composed in series and in parallel. We first define the operational, observational and denotational semantics of connectors, then we show that the observational and denotational semantics coincide and finally we give a complete normal-form axiomatization. The expressiveness of the framework is witnessed by the ability to model all the (stateless) connectors of the architectural design language CommUnity and of the coordination language Reo.

© Springer Verlag - DOI http://dx.doi.org/10.1007/11841883_17

"Dynamic Graph Transformation Systems",
Roberto Bruni and Hernán Melgratti,
in Proceedings of ICGT 2006, 3rd International Conference on Graph Transformation,
(Andrea Corradini, Hartmut Ehrig, Ugo Montanari, Leila Ribeiro and Gregor Rozenberg, Editors), 17-23 September 2006, Natal, Rio Grande do Norte, Brazil,
Lecture Notes in Computer Science 4178, pages 230-244, Springer Verlag, 2006.
ISBN 3-540-38870-2.
Transparencies: power point.

Keywords: Dynamic graph grammars, reflexivity, join calculus

(Postscript) (PDF)

Abstract
We introduce an extension of Graph Grammars (GGs), called Dynamic Graph Grammars (DynGGs), where the right-hand side of a production can spawn fresh parts of the type graph and fresh productions operating on it. The features of DynGGs make them suitable for the straightforward modeling of reflexive mobile systems like dynamic nets and the join calculus. Our main result shows that each DynGG can be modeled as a (finite) GG, so that the dynamically generated structure can be typed statically, still preserving exactly all derivations.

© Springer Verlag - DOI http://dx.doi.org/10.1007/11841197_3

"SCC: a Service Centered Calculus",
Michele Boreale, Roberto Bruni, Luis Caires, Rocco De Nicola, Ivan Lanese, Michele Loreti, Francisco Martins, Ugo Montanari, Antonio Ravara, Davide Sangiorgi, Vasco Vasconcelos, and Gianluigi Zavattaro,
in Proceedings of WS-FM 2006, 3rd International Workshop on Web Services and Formal Methods,
(Mario Bravetti, Manuel Núñez, Gianluigi Zavattaro, Editors), 8-9 September 2006, Vienna, Austria,
Lecture Notes in Computer Science 4184, pages 38-57, Springer Verlag, 2006.
ISBN 3-540-38862-1.
Transparencies: PDF.

Keywords: Service Oriented Computing, interaction protocols, SCC, PSC, Orc

(Postscript) (PDF)

Abstract
We seek for a small set of primitives that might serve as a basis for formalising and programming {service} oriented applications over global computers. As an outcome of this study we introduce here SCC, a process calculus that features explicit notions of service definition, service invocation and session handling. Our proposal has been influenced by Orc, a programming model for structured orchestration of services, but the SCC's session handling mechanism allows for the definition of structured interaction protocols, more complex than the basic request-response provided by Orc. We present syntax and operational semantics of SCC and a number of simple but nontrivial programming examples that demonstrate flexibility of the chosen set of primitives. A few encodings are also provided to relate our proposal with existing ones.

© Springer Verlag - DOI http://dx.doi.org/10.1007/11841197_8

"Translating Orc features into Petri Nets and Join Calculus",
Roberto Bruni, Hernán Melgratti and Emilio Tuosto,
in Proceedings of WS-FM 2006, 3rd International Workshop on Web Services and Formal Methods,
(Mario Bravetti, Manuel Núñez, Gianluigi Zavattaro, Editors), 8-9 September 2006, Vienna, Austria,
Lecture Notes in Computer Science 4184, pages 123-137, Springer Verlag, 2006.
ISBN 3-540-38862-1.
Transparencies: power point.

Keywords: Orc, Petri nets, reset arcs, inhibitor arcs, join calculus

(Postscript) (PDF)

Abstract
Cook and Misra's Orc is an elegant language for orchestrating distributed services, able to cover e.g. van der Aalst's workflow patterns. We aim to understand the key novel features of Orc by comparing it with variations of Petri nets. The comparison shows that Orc hides powerful mechanisms for name handling (creation and passing) and for atomic distributed termination. Petri nets with static topology can encode Orc under severe restrictions while the full language (up to a more realistic cancellation strategy) can be encoded in join (that can be seen as a higher-order extension of Petri nets). As an overall result, we promote join calculus as an elegant language embedding orchestration and computation.

© Springer Verlag - DOI http://dx.doi.org/10.1007/11817949_20

"Event Structure Semantics for Nominal Calculi",
Roberto Bruni, Hernán Melgratti and Ugo Montanari,
in Proceedings of CONCUR 2006, 17th International Conference on Concurrency Theory,
(Christel Baier, Holger Hermanns, Editors), 27-30 August 2006, Bonn, Germany,
Lecture Notes in Computer Science 4137, pages 295-309, Springer Verlag, 2006.
ISBN 3-540-37376-4.
Transparencies: PDF.

Keywords: Event structures, persistent graph grammars, Join calculus, pi-calculus

(Postscript) (PDF)

Abstract
Event structures have been used for giving true concurrent semantics to languages and models of concurrency such as CCS, Petri nets and graph grammars. Although certain nominal calculi have been modeled with graph grammars, and hence their event structure semantics could be obtained as instances of the general case, the main limitation is that in the case of graph grammars the construction is more complex than strictly necessary for dealing with usual nominal calculi and, speaking in categorical terms, it is not as elegant as in the case of Petri nets. The main contribution of this work is the definition of a particular class of graph grammars, called persistent, that are expressive enough to model name passing calculi while simplifying the denotational domain construction, which can be expressed as an adjunction. Finally, we apply our technique to derive event structure semantics for pi-calculus and join-calculus processes.

© Elsevier Science - DOI http://dx.doi.org/10.1016/j.tcs.2006.04.012

"Semantic foundations for generalized rewrite theories",
Roberto Bruni and José Meseguer,
Theoretical Computer Science 360:pages 386-414, Elsevier Science, 2006.
ISSN 0304-3975 (August 2006).
Extends a ICALP 2003 paper.
Contact the author(s) for a free reprint.

Keywords: Conditional rewriting logic, Frozen operators, Partial Membership Equational Logic, Concurrent semantics

Abstract
Since its introduction, more than one decade ago, rewriting logic has attracted the interest of both theorists and practitioners, who have contributed in showing its generality as a semantic and logical framework and also as a programming paradigm. The experimentation conducted in these years has suggested that some significant extensions to the original definition of the logic would be very useful in practice. In particular, the Maude system now supports subsorting and conditional sentences in the equational logic for data, and also frozen arguments to block undesired nested rewrites; moreover, it allows equality and membership assertions in rule conditions. In this paper, we give a detailed presentation of the inference rules, model theory, and completeness of such generalized rewrite theories.

© Springer Verlag - DOI http://dx.doi.org/10.1007/11767589_7

"Non-sequential behaviour of dynamic nets",
Roberto Bruni and Hernán Melgratti,
in Proceedings of ATPN 2006, 27th International Conference on Application and Theory of Petri Nets and Other Models Of Councurrency,
(Susanna Donatelli, P. S. Thiagarajan, Editors), 26-30 June 2006, Turku, Finland,
Lecture Notes in Computer Science 4024, pages 105-124, Springer Verlag, 2006.
ISBN 3-540-34699-6.
Transparencies: PDF.

Keywords: Dynamic nets, process semantics, unfolding semantics

(Postscript) (PDF)

Abstract
Dynamic nets are an extension of Petri nets where the net topology may change dynamically. This is achieved by allowing (i) tokens to be coloured with place names (carried on as data), (ii) transitions to designate places where to spawn new tokens on the basis of the colours in the fetched tokens, and (iii) firings to add fresh places and transitions to the net. Dynamic nets have been given step or interleaving semantics but, to the best of our knowledge, their non-sequential truly concurrent semantics has not been addressed in the literature. To fill this gap, we extend the ordinary notions of processes and unfolding to dynamic nets, providing two different constructions: (i) a specific process and unfolding for a particular initial marking, and (ii) processes and unfolding patterns that abstract away from the colours of the token initially available.

© Springer Verlag - DOI http://dx.doi.org/10.1007/11549970_20

"From Theory to Practice in Transactional Composition of Web Services",
Roberto Bruni, Gianluigi Ferrari, Hernán Melgratti, Ugo Montanari, Daniele Strollo and Emilio Tuosto,
in Proceedings of WS-FM 2005, 2nd International Workshop on Web Services and Formal Methods,
(Mario Bravetti, Leila Kloul, Gianluigi Zavattaro, Editors), 1-3 September 2005, Versailles, France,
Lecture Notes in Computer Science 3670, pages 272-286, Springer Verlag, 2005.
ISBN 3-540-28701-9 (August 2005).
Transparencies: power point.

Keywords: Flow composition, compensation, trace semantics, JTWS

(Postscript) (PDF)

Abstract
We address the problem of composing Web Services in long-running transactional business processes, where compensations must be dealt with appropriately. The framework presented in this paper is a Java API called Java Transactional Web Services (JTWS), which provides suitable primitives for wrapping and invoking Web Services as activities in long-running transactions. JTWS adheres to a process calculi formalisation of long-running transactions, called Sagas, which fixes unambiguously the implemented compensation policy. In particular, the primitives provided by JTWS are in one-to-one correspondence with the primitives of Sagas, and they are abstract enough to hide the complex details of their realization, thus favouring usability. Moreover, JTWS orchestrates business processes in a distributed way.

© Springer Verlag - DOI http://dx.doi.org/10.1007/11539452_30

"Comparing two approaches to compensable flow composition",
Roberto Bruni, Michael Butler, Carla Ferreira, Tony Hoare, Hernán Melgratti and Ugo Montanari,
in Proceedings of CONCUR 2005, 16th International Conference on Concurrency Theory,
(Martín Abadi, Luca de Alfaro, Editors), 23-26 August 2005, San Francisco, CA, USA,
Lecture Notes in Computer Science 3653, pages 383-397, Springer Verlag, 2005.
ISBN 3-540-28309-9 (August 2005).
Transparencies: power point.

Keywords: Flow composition, compensation, orchestration, CSP, trace semantics

(Postscript) (PDF)

Abstract
Web services composition is an emerging paradigm for the integration of long running business processes, attracting the interest of both Industry, in terms of XML-based standards for business description, and Academy, exploiting process description languages. The key challenging aspects to model are orchestration workflows, choreography of exchanged messages, fault handling, and transactional integrity with compensation mechanisms. Few recent proposals attempted to mitigate the explosion of XML-constructs in ad hoc standards by a careful selection of a small set of primitives related to the above aspects. This papers clarifies analogies and differences between two such recent process description languages: one based on interleaving trace semantics and the other on concurrent traces. We take advantage of their comparison to characterise and relate four different coordination policies for compensating parallel processes. Such policies differ on the way in which the abort of a process influences the execution of sibling processes, and whether compensation is distributed or centralised.

© Springer Verlag - DOI http://dx.doi.org/10.1007/11539452_24

"Deriving weak bisimulation congruences from reduction systems",
Roberto Bruni, Fabio Gadducci, Ugo Montanari and Pawel Sobocinski,
in Proceedings of CONCUR 2005, 16th International Conference on Concurrency Theory,
(Martín Abadi, Luca de Alfaro, Editors), 23-26 August 2005, San Francisco, CA, USA,
Lecture Notes in Computer Science 3653, pages 293-307, Springer Verlag, 2005.
ISBN 3-540-28309-9 (August 2005).

Keywords: Relative push-outs, 2-categories, double categories, reactive systems, labelled transition systems, weak bisimilarity

(Postscript) (PDF)

Abstract
The focus of process calculi is interaction rather than computation, and for this very reason: (i) their operational semantics is conveniently expressed by labelled transition systems (LTSs) whose labels model the possible interactions of a process with the environment; (ii) their abstract semantics is conveniently expressed by observational congruences. However, many current-day process calculi are more easily equipped with reduction semantics, where the notion of observable action is missing. Recent techniques attempted to bridge this gap by synthesising LTSs whose labels are process contexts that enable reactions and for which bisimulation is a congruence. Starting from Sewell's set-theoretic construction, category-theoretic techniques were defined and based on Leifer and Milner's relative pushouts, later refined by Sassone and the fourth author to deal with structural congruences given as groupoidal 2-categories. Building on recent works concerning observational equivalences for tile logic, the paper demonstrates that double categories provide an elegant setting in which the aforementioned contributions can be studied. Moreover, the formalism allows for a straightforward and natural definition of weak observational congruence.

© Springer Verlag - DOI http://dx.doi.org/10.1007/11548133_7

"Complete Axioms for Stateless Connectors",
Roberto Bruni, Ivan Lanese and Ugo Montanari,
in Proceedings of CALCO 2005, 1st Conference on Algebra and Coalgebra in Computer Science,
(José Luis Fiadeiro, Neil Harman, Markus Roggenbach, Jan Rutten, Editors), 3-6 September 2005, Swansea, UK,
Lecture Notes in Computer Science 3629, pages 98-113, Springer Verlag, 2005.
ISBN 3-540-28620-9 (August 2005).
Transparencies: power point.
Extended talk given at Dagstuhl-Seminar 04241: power point.

Keywords: Connectors, Normal Forms, Algebraic Semantics, Axiomatization, Monoidal Categories

(Postscript) (PDF)

Abstract
The conceptual separation between computation and coordination in distributed computing systems motivates the use of peculiar entities commonly called connectors, whose task is managing the interaction among distributed components. Different kinds of connectors exist in the literature, at different levels of abstraction. We focus on a basic algebra of connectors which is expressive enough to model, e.g., all the architectural connectors of CommUnity. We first define the operational, observational and denotational semantics of connectors, then we show that the observational and denotational semantics coincide and finally we give a complete normal-form axiomatization.

© Elsevier Science - DOI http://dx.doi.org/10.1016/j.tcs.2004.10.044

"Observational congruences for dynamically reconfigurable tile systems",
Roberto Bruni, Ugo Montanari and Vladimiro Sassone,
Theoretical Computer Science 335(2-3):pages 331-372, Elsevier Science, 2005.
ISSN 0304-3975 (May 2005).
Extends a IFIP TCS 2000 paper.
Contact the author(s) for a free reprint.

Keywords: Bisimulation, SOS Formats, Dynamic Bisimulation, Tile Logic

Abstract
The SOS formats that ensure that bisimilarity is a congruence fail in the presence of structural axioms on states. Dynamic bisimulation, introduced to characterize the coarsest congruence for CCS which is also a weak bisimulation, reconciles the bisimilarity is a congruence property with structural axioms and also with the specification of open ended systems, where states can be reconfigured at runtime. We show that the compositional framework offered by tile logic handles structural axioms and specifications of reconfigurable systems successfully. This allows for a finitary presentation of dynamic context closure, as internalized in the tile language. The case study of the pi-calculus illustrates the main features of our approach. Moreover, duality is exploited to model a second kind of reconfiguration: dynamic specialization.

"Normal Forms for Stateless Connectors",
Roberto Bruni, Ivan Lanese and Ugo Montanari,
Technical Report TR-05-11, Computer Science Department, University of Pisa, 2005.
Published 3 May 2005.

Keywords: Connectors, Normal Forms, Algebraic Semantics, Axiomatization, Monoidal Categories

(Postscript) (PDF)

Abstract
The conceptual separation between computation and coordination in distributed computing systems motivates the use of peculiar entities commonly called connectors, whose task is managing the interaction among distributed components. Different kinds of connectors exist in the literature at different levels of abstraction. We focus on a basic algebra of connectors which is expressive enough to model e.g. all the architectural connectors of CommUnity. We first define the operational, observational and denotational semantics of connectors, then we show that the observational and denotational semantics coincide and finally we give a complete normal-form axiomatization.

© Springer Verlag - DOI http://dx.doi.org/10.1007/978-3-540-31794-4_1

"Symbolic Equivalences for Open Systems",
Paolo Baldan, Andrea Bracciali and Roberto Bruni,
in Proceedings of GC 2004, International Workshop on Global Computing 2004,
(Corrado Priami, Paola Quaglia, Editors), 9-12 March 2004, Rovereto (Trento), Italy,
Lecture Notes in Computer Science 3267, pages 1-17, Springer Verlag, 2004.
ISBN 3-540-24101-9.

Keywords: Open systems, symbolic bisimulation, symbolic traces, unification

(Postscript) (PDF)

Abstract
Behavioural equivalences on open systems are usually defined by comparing system behaviour in all environments. Due to this universal quantification over the possible hosting environments, such equivalences are often difficult to check in a direct way. Here, working in the setting of process calculi, we introduce a hierarchy of behavioural equivalences for open systems, building on a previously defined symbolic approach. The hierarchy comprises both branching, bisimulation-based, and non-branching, trace-based, equivalences. Symbolic equivalences are amenable to effective analysis techniques (e.g., the symbolic transition system is finitely branching under mild assumptions), which result to be sound, but often not complete due to redundant information. Two kinds of redundancy, syntactic and semantic, are discussed and one class of symbolic equivalences is identified that deals satisfactorily with syntactic redundant transitions, which are a primary source of incompleteness.

© Schloss Dagstuhl - International Conference and Research Center for Computer Science

"On Graph(ic) Encodings",
Roberto Bruni and Ivan Lanese,
in Proceedings of Dagstuhl Seminar n.04241, Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems,
(Barbara Koenig, Ugo Montanari, Philippa Gardner, Editors), 6-11 June 2004, Dagstuhl, Germany,
pages 23-39, Technical Report Electronic Proceedings, 2005.
ISSN 1862-4405 (February 2005).

Keywords: Solo diagrams, Term graph rewriting, Synchronized hyperedge replacement, Bigraphs, Tile systems, Interactive systems

(Postscript) (PDF)

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.

© Schloss Dagstuhl - International Conference and Research Center for Computer Science

"CommUnity, Tiles and Connectors (abstract)",
Roberto Bruni,
in Proceedings of Dagstuhl Seminar n.04241, Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems,
(Barbara Koenig, Ugo Montanari, Philippa Gardner, Editors), 6-11 June 2004, Dagstuhl, Germany,
pages 54-55, Technical Report Electronic Proceedings, 2005.
Transparencies: power point.

Keywords: CommUnity, tile model, categorical semantics, algebraic semantics, software architectures, connectors

(Postscript) (PDF)

© ACM - DOI http://dx.doi.org/10.1145/1040305.1040323

"Theoretical foundations for compensations in flow composition languages",
Roberto Bruni, Hernán Melgratti and Ugo Montanari,
in Proceedings of POPL 2005, The 32nd Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages ,
12-14 January 2005, Long Beach, California, USA,
pages 209-220, 2005.
© ACM, (2005) This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution.
ISBN 1-58113-830-X
Transparencies: power point.
Extended talk given at the University of Santa Cruz: power point.

Keywords: Flow composition, compensation, process calculi, long-running transactions

(Postscript) (PDF)

Abstract
A key aspect when aggregating business processes and web services is to assure transactional properties of process executions. Since transactions in this context may require long periods of time to complete, traditional mechanisms for guaranteeing atomicity are not always appropriate. Generally the concept of long running transactions relies on a weaker notion of atomicity based on compensations. For this reason, programming languages for service composition cannot leave out two key aspects: compensations, i.e. ad hoc activities that can undo the effects of a process that fails to complete, and transactional boundaries to delimit the scope of a transactional flow. This paper presents a hierarchy of transactional calculi with increasing expressiveness. We start from a very small language in which activities can only be composed sequentially. Then, we progressively introduce parallel composition, nesting, programmable compensations and exception handling. A running example illustrates the main features of each calculus in the hierarchy.

© Elsevier Science - DOI http://dx.doi.org/10.1016/j.entcs.2004.02.039

"Modeling Fresh Names in pi-calculus Using Abstractions",
Roberto Bruni, Furio Honsell, Marina Lenisa and Marino Miculan,
in Proceedings of CMCS 2004, 7th International Workshop on Coalgebraic Methods in Computer Science,
(Jirí Adámek, Stefan Milius, Editors), 27-29 March 2004, Barcelona, Spain,
Electronic Notes in Theoretical Computer Science 106, pages 25-41, Elsevier Science, 2004.
ISSN 1571-0661 (published 11 December 2004).
Transparencies: pdf.

Keywords: Coalgebraic semantics, pi-calculus, theta-automata

(Postscript) (PDF)

Abstract
In this paper, we model fresh names in the pi-calculus using abstractions with respect to a new binding operator theta. Both the theory and the metatheory of the pi-calculus benefit from this simple extension. The operational semantics of this new calculus is finitely branching. Bisimulation can be given without mentioning any constraint on names, thus allowing for a straightforward definition of a coalgebraic semantics, within a category of coalgebras over permutation algebras. Following previous work by Montanari and Pistore, we present also a finite representation for finitary processes and a finite state verification procedure for bisimilarity, based on the new notion of theta-automaton.

© Elsevier Science - DOI http://dx.doi.org/10.1016/j.entcs.2004.09.021

"Flat Committed Join in Join",
Roberto Bruni, Hernán Melgratti and Ugo Montanari,
in Proceedings of CoMeta 2003, Final Workshop of the CoMeta Project,
(Furio Honsell, Marina Lenisa, and Marino Miculan, Editors), 15-17 December 2003, Udine, Italy,
Electronic Notes in Theoretical Computer Science 104, pages 39--59, Elsevier Science, 2003.
ISSN 1571-0661 (published 15 November 2004).
Transparencies: power point or PDF.

Keywords: Join, Distributed negotiations, Zero-safe nets, Orchestration

(Postscript) (PDF)

Abstract
Committed Join (cJoin) is an extension of Join with high-level primitives for programming dynamic nested negotiations with compensations. In this paper we show that flat cJoin processes (i.e. processes without sub-negotiations) can be encoded in the ordinary Join calculus by exploiting a distributed two-phase commit protocol. In particular, we first define a type system that singles out flat processes and prove subject reduction for it. Then, we show that all flat cJoin processes can be written in an equivalent canonical form, where a few elementary definition patterns are used. Finally, we show that canonical flat processes can be implemented in Join. It is worth noting that negotiation primitives are encoded as fully distributed agreements between all participants, thus avoiding a centralized coordinator.

© Kluwer Academics

"Nested commits for mobile calculi: extending Join",
Roberto Bruni, Hernán Melgratti and Ugo Montanari,
in Proceedings of IFIP TCS 2004, 3rd IFIP International Conference on Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics,
(Jean-Jacques Levy, Ernst W. Mayr, John C. Mitchell, Editors), 24-26 August 2004, Toulose, France,
IFIP Conference Proceedings, pages 563-576, Kluwer Academics, 2004.
ISBN 1-4020-8140-5.
Transparencies: power point.
Extended talk given at the University of Santa Cruz: power point.

Keywords: Join, Distributed negotiations, Nested negotiations, Compensation on abort, Committed choice languages, Zero safe nets, Orchestration, AKL, Serializability

(Postscript) (PDF)

Abstract
In global computing applications the availability of a mechanism for some form of committed choice can be useful, and sometimes necessary. It can conveniently handle, e.g., distributed agreements and negotiations with nested choice points. We propose a linguistic extension of the Join calculus for programming nested commits, called Committed Join (cJoin). It provides primitives for explicit abort, programmable compensations and interactions between negotiations. We give the operational semantics of cJoin in the reflexive CHAM style. Then we discuss its expressiveness on the basis of a few examples and encodings. Finally, we provide a big-step semantics for cJoin processes that can be typed as shallow and we show that shallow processes are serializable.

© Kluwer Academics

"New insights on architectural connectors",
Roberto Bruni, José Luiz Fiadeiro, Ivan Lanese, Antónia Lopes and Ugo Montanari,
in Proceedings of IFIP TCS 2004, 3rd IFIP International Conference on Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics,
(Jean-Jacques Levy, Ernst W. Mayr, John C. Mitchell, Editors), 24-26 August 2004, Toulose, France,
IFIP Conference Proceedings, pages 367-379, Kluwer Academics, 2004.
ISBN 1-4020-8140-5.
Transparencies: power point.

Keywords: CommUnity, tile model, categorical semantics, algebraic semantics, software architectures, connectors

(Postscript) (PDF)

Abstract
This work is a first step toward the reconciliation of the two main approaches to composition in system modeling, namely the categorical one and the algebraic one. In particular, we present a mapping from CommUnity, which uses the categorical approach based on colimits, into the Tile Model, which uses algebraic operators for composition. Our results include a standard decomposition for CommUnity programs. We also establish a strong link between the colimit computation of the categorical approach and the abstract semantics of configurations in the algebraic approach by proving that the encoding of a CommUnity diagram is behaviorally equivalent to the encoding of its colimit.

© Elsevier Science - DOI http://dx.doi.org/10.1016/S1571-0661(05)82530-7

"Tiling transactions in rewriting logic",
Roberto Bruni, José Meseguer and Ugo Montanari,
in Proceedings of WRLA 2002, 4th International Workshop on Rewriting Logic and its Applications,
(Fabio Gadducci, Ugo Montanari, Editors), 19-21 September 2002, Pisa, Italy,
Electronic Notes in Theoretical Computer Science 71, pages 90-109, Elsevier Science, 2004.
ISSN 1571-0661 (published April 2004).
Transparencies: power point.

Keywords: Tile Logic, Rewriting Logic, Category Theory, Transactions, Zero Safe Nets, Petri Nets

(Postscript) (PDF)

Abstract
We propose a modular high-level approach to the specification of transactions in rewriting logic, where the operational and the abstract views are related by suitable adjunctions between categories of tile theories and of rewrite theories.

© Springer Verlag - DOI http://dx.doi.org/10.1007/978-3-540-27755-2_7

"Extending the Zero-Safe approach to Coloured, Reconfigurable and Dynamic Nets",
Roberto Bruni, Hernán Melgratti and Ugo Montanari,
in Proceedings of Advances in Petri Nets: Lectures on Concurrency and Petri Nets,
(Jorg Desel, Wolfgang Reisig, Grzegorz Rozenberg, Editors),
Lecture Notes in Computer Science 3098, pages 291-327, Springer Verlag, 2004.
ISBN 3-540-22261-8 (June 2004).

Keywords: Zero-safe nets, Colured nets, Reconfigurable nets, Dynamic nets

(Postscript) (PDF)

Abstract
As web applications become more and more complex, primitives for handling interaction patterns among independent components become essential. In fact, distributed applications require new forms of transactions for orchestrating the progress of their negotiations and agreements. Still we lack foundational models that accurately explain the crucial aspects of the problem. In this work we explore how to model transactions in coloured, reconfigurable and dynamic nets, (i.e., high-level/high-order Petri nets that can express mobility and can extend themselves dynamically during their execution). Starting from zero-safe nets --- a well-studied extension of Place/Transition Petri nets with a transactional mechanism based on a distinction between consistent (observable) and transient (hidden) states --- we show how the zero-safe approach can be smoothly applied to a hierarchy of nets of increasing expressiveness.

© Cambridge University Press - DOI http://dx.doi.org/10.1017/S0960129504004189

"Concurrent models for Linda with Transactions",
Roberto Bruni and Ugo Montanari,
Mathematical Structures in Computer Science 14(3):pages 421-468, Cambridge University Press, 2004.
ISSN 0960-1295 (June 2004).
Extends the ConCoord 2001 paper.
Contact the author(s) for a free reprint.

Keywords: Zero Safe Nets, Contextual Nets, Transactions, Coordination, Linda, PMEqtl, Refinement

Abstract
Nowadays concepts, languages and models for coordination cannot leave aside the needs of the increasing number of commercial applications based on global computing over the (inter)net. For example, platforms like Microsoft .NET and Sun Microsystems Java come equipped with packages for supporting ad hoc transactional features, which are essential for most business applications. We show how to extend the coordination language par excellence (i.e. Linda) with basic primitives for transactions, while retaining a formal model for its concurrent computations. This is achieved by exploiting a variation of Petri nets, called zero-safe nets, where transactions can be suitably modeled by distinguishing between stable places (ordinary ones) and zero places (where tokens can only be temporarily allocated, defining hidden states). The relevance of the transaction mechanism is illustrated in terms of expressive power. Finally, it is shown that stable places and transactions viewed as atomic steps define an abstract semantics that is apt to a fully algebraic treatment, demonstrated via categorical adjunctions between suitable categories of nets.

"A prototype implementation of distributed agreements",
Alberto Baragatti, Roberto Bruni, Hernán Melgratti and Ugo Montanari,
Technical Report TR-04-10, Computer Science Department, University of Pisa, 2004.
Published 22 April 2004.

Keywords: Distributed negotiations, mobile ad-hoc networks, JoCaml, D2PC

(Postscript) (PDF)

Abstract
We present a prototype application for distributed agreements in multi-parties negotiations, where the number of participants is statically unknown, new participants can dynamically join ongoing negotiations and each participant knows only those parties with whom interacted. The application is based on asynchronous communication and it exploits the D2PC protocol for committing or aborting the negotiation. The software architecture consists of three modular layers, with the D2PC compiled in the bottom layer and completely transparent to final users. Our prototype is tailored to the running scenario of Ad-Hoc networks used by rescue teams for disaster recovery.

"Symbolic Equivalences for Open Systems (Tech. Rep.)",
Paolo Baldan, Andrea Bracciali and Roberto Bruni,
Technical Report TR-03-16, Computer Science Department, University of Pisa, 2003.
Published 31 December 2003.
Transparencies of a seminar for the Maude group at UIUC: power point.
Transparencies of a seminar for the Formal Methods group at UIUC: power point.

Keywords: Open systems, symbolic bisimulation, symbolic traces, unification

(Postscript) (PDF)

Abstract
Behavioural equivalences on open systems are usually defined by comparing system behaviour in all environments. Here, we introduce a hierarchy of behavioural equivalences for open systems in the setting of process calculi, building on a symbolic approach proposed in a previous paper. The hierarchy comprises both branching, bisimulation-based, and non-branching, trace-based, equivalences. Symbolic equivalences are amenable to effective analysis techniques (e.g., the symbolic transition system is finitely branching under mild assumptions), which result to be correct, but often not complete due to redundant information. Two kinds of redundancy, syntactic and semantic, are discussed and one class of symbolic equivalences is identified that deals satisfactorily with syntactic redundant transitions, which are a primary source of incompleteness.

© Springer Verlag - DOI http://dx.doi.org/ 10.1007/978-3-540-40020-2_1

"AGILE: Software Architecture for Mobility",
L. Andrade, P. Baldan, H. Baumeister, R. Bruni, A. Corradini, R. De Nicola, J.L. Fiadeiro, F. Gadducci, S. Gnesi, P. Hoffman, N. Koch, P. Kosiuczenko, A. Lapadula, D. Latella, A. Lopes, M. Loreti, M. Massink, F. Mazzanti, U. Montanari, C. Oliveira, R. Pugliese, A. Tarlecki, M. Wermelinger, M. Wirsing, A. Zawlocki,
in Proceedings of WADT 2002, 16th International Workshop on Algebraic Development Techniques,
(Martin Wirsing, Dirk Pattinson, Rolf Hennicker, Editors), 24-27 September 2002, Frauenchiemsee, Germany,
Lecture Notes in Computer Science 2755, pages 1-33, Springer Verlag, 2003.
ISBN 3-540-20537-3 (November 2003).

Keywords: Software architectures for mobility, UML, Statecharts, Open KLAIM, CommUnity, graph transformation

(Postscript) (PDF)

Abstract
Architecture-based approaches have been promoted as a means of controlling the complexity of system construction and evolution, in particular for providing systems with the agility required to operate in turbulent environments and to adapt very quickly to changes in the enterprise world. Recent technological advances in communication and distribution have made mobility an additional factor of complexity, one for which current architectural concepts and techniques can be hardly used. The AGILE project is developing an architectural approach in which mobility aspects can be modelled explicitly and mapped on the distribution and communication topology made available at physical levels. The whole approach is developed over a uniform mathematical framework based on graph-oriented techniques that support sound methodological principles, formal analysis, and refinement. This paper describes the AGILE project and some of the results gained during the first project year.

© Springer Verlag - DOI http://dx.doi.org/10.1007/978-3-540-40020-2_8

"Pre-nets, read arcs and unfolding: a functorial presentation",
Paolo Baldan, Roberto Bruni and Ugo Montanari,
in Proceedings of WADT 2002, 16th International Workshop on Algebraic Development Techniques,
(Martin Wirsing, Dirk Pattinson, Rolf Hennicker, Editors), 24-27 September 2002, Frauenchiemsee, Germany,
Lecture Notes in Computer Science 2755, pages 145-164, Springer Verlag, 2003.
ISBN 3-540-20537-3 (November 2003).
Transparencies: power point.

Keywords: Petri nets, Pre-nets, Functorial semantics, Processes, Unfolding

(Postscript) (PDF)

Abstract
Pre-nets have been recently proposed as a means of providing a functorial algebraic semantics to Petri nets (possibly with read arcs), overcoming some previously unsolved subtleties of the classical model. Here we develop a functorial semantics for pre-nets following a sibling classical approach based on an unfolding construction. Any pre-net is mapped to an acyclic branching net, representing its behaviour, then to a prime event structure and finally to a finitary prime algebraic domain. Then the algebraic and unfolding view are reconciled: we exploit the algebraic semantics to define a functor from the category of pre-nets to the category of domains that is shown to be naturally isomorphic to the unfolding-based functor. All the results are extended to pre-nets with read arcs.

© Springer Verlag - DOI http://dx.doi.org/10.1007/978-3-540-45208-9_21

"Algebraic theories for contextual pre-nets",
Roberto Bruni, José Meseguer, Ugo Montanari and Vladimiro Sassone,
in Proceedings of ICTCS 2003, 8th Italian Conference on Theoretical Computer Science,
(Carlo Blundo, Cosimo Laneve, Editors), 13-15 October 2003, Bertinoro, Italy,
Lecture Notes in Computer Science 2841, pages 256-270, Springer Verlag, 2003.
ISBN 3-540-20216-1 (November 2003).
Transparencies: power point.

Keywords: Contextual Pre-Nets, Partial Membership Equational Logic, Algebraic Semantics, Monoidal Categories

(Postscript) (PDF)

Abstract
The algebraic models of computation for contextual nets that have been proposed in the literature either rely on a non-free monoid of objects, or introduce too many fictitious behaviors that must be somewhat filtered out. In this paper, we exploit partial membership equational logic to define a suitable theory of models, where the meaningful concurrent computations can be selected by means of membership predicates.

© Springer Verlag - DOI http://dx.doi.org/10.1007/3-540-45061-0_22

"Generalized rewrite theories",
Roberto Bruni and José Meseguer,
in Proceedings of ICALP 2003, 30th International Colloquium on Automata, Languages and Programming,
(Jos C.M. Baeten, Jan Karel Lenstra, Joachim Parrow, Gerhard J. Woeginger, Editors), 30 June - 4 July 2003, Eindhoven, The Netherlands,
Lecture Notes in Computer Science 2719, pages 252-266, Springer Verlag, 2003.
ISBN 3-540-40493-7 (January 2003).
Transparencies: gzipped pdf.

Keywords: Conditional rewriting logic, Frozen operators, Partial Membership Equational Logic, Concurrent semantics

(Postscript) (PDF)

Abstract
Since its introduction, more than a decade ago, rewriting logic has attracted the interest of both theorists and practitioners, who have contributed in showing its generality as a semantic and logical framework and also as a programming paradigm. The experimentation conducted in these years has suggested that some significant extensions to the original definition of the logic would be very useful in practice. In particular, the Maude system now supports subsorting and conditions in the equational logic for data, and also frozen arguments to block undesired nested rewritings; moreover, it allows equality and membership assertions in rule conditions. In this paper, we give a detailed presentation of the inference rules, model theory, and completeness of such generalized rewrite theories.

"Pre-nets, read arcs and unfolding: a functorial presentation (extended abstract)",
Paolo Baldan, Roberto Bruni and Ugo Montanari,
Technical Report 0207, LMU Munchen, 2002.
Pre-proceedings WADT 2002, 16th International Workshop on Algebraic Development Techniques, 24-27 September 2002, Frauenchiemsee, Germany (Martin Wirsing, Dirk Pattinson, Rolf Hennicker, Editors).
Transparencies: power point.

Keywords: Petri nets, Pre-nets, Functorial semantics, Processes, Unfolding

(Postscript) (PDF)

Abstract
P/T Petri nets are one of the most widely known models of concurrency. Since their introduction, the conceptual simplicity of the model and its intuitive graphical presentation have attracted the interest of both theoreticians and practitioners. Nevertheless, the concurrent semantics of Petri nets present several subtleties that still cannot be considered fully understood. In this presentation, we concentrate on the semantic interpretations arising from the so-called individual token philosophy (ITPh) as opposed to the collective token philosophy (CTPh), the latter being less amenable to the full variety of aspects that can be studied in the ITPh. Our twofold aim is: (1) to emphasise the missing fragments of the overall picture arising from the different semantic frameworks for P/T Petri nets (roughly classified in process-oriented, unfolding, algebraic, logical, categorical); (2) to outline some preliminary ideas and results for bridging the gaps in a formal and satisfactory way.

© Elsevier Science - DOI http://dx.doi.org/10.1016/S0304-3975(01)00318-8

"Normal Forms for Algebras of Connections",
Roberto Bruni, Fabio Gadducci and Ugo Montanari,
Theoretical Computer Science 286(2):pages 247-292, Elsevier Science, 2002.
ISSN 0304-3975 (September 2002).
Extends a WADT98 paper.
Contact the author(s) for a free reprint.

Keywords: Distributed Systems, Normal Forms, Sigma-Spaces, Partitions, Relations, (Co)Gs-Monoidal Categories

Abstract
Recent years have seen a growing interest towards algebraic structures that are able to express formalisms different from the standard, tree-like presentation of terms. Many of these approaches reveal a specific interest towards the application to the `distributed and concurrent systems' field, but an exhaustive comparison between them is sometimes difficult, because their presentations can be quite dissimilar. This work is a first step towards a unified view: Focusing on the primitive ingredients of distributed spaces (namely interfaces, links and basic modules), we introduce a general schema for describing a normal form presentation of many algebraic formalisms, and show that those normal forms can be thought of as arrows of suitable monoidal categories.

© Springer Verlag - DOI http://dx.doi.org/10.1007/3-540-45719-4_18

"Bisimulation by unification",
Paolo Baldan, Andrea Bracciali and Roberto Bruni,
in Proceedings of AMAST 2002, 9th International Conference on Algebraic Methodology And Software Technology,
(Helene Kirchner, Christophe Ringeissen, Editors), 9-13 September 2002, St. Gilles les Bains, Reunion Island, France,
Lecture Notes in Computer Science 2422, pages 254-270, Springer Verlag, 2002.
ISBN 3-540-44144-1 (September 2002).
Transparencies: power point.

Keywords: Open systems, symbolic bisimulation, unification, ambient calculus

(Postscript) (PDF)

Abstract
We propose a methodology for the analysis of open systems based on process calculi and bisimilarity. Open systems are seen as coordinators (i.e. terms with place-holders), that evolve when suitable components (i.e. closed terms) fill in their place-holders. The distinguishing feature of our approach is the definition of a symbolic operational semantics for coordinators that exploits spatial/modal formulae as labels of transitions and avoids the universal closure of coordinators w.r.t. all components. Two kinds of bisimilarities are then defined, called strict and large, which differ in the way formulae are compared. Strict bisimilarity implies large bisimilarity which, in turn, implies the one based on universal closure. Moreover, for process calculi in suitable formats, we show how the symbolic semantics can be defined constructively, using unification. Our approach is illustrated on a toy process calculus with CCS-like communication within ambients.

© Springer Verlag - DOI http://dx.doi.org/10.1007/3-540-45694-5_22

"Orchestrating Transactions in Join Calculus",
Roberto Bruni, Cosimo Laneve and Ugo Montanari,
in Proceedings of CONCUR 2002, 13th International Conference on Concurrency Theory,
(Lubos Brim, Petr Jancar, Mojmir Kretinsky, Antonin Kucera, Editors), 20-23 August 2002, Brno, Czech Republic,
Lecture Notes in Computer Science 2421, pages 321-336, Springer Verlag, 2002.
ISBN 3-540-44043-7 (August 2002).

Keywords: Zero Safe Nets, Join Calculus, BizTalk, Orchestration, Concurrent Semantics, Transactions

(Postscript) (PDF)

Abstract
We discuss the principles of distributed transactions, then we define an operational model which meets the basic requirements and we give a prototyping implementation for it in join-calculus. Our model: (1) extends BizTalk with multiway transactions; (2) exploits an original algorithm, for distributed commit; (3) can deal with dynamically changing communication topology; (4) is almost language-independent. In fact, the model is based on a two-level classification of resources, which should be easily conveyed to distributed calculi and languages, providing them with a uniform transactional mechanism.

"Centralized and distributed orchestration of transactions in the join calculus",
Roberto Bruni, Cosimo Laneve and Ugo Montanari,
Technical Report TR-02-12, Computer Science Department, University of Pisa, 2002.
Published 12 July 2002.

Keywords: Zero Safe Nets, Join Calculus, BizTalk, Orchestration, Concurrent Semantics, Transactions

(Postscript) (PDF)

Abstract
We discuss the principles of distributed transactions, then we define an operational model which meets the basic requirements and we give a prototyping implementation for it in join-calculus. Our model: (1) extends BizTalk with multiway transactions; (2) exploits an original algorithm, for distributed commit; (3) can deal with dynamically changing communication topology; (4) is almost language-independent. In fact, the model is based on a two-level classification of resources, which should be easily conveyed to distributed calculi and languages, providing them with a uniform transactional mechanism.

"Functorial models for contextual pre-nets",
Roberto Bruni, José Meseguer, Ugo Montanari and Vladimiro Sassone,
Technical Report TR-02-09, Computer Science Department, University of Pisa, 2002.
Published 25 June 2002.

Keywords: Contextual Pre-Nets, Partial Membership Equational Logic, Algebraic Semantics, Monoidal Categories

(Postscript) (PDF)

Abstract
The algebraic models of computation for contextual nets that have been proposed in the literature either rely on non-free monoid of objects, or introduce too many behaviors that must be somewhat filtered out. In this report, we exploit partial membership equational logic to define a suitable theory of models, where the meaningful concurrent computations can be selected by means of membership predicates.

"Modeling fresh names in pi-calculus using abstractions",
Roberto Bruni, Furio Honsell, Marina Lenisa, and Marino Miculan,
Technical Report TR 21/2002, Department of Mathematics and Computer Science, University of Udine, 2002.
Published April 2002.

Keywords: Coalgebraic semantics, pi-calculus, theta-automata

(Postscript) (PDF)

Abstract
In this paper, we model fresh names in the pi-calculus using abstractions w.r.t. a new binding operator theta. Both the theory and the metatheory of the pi-calculus benefit from this simple extension. The operational semantics of this new calculus is finitely branching. Bisimulation can be given without mentioning any constraint on names, thus allowing for a straightforward definition of a coalgebraic semantics. This is cast within a category of coalgebras over algebras with infinitely many unary operators, in order to capitalize on theta. Following previous work by Montanari and Pistore, we present also a finite representation for finitary processes and a finite state verification procedure for bisimilarity, based on the new notion of theta-automaton. Finally, we improve previous encodings of the pi-calculus in the Calculus of Inductive Constructions.

© Elsevier Science - DOI http://dx.doi.org/10.1016/S0304-3975(01)00318-8

"Dynamic connectors for concurrency",
Roberto Bruni and Ugo Montanari,
Theoretical Computer Science 281(1-2):pages 131-176, Elsevier Science, 2002.
ISSN 0304-3975 (May 2002).
Transparencies: Postscript or PDF.
Contact the author(s) for a free reprint.

Keywords: Tile Logic, Distributed Systems, Concurrent Semantics, Causal Semantics, Connectors, Process Rewrite Systems, Basic Parallel Processes

Abstract
We propose a meta-theoretic approach to the definition of operational and abstract concurrent semantics for systems where name handling is a key issue. The main ingredients of our framework are connectors and tile logic. The former allow for the modeling of various kinds of graph-like and term-like structures, which can be useful in representing system distribution and causal histories. The latter is used to combine the use of connectors in space and in time (i.e., according to configurations and computations). As a detailed case study, we show how to define a concurrent operational semantics and causal weak bisimilarity for a flavour of basic parallel processes.

© Cambridge University Press - DOI http://dx.doi.org/10.1017/S0960129501003462

"Symmetric Monoidal and Cartesian Double Categories as a Semantic Framework for Tile Logic",
Roberto Bruni, José Meseguer and Ugo Montanari,
Mathematical Structures in Computer Science 12(1):pages 53-90, Cambridge University Press, 2002.
ISSN 0960-1295 (February 2002).
Contact the author(s) for a free reprint.

Keywords: Category Theory, Double Categories, Tile Logic, Distributed Systems

Abstract
Tile systems offer a general paradigm for modular descriptions of concurrent systems, based on a set of rewriting rules with side-effects. Monoidal double categories are a natural semantic framework for tile systems, because the mathematical structures describing system states and synchronizing actions (called configurations and observations, respectively, in our terminology) are monoidal categories having the same objects (the interfaces of the system). In particular, configurations and observations based on net-process-like and term structures are usually described in terms of symmetric monoidal and cartesian categories, where the auxiliary structures for the rearrangement of interfaces correspond to suitable natural transformations. In this paper we discuss the lifting of these auxiliary structures to double categories. We notice that the internal construction of double categories produces a pathological asymmetric notion of natural transformation, which is fully exploited in one dimension only (for example, for configurations or for observations, but not for both). Following Ehresmann (1963), we overcome this biased definition, introducing the notion of generalized natural transformation between four double functors (rather than two). As a consequence, the concepts of symmetric monoidal and cartesian (with consistently chosen products) double categories arise in a natural way from the corresponding ordinary versions, giving a very good relationship between the auxiliary structures of configurations and observations. Moreover, the Kelly-MacLane coherence axioms can be lifted to our setting without effort, thanks to the characterization of two suitable diagonal categories that are always present in a double category. Then, symmetric monoidal and cartesian double categories are shown to offer an adequate semantic setting for process and term tile systems.

© Academic Press - DOI http://dx.doi.org/10.1006/inco.2001.3050

"Functorial Models for Petri Nets",
Roberto Bruni, José Meseguer, Ugo Montanari and Vladimiro Sassone,
Information and Computation 170(2):pages 207-236, Academic Press, 2001.
ISSN 0890-5401 (November 2001).
Extends the ASIAN98 and the CTCS99 papers.
Contact the author(s) for a free reprint.

Keywords: Petri Nets, Pre-Nets, Concurrent Transition Systems, Category Theory, Monoidal Categories, PMEqtl

Abstract
We show that although the algebraic semantics of place/transition Petri nets under the collective token philosophy can be fully explained in terms of strictly symmetric monoidal categories, the analogous construction under the individual token philosophy is not completely satisfactory, because it lacks universality and also functoriality. We introduce the notion of pre-nets to overcome this, obtaining a fully satisfactory categorical treatment, where the operational semantics of nets yields an adjunction. This allows us to present a uniform logical description of net behaviors under both the collective and the individual token philosophies in terms of theories and theory morphisms in partial membership equational logic. Moreover, since the universal property of adjunctions guarantees that colimit constructions on nets are preserved in our algebraic models, the resulting semantic framework has good compositional properties.

© Cambridge University Press - DOI http://dx.doi.org/10.1017/S1471068401000035

"An Interactive Semantics of Logic Programming",
Roberto Bruni, Ugo Montanari and Francesca Rossi,
Theory and Practice of Logic Programming 1(6):pages 647-690, Cambridge University Press, 2001.
ISSN 1471-0684 (November 2001).
Contact the author(s) for a free reprint.

Keywords: Tile Logic, Logic Programming, Open Systems

Abstract
We apply to logic programming some recently emerging ideas from the field of reduction-based communicating systems, with the aim of giving evidence of the hidden interactions and the coordination mechanisms that rule the operational machinery of such a programming paradigm. The semantic framework we have chosen for presenting our results is tile logic, which has the advantage of allowing a uniform treatment of goals and observations and of applying abstract categorical tools for proving the results. As main contributions, we mention the finitary presentation of abstract unification, and a concurrent and coordinated abstract semantics consistent with the most common semantics of logic programming. Moreover, the compositionality of the tile semantics is guaranteed by standard results, as it reduces to check that the tile systems associated to logic programs enjoy the tile decomposition property. An extension of the approach for handling constraint systems is also discussed.

© Springer Verlag - DOI http://dx.doi.org/10.1007/3-540-45541-8_12

"Transactions and Zero-Safe Nets",
Roberto Bruni and Ugo Montanari,
in Proceedings of Advances in Petri Nets: Unifying Petri Nets,
(Hartmut Ehrig, Gabriel Juhás, Julia Padberg, Grzegorz Rozenberg, Editors),
Lecture Notes in Computer Science 2128, pages 380-426, Springer Verlag, 2001.
ISBN 3-540-43067-9 (December 2001).
Extends a ICATPN 2000 paper.

Keywords: Zero Safe Nets, Petri Nets, Contextual Nets, Distributed Systems, Unfolding, Transactions, Refinement

(Postscript) (PDF)

Abstract
When employing Petri nets to model distributed systems, one must be aware that the basic activities of each component can vary in duration and can involve smaller internal activities, i.e., that transitions are conceptually refined into transactions. We present an approach to the modeling of transactions based on zero-safe nets. They extend ordinary PT nets with a simple mechanism for transition synchronization. We show that the net theory developed under the two most diffused semantic interpretations (collective token and individual token philosophies) can be uniformly adapted to zero-safe nets. In particular, we show that each zero-safe net has associated two PT nets which represent the abstract counterparts of the modeled system according to the two philosophies. We show several applications of the framework, a distributed interpreter for ZS nets based on classical net unfolding (here extended with a commit rule) and discuss some extensions to other net flavours to show that the concept of zero place provides a unifying notion of transaction for several different kinds of Petri nets.

© Springer Verlag - DOI http://dx.doi.org/10.1007/3-540-45541-8_13

"Two Algebraic Process Semantics for Contextual Nets",
Roberto Bruni and Vladimiro Sassone,
in Proceedings of Advances in Petri Nets: Unifying Petri Nets,
(Hartmut Ehrig, Gabriel Juhás, Julia Padberg, Grzegorz Rozenberg, Editors),
Lecture Notes in Computer Science 2128, pages 427-456, Springer Verlag, 2001.
ISBN 3-540-43067-9 (December 2001).
Extends a ICALP 2000 paper.

Keywords: Petri Nets, Contextual Nets, Monoidal Categories

(Postscript) (PDF)

Abstract
We show that the so-called `Petri nets are monoids' approach initiated by Meseguer and Montanari can be extended from ordinary place/transition Petri nets to contextual nets by considering suitable non-free monoids of places. The algebraic characterizations of net concurrent computations we provide cover both the collective and the individual token philosophy, uniformly along the two interpretations, and coincide with the classical proposals for place/transition Petri nets in the absence of read-arcs.

© Elsevier Science - DOI http://dx.doi.org/10.1016/S1571-0661(04)00324-X

"Comparing higher-order encodings in logical frameworks and tile logic",
Roberto Bruni, Furio Honsell, Marina Lenisa and Marino Miculan,
in Proceedings of TOSCA 2001, Final Workshop of the TOSCA Project,
(Ugo Montanari, Editor), 19-21 November 2001, Udine, Italy,
Electronic Notes in Theoretical Computer Science 62, pages 136-156, Elsevier Science, 2002.
ISSN 1571-0661 (published June 2002).
Transparencies (of part II): Postscript or PDF.

Keywords: Logical Framework, Tile Logic, HOAS

(Postscript) (PDF)

Abstract
In recent years, logical frameworks and tile logic have been separately proposed by our research groups, respectively in Udine and in Pisa, as suitable metalanguages with higher-order features for encoding and studying nominal calculi. This paper discusses the main features of the two approaches, tracing differences and analogies on the basis of two case studies: late pi-calculus and lazy simply typed lambda-calculus.

© Elsevier Science - DOI http://dx.doi.org/10.1016/S1571-0661(04)00239-7

"Zero-safe net models for transactions in Linda",
Roberto Bruni and Ugo Montanari,
in Proceedings of ConCoord 2001, International Workshop on Concurrency and Coordination,
(Ugo Montanari, Vladimiro Sassone, Editors), 6-8 July 2001, Lipari Island, Italy,
Electronic Notes in Theoretical Computer Science 54, pages 106-116, Elsevier Science, 2001.
ISBN 0444510680.
Transparencies: power point.

Keywords: Zero Safe Nets, Contextual Nets, Transactions, Coordination, Linda

(Postscript) (PDF)

Abstract
Zero-safe nets are a variation of Petri nets, where transactions can be suitably modeled. The idea is to distinguish between stable places (whose markings define observable states) and zero-safe places (where tokens can only be temporarily allocated, defining hidden states): Transactions must start and end in observable states. We propose an extension of the coordination language Linda, called TraLinda, where a few basic primitives for expressing transactions are introduced by means of different typing of tuples. By exploiting previous results of Busi, Gorrieri and Zavattaro on the net modeling of Linda-like languages, we define a concurrent operational semantics based on zero-safe nets for TraLinda, where the typing of tuples reflects evidently on the distinction between stable and zero-safe places.

© Elsevier Science - DOI http://dx.doi.org/10.1016/S1571-0661(04)80937-X

"Some algebraic laws for spans (and their connections with multirelations)",
Roberto Bruni and Fabio Gadducci,
in Proceedings of RelMiS 2001, Relational Methods in Software,
(Wolfram Kahl, David L. Parnas, Gunther Schmidt, Editors), 7-8 April 2001, Genova, Italy,
Electronic Notes in Theoretical Computer Science 44.3, pages 175-193, Elsevier Science, 2001.
ISSN 1571-0661 (published May 2003).
Transparencies: Postscript or PDF.

Keywords: (Co)Spans, Relations, Partitions

(Postscript) (PDF)

Abstract
This paper investigates some key algebraic properties of the categories of spans and cospans (up to isomorphic supports) over the category Set of (small) sets and functions, analyzing the monoidal structures induced over both spans and cospans by cartesian product and disjoint union of sets. Our results find analogous counterparts in (and are partly inspired by) the theory of relational algebras, thus our paper also sheds some light on the relationship between (co)spans and the categories of (multi)relations and of equivalence relations. And, since (co)spans yield an intuitive presentation of dynamical systems with input and output interfaces, our results introduce an expressive, two-fold algebra that can serve as a specification formalism for rewriting systems and for composing software modules.

"First order and higher order tile models for open and mobile systems (abstract)",
Roberto Bruni and Ugo Montanari,
in Proceedings of TOSCA'00, Workshop Annuale del Progetto TOSCA,
30 November - 2 December 2000, Genova, Italy,
2000.
Virtual Proceedings.

Keywords: Tile Logic, Bisimilarity Congruences, Open Systems

(Postscript) (PDF)

© Springer Verlag - DOI http://dx.doi.org/10.1007/3-540-44618-4_20

"Bisimilarity congruences for open terms and term graphs via tile logic",
Roberto Bruni, David de Frutos-Escrig, Narciso Martí-Oliet and Ugo Montanari,
in Proceedings of CONCUR 2000, 11th International Conference on Concurrency Theory,
(Catuscia Palamidessi, Editor), 22-25 August 2000, Pennsylvania, USA,
Lecture Notes in Computer Science 1877, pages 259-274, Springer Verlag, 2000.
ISBN 3-540-67897-2 (August 2000).
Transparencies: Postscript or PDF.

Keywords: Tile Logic, Bisimilarity Congruences, Term Graphs, Open Systems

(Postscript) (PDF)

Abstract
The definition of SOS formats ensuring that bisimilarity on closed terms is a congruence has received much attention in the last two decades. For dealing with open terms, the congruence is usually lifted from closed terms by instantiating the free variables in all possible ways; the only alternatives considered in the literature are Larsen and Xinxin's context systems and Rensink's conditional transition systems. We propose an approach based on tile logic, where closed and open terms are managed uniformly, and study the `bisimilarity as congruence' property for several tile formats, accomplishing different concepts of open system.

© Springer Verlag - DOI http://dx.doi.org/10.1007/3-540-44929-9_31

"Open ended systems, dynamic bisimulation and tile logic",
Roberto Bruni, Ugo Montanari and Vladimiro Sassone,
in Proceedings of IFIP TCS 2000, IFIP International Conference on Theoretical Computer Science,
(Jan van Leeuwen, Osamu Watanabe, Masami Hagiya, Peter D. Mosses, Takayasu Ito, Editors), 17-19 August 2000, Sendai, Japan,
Lecture Notes in Computer Science 1872, pages 440-456, Springer Verlag, 2000.
ISBN 3-540-67823-9 (August 2000).
Transparencies: Postscript or PDF.

Keywords: Tile Logic, Dynamic Bisimilarity, Open Systems

(Postscript) (PDF)

Abstract
The SOS formats ensuring that bisimilarity is a congruence often fail in the presence of structural axioms on the algebra of states. Dynamic bisimulation, introduced to characterize the coarsest congruence for CCS which is also a (weak) bisimulation, reconciles the bisimilarity as congruence property with such axioms and with the specification of open ended systems, where states can be reconfigured at run-time, at the cost of an infinitary operation at the meta-level. We show that the compositional framework offered by tile logic is suitable to deal with structural axioms and open ended systems specifications, allowing for a finitary presentation of context closure.

© Springer Verlag - DOI http://dx.doi.org/10.1007/3-540-45022-X_15

"Algebraic Models for Contextual Nets",
Roberto Bruni and Vladimiro Sassone,
in Proceedings of ICALP 2000, 27th International Colloquium on Automata, Languages and Programming,
(Ugo Montanari, José D.P. Rolim, Emo Welzl, Editors), 9-15 July 2000, Geneva, Switzerland,
Lecture Notes in Computer Science 1853, pages 175-186, Springer Verlag, 2000.
ISBN 3-540-67715-1 (July 2000).

Keywords: Petri Nets, Contextual Nets, Monoidal Categories

(Postscript) (PDF)

Abstract
We extend the algebraic approach of Meseguer and Montanari from ordinary place/transition Petri nets to contextual nets, covering both the collective and the individual token philosophy uniformly along the two interpretations of net behaviors.

© Springer Verlag - DOI http://dx.doi.org/10.1007/3-540-44988-4_7

"Executing Transactions in Zero-Safe Nets",
Roberto Bruni and Ugo Montanari,
in Proceedings of ICATPN 2000, 21st International Conference on Application and Theory of Petri Nets,
(Mogens Nielsen, Dan Simpson, Editors), 26-30 June 2000, Aarhus, Denmark,
Lecture Notes in Computer Science 1825, pages 83-102, Springer Verlag, 2000.
ISBN 3-540-67693-7 (June 2000).

Keywords: Zero Safe Nets, Petri Nets, Unfolding, Transactions, Refinement, Distributed Systems

(Postscript) (PDF)

Abstract
Distributed systems are often composed by many heterogeneous agents that can work concurrently and exchange information. Therefore, in their modeling via PT nets we must be aware that the basic activities of each system can vary in duration and can be constituted by smaller internal activities, i.e., transitions are conceptually refined into transactions. We address the issue of modeling transactions in distributed systems by using zero-safe nets, which extend PT nets with a simple mechanism for transition synchronization. In particular, starting from the zero-safe net that represents a certain system, we give a distributed algorithm for executing the transactions of the system as transitions of a more abstract PT net. Among the advantages of our approach, we emphasize that the zero-safe net can be much smaller than its abstract counterpart, due to the synchronization mechanism.

"Tile Bisimilarity Congruences for Open Terms and Term Graphs",
Roberto Bruni, David de Frutos-Escrig, Narciso Martí-Oliet and Ugo Montanari,
Technical Report TR-00-06, Computer Science Department, University of Pisa, 2000.
Published 23 May 2000.
Full version of the CONCUR 2000 paper.

Keywords: Tile Logic, Bisimilarity Congruences, Term Graphs, Open Systems

(Postscript) (PDF)

Abstract
The definition of SOS formats ensuring that bisimilarity on closed terms is a congruence has received much attention in the last two decades. For dealing with open system specifications, the congruence is usually lifted from closed terms to open terms by instantiating the free variables in all possible ways; the only alternatives considered in the literature relying on Larsen and Xinxin's context systems and Rensink's conditional transition systems. We propose a different approach based on tile logic, where both closed and open terms are managed analogously. In particular, we analyze the `bisimilarity as congruence' property for several tile formats that accomplish different concepts of subterm sharing.

© Academic Press - DOI http://dx.doi.org/10.1006/inco.1999.2819

"Zero-Safe Nets: Comparing the Collective and Individual Token Approaches",
Roberto Bruni and Ugo Montanari,
Information and Computation 156(1-2):pages 46-89, Academic Press, 2000.
ISSN 0890-5401 (January 2000).
Extends the EXPRESS97 and the WADT97 papers.
Contact the author(s) for a free reprint.

Keywords: Zero Safe Nets, Petri Nets, Category Theory, Transactions, Refinement

Abstract
The main feature of zero-safe nets is a primitive notion of transition synchronization. To this aim, besides ordinary places, called stable places, zero-safe nets are equipped with zero places, which in an observable marking cannot contain any token. This yields the notion of transaction: a basic atomic computation, which may use zero tokens as triggers, but defines an evolution between observable markings only. The abstract counterpart of a generic zero-safe net B consists of an ordinary P/T net whose places are the stable places of B, and whose transitions represent the transactions of B. The two nets offer both the refined and the abstract model of the same system, where the former can be much smaller than the latter, because of the transition synchronization mechanism. Depending on the chosen approach -- collective vs individual token philosophy -- two notions of transaction may be defined, each leading to different operational and abstract models. Their comparison is fully discussed on the basis of a multicasting system example. In the second part of the paper, we make use of category theory to analyze and motivate our framework. More precisely, the two operational semantics of zero-safe nets are characterized as adjunctions, and the derivation of abstract P/T nets as coreflections.

"Zero-safe nets: Modeling transactions via transition synchronization (abstract)",
Roberto Bruni and Ugo Montanari,
in Proceedings of Final Workshop of the Project "Tecniche Formali per la Specifica, l'Analisi, la Verifica, la Sintesi e la Trasformazione di Sistemi Software",
19-21 January 2000, Venice, Italy,
pages 47-48, Technical Report CS-2000-01, Computer Science Department, University Ca' Foscari of Venice, 2000.

Keywords: Zero Safe Nets, Refinement, Transactions, Petri Nets

(Postscript) (PDF)

"Zero-Safe Nets: Composing Nets via Transition Synchronization",
Roberto Bruni and Ugo Montanari,
in Proceedings of Colloquium on Petri Net Technologies for Modelling Communication Based Systems,
(Herbert Weber, Hartmut Ehrig, Wolfgang Reisig, Editors), 21-22 October 1999, Berlin, Germany,
pages 43-80, Fraunhofer Gesellschaft ISST, 1999.

Keywords: Zero Safe Nets, Petri Nets, Unfolding, Distributed Transactions

(Postscript) (PDF)

Abstract
Zero-safe nets have been introduced to extend classical Petri nets with a primitive notion of transition synchronization. To this aim, besides ordinary places, called stable, zero-safe nets are equipped with zero places, which cannot contain any token in a stable marking. An evolution between two stable markings is called transaction and can be a complex computation that involves zero places, with the restriction that no stable token generated in a transaction can be reused in the same transaction. The abstract counterpart of a generic zero-safe net B consists of an ordinary PT net whose places are the stable places of B, and whose transitions are the transactions of B. The two nets offer the refined and the abstract model of the same system, where the former can be much smaller than the latter, because of the transition synchronization mechanism. Depending on the chosen approach -- collective vs individual token philosophy -- two notions of transaction may be defined, each leading to different operational and abstract models. We survey the two approaches, discussing their main properties and showing several applications.

© Elsevier Science - DOI http://dx.doi.org/10.1016/S1571-0661(05)80302-0

"Functorial Semantics for Petri Nets under the Individual Token Philosophy",
Roberto Bruni, José Meseguer, Ugo Montanari and Vladimiro Sassone,
in Proceedings of CTCS99, 8th conference on Category Theory and Computer Science,
(Martin Hofmann, Giuseppe Rosolini, Dusko Pavlovic, Editors), 10-12 September 1999, Edinburgh, Scotland,
Electronic Notes in Theoretical Computer Science 29, 19 pages, Elsevier Science, 1999.
ISBN 0444507965.

Keywords: Petri Nets, Pre-Nets, Category Theory, Monoidal Categories, PMEqtl

(Postscript) (PDF)

Abstract
Although the algebraic semantics of place/transition Petri nets under the collective token philosophy has been fully explained in terms of (strictly) symmetric (strict) monoidal categories, the analogous construction under the individual token philosophy is not completely satisfactory because it lacks universality and also functoriality. We introduce the notion of pre-net to recover these aspects, obtaining a fully satisfactory categorical treatment centered on the notion of adjunction. This allows us to present a purely logical description of net behaviours under the individual token philosophy in terms of theories and theory morphisms in partial membership equational logic, yielding a complete match with the theory developed by the authors for the collective token view of nets.

© IEEE Press - DOI http://dx.doi.org/10.1109/LICS.1999.782620

"Cartesian Closed Double Categories, their Lambda-Notation, and the Pi-Calculus",
Roberto Bruni and Ugo Montanari,
in Proceedings of LICS99, 14th Annual IEEE Symposium on Logic in Computer Science,
2-5 July 1999, Trento, Italy,
pages 246-265, IEEE Computer Society, 1999.
ISBN 0-7695-0158-3 (July 1999).

Keywords: Category Theory, Double Categories, Pi-Calculus

(Postscript) (PDF)

Abstract
We introduce the notion of cartesian closed double category to provide mobile calculi for communicating systems with specific semantic models: One dimension is dedicated to compose systems and the other to compose their computations and their observations. Also, inspired by the connection between simply typed lambda-calculus and cartesian closed categories, we define a new typed framework, called double lambda-notation, which is able to express the abstraction/application and pairing/projection operations in all dimensions. In this development, we take the categorical presentation as a guidance in the interpretation of the formalism. A case study of the pi-calculus, where the double lambda-notation straightforwardly handles name passing and creation, concludes the presentation.

© Springer Verlag - DOI http://dx.doi.org/10.1007/978-3-540-49020-3_5

"Executable Tile Specifications for Process Calculi",
Roberto Bruni, José Meseguer and Ugo Montanari,
in Proceedings of FASE99, Fundamental Approaches to Software Engineering,
(Jean-Pierre Finance, Editor), 20-28 March 1999, Amsterdam, The Netherlands,
Lecture Notes in Computer Science 1577, pages 60-76, Springer Verlag, 1999.
ISBN 3-540-65718-5 (March 1999).

Keywords: Tile Logic, Rewriting Logic, Strategies, PMEqtl, Maude

(Postscript) (PDF)

Abstract
Tile logic extends rewriting logic by taking into account side-effects and rewriting synchronization. These aspects are very important when we model process calculi, because they allow us to express the dynamic interaction between processes and ``the rest of the world''. Since rewriting logic is the semantic basis of several language implementation efforts, we can define an executable specification of tile systems by mapping tile logic back into rewriting logic. In particular, this implementation requires the development of a metalayer to control rewritings, i.e., to discard computations that do not correspond to any deduction in tile logic. Our methodology is applied to term tile systems that cover and extend a wide-class of SOS formats for the specification of process calculi. The case study of full CCS, where the term tile format is needed to deal with recursion (in the form of the replicator operator), is discussed in detail.

"Tile Logic for Synchronized Rewriting of Concurrent Systems",
Roberto Bruni,
Ph.D. Thesis TD-99-01, Computer Science Department, University of Pisa, 1999.
Published March 1999.

Keywords: Zero Safe Nets, Tile Logic, Petri Nets, Rewriting Logic, Strategies, PMEqtl, Maude, Transactions, Category Theory, 2-Categories, Double Categories, Monoidal Categories

(Postscript)

Abstract
Tile logic is a framework to reason about the dynamic evolution of concurrent systems in a modular way. It extends rewriting logic (in the unconditional case) by adding rewriting synchronization and side effects. This dissertation concerns both theoretical and implementation issues of tile models of computation where the mathematical structures representing configurations (i.e., system states) and observations (i.e., observable actions) rely on the same common auxiliary structure (e.g., for tupling, projecting, etc.).
We proceed by considering maybe the simplest tile model (whose configurations and observations are just commutative monoids, and their sequential and parallel compositions coincide) and showing that it yields an original net model, called zero-safe net, which comes equipped with a primitive notion of transition synchronization, which is missing in ordinary Petri nets. The operational and abstract semantics of the model are expressed in the language of Net Theory and also as universal constructions in the language of Category Theory.
Then, two original versions of tile logic (called process and term tile logic respectively) are fully discussed, where net-process-like and usual term structures are employed for modelling configurations and observations. The categorical models for the two logics are introduced in terms of suitable classes of double categories. Then, the new model theory of 2EVH-categories is proposed to relate the categorical models of tile logic and rewriting logic. This is particularly important, because rewriting logic is the semantic basis of several language implementation efforts (Cafe, ELAN, Maude), and therefore a conservative mapping of tile logic back into rewriting logic can be useful to get executable specifications of tile systems.
The theory required to relate the two logics is presented in partial membership equational logic, a recently developed framework, which is particularly suitable to deal with categorical structures. The comparison yields a correct rewriting implementation of tile logic that uses a meta-layer to make sure that only tile computations are performed. Exploiting the reflective capabilities of the Maude language, such meta-layer is specified in terms of internal strategies. Several detailed examples illustrating the implementation of tile systems for concurrent process calculi conclude the presentation.

"Tile logic: Rewriting with side-effects (abstract)",
Roberto Bruni, José Meseguer and Ugo Montanari,
in Proceedings of First Workshop of the Project "Tecniche Formali per la Specifica, l'Analisi, la Verifica, la Sintesi e la Trasformazione di Sistemi Software",
21-23 December 1998, Rome, Italy,
pages 25-26, Technical Report SI-98/11, Computer Science Department, University La Sapienza of Rome, 1998.

Keywords: Tile Logic, Rewriting Logic, Strategies, PMEqtl, Maude

(Postscript) (PDF)

© Springer Verlag - DOI http://dx.doi.org/10.1007/3-540-49366-2_18

"A Comparison of Petri Net Semantics under the Collective Token Philosophy",
Roberto Bruni, José Meseguer, Ugo Montanari and Vladimiro Sassone,
in Proceedings of ASIAN98, 4th Asian Computing Science Conference,
(Jieh Hsiang, Atsushi Ohori, Editors), 8-10 December 1998, Manila, The Philippines,
Lecture Notes in Computer Science 1538, pages 225-244, Springer Verlag, 1998.
ISBN 3-540-65388-0 (December 1998).

Keywords: Petri Nets, Concurrent Transition Systems, Category Theory, PMEqtl, Maude

(Postscript) (PDF)

Abstract
In recent years, several semantics for place/transition Petri nets have been proposed that adopt the collective token philosophy. We investigate distinctions and similarities between three such models, namely configuration structures, concurrent transition systems, and (strictly) symmetric (strict) monoidal categories. We use the notion of adjunction to express each connection. We also present a purely logical description of the collective token interpretation of net behaviours in terms of theories and theory morphisms in partial membership equational logic.

© World Scientific

"Implementing Tile Systems: Some Examples from Process Calculi",
Roberto Bruni, José Meseguer and Ugo Montanari,
in Proceedings of ICTCS98, 6th Italian Conference on Theoretical Computer Science,
(Pierpaolo Degano, Ugo Vaccaro, Giuseppe Pirillo, Editors), 9-11 November 1998, Prato, Italy,
pages 168-179, World Scientific, 1998.
ISBN 981-02-3655-7 (November 1998).

Keywords: Tile Logic, Rewriting Logic, Strategies, PMEqtl, Maude

(Postscript) (PDF)

Abstract
This work reports on some useful applications of the tile model to the specification and execution of CCS-like process calculi. This activity is part of our ongoing research on the relation between tile logic and rewriting logic.

© Elsevier Science - DOI http://dx.doi.org/10.1016/S1571-0661(05)80016-7

"Internal Strategies in a Rewriting Implementation of Tile Systems",
Roberto Bruni, José Meseguer and Ugo Montanari,
in Proceedings of WRLA98, 2nd workshop on Rewriting Logic and its Applications,
(Claude Kirchner, Helene Kirchner, Editors), 1-4 September 1998, Pont-a-Mousson, France,
Electronic Notes in Theoretical Computer Science 15, pages 263-284, Elsevier Science, 1998.
ISBN 0444507787.

Keywords: Tile Logic, Rewriting Logic, Strategies, PMEqtl, Maude

(Postscript) (PDF)

Abstract
Tile logic extends rewriting logic, taking into account rewriting with side-effects and rewriting synchronization. Since rewriting logic is the semantic basis of several language implementation efforts, it is interesting to map tile logic back into rewriting logic in a conservative way, to obtain executable specifications of tile systems. The resulting implementation requires a meta-layer to control the rewritings, so that only tile proofs are accepted. However, by exploiting the reflective capabilities of the Maude language, such meta-layer can be specified as a kernel of internal strategies. It turns out that the required strategies are very general and can be reformulated in terms of search algorithms for non-confluent systems equipped with a notion of success. We formalize such strategies, giving their detailed description in Maude, and showing their application to modeling uniform tile systems.

© Elsevier Science - DOI http://dx.doi.org/10.1016/S1571-0661(05)80760-1

"A logic for modular descriptions of asynchronous and synchronized concurrent systems",
Roberto Bruni,
in Proceedings of WRLA98, 2nd workshop on Rewriting Logic and its Applications,
(Claude Kirchner, Helene Kirchner, Editors), 1-4 September 1998, Pont-a-Mousson, France,
Electronic Notes in Theoretical Computer Science 15, pages 161-172, Elsevier Science, 1998.
ISBN 0444507787.
Extended Abstract.

Keywords: Tile Logic, Rewriting Logic, Strategies, PMEqtl, Maude

(Postscript) (PDF)

Abstract
Tile logic is a framework to reason about the dynamic evolution of concurrent systems in a modular way, and it extends rewriting logic (in the unconditional case) by rewriting synchronization and side effects. The subject of this dissertation concerns some interesting tile models of computation such that the mathematical structures representing configurations (i.e., system states) and effects (i.e., observable actions) have in common some auxiliary structure (e.g., for tupling, projecting, etc.). In particular, two such logics (called process and term tile logic respectively) are fully discussed, where net-process-like and usual term structures are employed. The categorical models for the two logics are introduced in terms of suitable classes of double categories. Then, the new model theory of 2EVH-categories is proposed to relate the categorical models of tile logic and rewriting logic. This is particularly important, because rewriting logic is the semantic basis of several language implementation efforts (Cafe, ELAN, Maude), and therefore a conservative mapping of tile logic back into rewriting logic can be useful to get executable specifications of tile systems. The new model theory required to relate the two logics is presented in partial membership equational logic, a recently developed framework, which is particularly suitable to deal with categorical structures. The comparison yields a correct rewriting implementation of tile logic that uses a meta-layer to make sure that only tile proofs are performed. Exploiting the reflective capabilities of the Maude language, such meta-layer is specified in terms of internal strategies. Some detailed examples illustrating the implementation of tile systems for interesting concurrent process calculi conclude the presentation.

"Process and Term Tile Logic",
Roberto Bruni, José Meseguer and Ugo Montanari,
Technical Report SRI-CSL-98-06, SRI International, 1998.
Also Technical Report TR-98-09, Computer Science Department, University of Pisa (22 July 1998).

Keywords: Tile Logic, Rewriting Logic, Strategies, PMEqtl, Maude, 2-Categories, Double Categories

(Postscript)

Abstract
In a similar way as 2-categories can be regarded as a special case of double categories, rewriting logic (in the unconditional case) can be embedded into the more general tile logic, where also side-effects and rewriting synchronization are considered. Since rewriting logic is the semantic basis of several language implementation efforts, it is useful to map tile logic back into rewriting logic in a conservative way, to obtain executable specifications of tile systems. We extend the results of earlier work by two of the authors, focusing on some interesting cases where the mathematical structures representing configurations (i.e., states) and effects (i.e., observable actions) are very similar, in the sense that they have in common some auxiliary structure (e.g., for tupling, projecting, etc.). In particular, we give in full detail the descriptions of two such cases where (net) process-like and usual term structures are employed. Corresponding to these two cases, we introduce two categorical notions, namely, symmetric strict monoidal double category and cartesian double category with consistently chosen products, which seem to offer an adequate semantic setting for process and term tile systems. The new model theory of 2EVH-categories required to relate the categorical models of tile logic and rewriting logic is presented making use of a recently developed framework, called partial membership equational logic, particularly suitable to deal with categorical structures. Consequently, symmetric strict monoidal and cartesian classes of double categories and 2-categories are compared through their embedding in the corresponding versions of 2EVH-categories. As a result of this comparison, we obtain a correct rewriting implementation of tile logic. This implementation uses a meta-layer to control the rewritings, so that only tile proofs are accepted. Making use of the reflective capabilities of the Maude language, some (general) internal strategies are then defined to implement the mapping from tile systems into rewriting systems, and some interesting applications related to the implementation of concurrent process calculi are presented.

© Springer Verlag - DOI http://dx.doi.org/10.1007/3-540-48483-3_3

"Normal Forms for Partitions and Relations",
Roberto Bruni, Fabio Gadducci and Ugo Montanari,
in Proceedings of WADT98, 13th workshop on Recent Trends in Algebraic Development Techniques,
(José Luiz Fiadeiro, Editor), 2-4 April 1998, Lisbon, Portugal,
Lecture Notes in Computer Science 1589, pages 31-47, Springer Verlag, 1999.
ISBN 3-540-66246-4.

Keywords: Distributed Systems, Normal Forms, Sigma-Spaces, Partitions, Relations, (Co)Gs-Monoidal Categories

(Postscript) (PDF)

Abstract
In recent times there has been a growing interest towards algebraic structures which are able to express formalisms different from the well-known, tree-like presentation of terms. Many of the approaches adopted for such descriptions reveal a common, specific interest towards their application in the ``distributed and concurrent systems'' field, but an exhaustive comparison between them is very difficult because their presentations can be quite different. This work is a first step towards a unified view, which is able to recast all those formalisms into a more general one, where they can be easily compared. We introduce a general schema for describing a characteristic normal form for many interesting algebraic formalisms, and show that those normal forms can be thought of as arrows of suitable concrete monoidal categories, whose operations preserve the normal form itself.

© Elsevier Science - DOI http://dx.doi.org/10.1016/S1571-0661(05)80466-9

"Zero-Safe Nets, or Transition Synchronization Made Simple",
Roberto Bruni and Ugo Montanari,
in Proceedings of EXPRESS97, 4th workshop on Expressiveness in Concurrency,
(Catuscia Palamidessi, Joachim Parrow, Editors), 8-12 September 1997, Santa Margherita Ligure, Italy,
Electronic Notes in Theoretical Computer Science 7, pages 55-74, Elsevier Science, 1997.
ISBN 0444507701.

Keywords: Petri Nets, Zero Safe Nets, Category Theory, Transactions, Refinement

(Postscript) (PDF)

Abstract
In addition to ordinary places, called stable, zero-safe nets are equipped with zero places, which in a stable marking cannot contain any token. An evolution between two stable markings, instead, can be a complex computation called stable transaction, which may use zero places, but which is atomic when seen from stable places: no stable token generated in a transaction can be reused in the same transaction. Every zero-safe net has an ordinary Place-Transition net as its abstract counterpart, where only stable places are maintained, and where every transaction becomes a transition. The two nets allow us to look at the same system from both an abstract and a refined viewpoint. To achieve this result no new interaction mechanism is used, besides the ordinary token-pushing rules of nets. The refined zero-safe nets can be much smaller than their corresponding abstract P/T nets, since they take advantage of a transition synchronization mechanism. For instance, when transactions of unlimited length are possible in a zero safe net, the abstract net becomes infinite, even if the refined net is finite. In the second part of the paper two universal constructions - both following the Petri nets are monoids approach and the collective token philosophy - are used to give evidence of the naturality of our definitions. More precisely, the operational semantics of zero-safe nets is characterized as an adjunction, and the derivation of abstract P/T nets as a coreflection.

© Springer Verlag - DOI http://dx.doi.org/10.1007/3-540-64299-4_30

"Zero-Safe Nets: The Individual Token Approach",
Roberto Bruni and Ugo Montanari,
in Proceedings of WADT97, 12th workshop on Recent Trends in Algebraic Development Techniques,
(Francesco Parisi-Presicce, Editor), 3-7 June 1997, Tarquinia, Italy,
Lecture Notes in Computer Science 1376, pages 122-140, Springer Verlag, 1998.
ISBN 3-540-64299-4.

Keywords: Petri Nets, Zero Safe Nets, Category Theory, Transactions, Refinement

(Postscript) (PDF)

Abstract
In this paper we provide both an operational and an abstract concurrent semantics for zero-safe nets under the individual token philosophy. The main feature of zero-safe nets is a primitive notion of transition synchronization. Besides ordinary places, called stable places, zero-saf nets come equipped with zero places, which are empty in any stable marking. Connected transactions represent basic atomic computations of the system between stable markings. They must satisfy two main requirements: 1) to model interacting activities which cannot be decomposed into disjoint sub-activities, and 2) not to consume stable tokens which were generated in the same transaction. Zero tokens acts as triggers for the firings of the transitions which compose the transaction. The abstract counterpart of a zero-safe net consists of a P/T net where each transition locates a distinguished transaction. In the second part of the paper, following the Petri nets are monoids approach, we make use of category theory to analyze and motivate our framework. More precisely, the operational semantics of zero-safe nets is characterized as an adjunction, and the derivation of abstract P/T nets as a coreflection.

created: Tue Nov 30 2010 16:20:50 GMT+0100 (CET)