Pisa - Dipartimento di Informatica - Research Evaluation Exercise 1999


Models & languages
for
Open Distributed Systems



Ugo Montanari [*]



Keywords:

coalgebras, concurrency, coordination, graph rewriting, mobility, openness, security, structured transition systems, types, verification.

State of the Art and Trends


Highly distributed networks have now become a common platform for large scale distributed programming. While a number of useful internet applications can be developed using the standard client-server paradigm, internet applications distinguish themselves from traditional applications on scalability (huge number of users and nodes), connectivity (both availability and bandwidth), heterogeneity (operating systems and application software) and autonomy (of network nodes and administration domains having strong control of their resources). Hence, other programming paradigms (thin client and application servers, collaborative ``peer-to-peer'', code-on-demand, mobile agents) seem more appropriate for applications over internet. These emerging programming paradigms require on the one hand mechanisms to support mobility of code and computations, and effective infrastructures to support coordination and control of dynamically loaded software modules. On the other hand, an abstract semantic framework to formalize the model of computation of internet applications is clearly needed, and missing. Such semantic framework may provide the formal basis to discuss and motivate controversial design/implementation issues and to state and certify properties in a rigorous way. Concern for the limited understanding we have of network infrastructure and its applications has been explicitly expressed in the US PITAC documents [13]. Increased research efforts have been requested and planned in part.
More specifically, crucial issues to face when developing internet applications are about controlling component interactions, since some components can be dynamically downloaded from the network. For instance, the so called security architectures monitor the execution of mobile code to protect a host from external attacks to private information. Recently, the possibility has been explored of considering such issues at the level of language design, aiming at embedding dynamic linking and protection mechanisms in the languages. For instance, the Java language exploits type information and dynamic type checking as a foundation of its security: well-typed Java programs (and the corresponding verified bytecode) will never compromise the integrity of certain data.
Coordination [5,2] is a key concept for modeling and designing heterogeneous, distributed, open ended systems. It applies typically to systems consisting of a large number of software components, independently programmed in different programming languages, which may change their configuration during execution. Changes may be due both to external addition/deletion of software components and sites, and to transmission of code and resources made possible by mobility. Complex systems are designed and developed in a structured way, starting from the basic computational components and adding suitable software modules called coordinators. The potential reuse of both software agents and coordinators is increased, usually with acceptable overheads. Moreover, the formal description of coordination languages offers a natural framework for stating, checking and proving behavioral properties of open ended systems.
The scenario we outlined above is very appealing from the scientific point of view, since lots of the concepts to be made precise and most of the open problems involve fundamental issues of computer science research. More specifically, models, languages and logics are needed which are i) distributed, interactive & concurrent; ii) open & reconfigurable, iii) higher order & typed, iv) equipped with abstract compositional semantics; v) efficiently verifiable. While research has been quite successful on several of these issues separately, their combination is not well understood, and it is the object of our study. Here we extend our comments on the aspects of the above research scenario which are the most relevant for our approach.
In graph rewriting systems [14], rules specify local transformations that can be applied to graphs, possibly concurrently. As such, they are a powerful and flexible formalism suited for the specification of concurrent and distributed systems. They can be considered as a proper generalization of Petri nets, because the states are graphs (instead of (multi)sets), and rewriting rules are able to specify what part of the state must be preserved.
The use of coalgebras for the specification of interactive systems with a hidden state space is a valid alternative to algebraic methods based on observational equivalences [15,16]. In this perspective, a natural question is how and to what extent the rich body of techniques and results for the definition and the analysis of transition systems can be transferred to the coalgebraic framework.
The theory of mobile and higher order concurrency has been put under scrutiny only rather recently, and $\pi$% WIDTH=16 HEIGHT=17 -calculus [11] is definitely the most studied model. It can be considered as the concurrent counterpart of $\lambda$% WIDTH=16 HEIGHT=18 -calculus, which is the basis of most sequential languages. Connections between the two calculi have been studied for a while in the scientific community. However only limited results are known about embedding $\pi$% WIDTH=16 HEIGHT=17 -calculus (or similar kernel languages) into sufficiently rich type systems for higher order.
Distributed process calculi build the $\pi$% WIDTH=16 HEIGHT=17 -calculus to express some key issues of distributed computing, like security. We mention in particular the Join-Calculus [7], but several others have also been proposed (e.g. the Secure $\pi$% WIDTH=16 HEIGHT=17 -Calculus, the Distributed $\pi$% WIDTH=16 HEIGHT=17 -Calculus, the Ambient Calculus, and the Seal Calculus). Recent works have studied powerful type systems to enforce security property, e.g. [17,8], and the approach based on proof-carrying code [12]. This variety of models has motivated the introduction of more general approaches, like Action Calculi and Control Structures [10], Interaction Categories [1], Rewriting Logic [9], and Tile Logic [38]. All of them abstract at some extent from the concrete syntactical representations of process calculi to develop algebraic, universal models of distributed computing.
Among programming languages, there are languages designed to support distributed scope and access such as Obliq [4], and languages which provide mobility primitives within a distributed environment, such as Telescript [18] and others (e.g. Agent TCL, SUMATRA, Odyssey, Voyager).
Efficient algorithms and practical verification techniques have been developed for finite state labelled transition systems (automata). Finite state verification [6] has been very successful in all the situations where the control part and the data part can be cleanly separated and the control part is quite complex but finite state (e.g. communication protocols and hardware components). Actually, finite state verification techniques are the only case of verification widely used in practice.

Relevant Research Activities at the Department


In a few areas of historical relevance for this proposal, the research of the group has been, we think, well recognized by the scientific community. In this line we mention the work on concurrent process algebras. In the Esprit project Cedisys (Concurrent DIstributed SYStems, 1989-92), focused on this area, we had the role of coordinating partner. Another area is graph rewriting, where activity included the first model of synchronized graph rewriting, especially developed for distributed systems [31]. In this area we participated in Esprit Working Group Compugraph and Compugraph II. Finally, we mention the work on structured transition systems, where the algebraic structure of states is extended, using suitable categorical constructions, to transitions and computations. A monoidal structure, representing concurrency, yields Petri nets [41], while other kinds of structure yield Horn clauses and causal process algebras [29,36].
More recently, the general research area outlined in the previous section has been specifically instantiated in several original lines of research. The $\pi$% WIDTH=16 HEIGHT=17 -calculus was seen as a bridge from process algebras to mobile and higher order concurrent computing, and studied in detail from several points of view: A concurrent and distributed version of it was developed using graph rewriting techniques [44]; its operational definition was expressed in a restricted format, which automatically yields a reduction semantics [37]; and finite state verification was made possible for its finitary version [42]. In this line, we participated in Esprit project Confer and we are now part of working group Confer2, both dedicated to functional languages and calculi for concurrency and mobility.
The step from the $\pi$% WIDTH=16 HEIGHT=17 -calculus towards programming languages for mobility and coordination was taken recently with the definition [32] and initial implementation [21] of the language KLAIM (in collaboration with the university of Florence). Special attention was given to types for security and access control [33]. We participate in Esprit working group Coordina, which hosts most of the European community on the subject.
The approach developed for the finite state verification of the $\pi$% WIDTH=16 HEIGHT=17 -calculus turned out to be flexible and general enough to handle various history-dependent formalisms, where new actions are declared in certain transitions and referred to later: e.g. process algebras with causality and locality information, Petri nets equipped with history preserving bisimulation, and asynchronous $\pi$% WIDTH=16 HEIGHT=17 -calculus. Correspondingly, to make the approach independent from the actual syntax, certain classes of automata, called History Dependent Automata (HD-automata) have been introduced [43], which are able to allocate and garbage collect names. Without the latter, even simple agents could generate infinite state systems. An extended format able to represent HD-automata has been defined within the verification environment JACK developed in Pisa at IEI-CNR, and a tool able to translate from the $\pi$% WIDTH=16 HEIGHT=17 -calculus to HD-automata has been implemented [34]. Behavioral properties related to dynamic network connectivity, locality of resources and processes, and causality among events can be translated to finite HD-automata and formally verified.
In the area of graph rewriting, the emphasis has been on generalizing analogous results for Petri nets. We developed a concurrent semantics [26] based on event structures, processes [30], and unfolding constructions [20]. We also took advantage of this semantics to define the concurrent semantics of other formalisms, like the $\pi$% WIDTH=16 HEIGHT=17 -calculus (already mentioned), concurrent constraint programming, and the synchronous/asynchronous coordination of concurrent processes communicating via shared ports [44]. We are coordinating partner for the TMR network Getgrats and we participate in the Esprit working group Appligraph. We also contributed with a total of three chapters to the Handbooks on the subject, edited by Grzegorz Rozenberg. The first chapter is in the Handbook [14]. The others are [19,44].
The work on structured transition systems evolved in a new model, called tile logic [38]. The basic algebraic structure involved is that of a double category. Tiles (i.e. double cells) are rules defining the behaviour of open configurations, i.e. system components, which may interact through their interfaces. Rewriting logic (a rather general formalism developed by Jose Meseguer [9]) and SOS specifications are usually special cases of tile logic. However, synchronizations and observations are not possible in rewriting logic. Moreover, SOS handles only closed terms and action sequences, while in tile logic open configurations and their observations can be e.g. graphs and locality or interaction diagrams. Thus tile logic proposes itself as a natural, rather general logic for open, distributed, interactive systems with coordinators. It supports reasoning about the interactions between the systems being described and their environment.
Ongoing work on tile logic can be divided into three parts. The first is about the foundations of the model itself, and includes work on algebraic and logical properties of double categories and on the definition of first order [23] and higher order [25] versions of them. The second part studies how useful are tiles as a foundation for open, distributed and interactive systems [35]. Especially interesting are applications to software architectures [39], where the flexibility and compositionality aspects of the tile model can be valuable. The third part concerns how to implement tile logic: a convenient way is to translate it into rewriting logic. The SRI implementation is quite efficient, and the translation has been tested and found acceptable for realistic languages [24]. The theory under the translation approach is based on a new link between double categories and 2-categories. Of special interest is the study of data structures to be used for representing configurations and observations. Term graphs have been studied in detail in a categorical framework [27]. Moreover, a specific analysis [22] has shown that quite a few classes of graphs, including all those which have been actually used in the case studies, can be suitably axiomatized and equipped with standard forms. In addition, these classes can be represented efficiently in the SRI rewriting logic implementation taking advantage only of ACI axioms and alpha conversion, both built-in in the available version.
The last line of research is about coalgebras. Specifically, we are interested to explore how coalgebraic techniques can be used for representing distributed systems. To achieve compositionality, the collection of states af a coalgebra must form an algebra with respect to suitable operators (like parallel composition) [16], and leads us to natural questions about how the static (algebraic) and dynamic (coalgebraic) components of the system interact with each other. Preliminary studies [28] show that coalgebras defined on a category of algebras are adequate for certain classes of specifications (which include and nontrivially generalize most formats used in process algebras). This setting guarantees that bisimulation is a congruence with respect to the algebraic operators. Another study shows the adequacy of coalgebraic methods to represent mobility [40].

Short Term Plans and Expected Results


We outline the short term expected results on each of the research lines mentioned in the previous section.
A strong interaction is expected between the work on tiles and the more applied development on coordination languages and software architectures. We intend to provide the mathematical foundations of existing coordination languages by exploiting tile logic and its higher order version [25]. Moreover, research is under way to develop a process calculus representation of the KLAIM language in order to define notions of observations and of behavioral equivalences as a basis for verification. We also intend to check the theoretical developments by designing and implementing suggestive case studies, taking advantage of the KLAIM prototype [21].
About verification, we plan to extend the HD-automata techniques to the analysis of security protocols specified in the secure $\pi$% WIDTH=16 HEIGHT=17 -calculus. Moreover, we intend to address the problem of developing a specification logic for open and untrusted dynamic networks and its model checking techniques.
Continuing the study of the concurrent semantics of graph rewriting systems, we intend to lift some of our results (for example, the construction of the event structure associated with a graph rewriting system) from the level of a single system to a categorical formulation in terms of an adjunction between suitable categories of systems and models. This kind of results are known in the case of Petri nets, but their extension to graph rewriting systems is not trivial.
The foundational work on tiles will continue studying the double $\lambda$% WIDTH=16 HEIGHT=18 -notation associated to their cartesian closed version [25]. Preliminary results about the early version of the $\pi$% WIDTH=16 HEIGHT=17 -calculus show the adequacy of this notation for modeling name passing and creation in a straightforward way. Also the obvious connections between coalgebras and tiles (which naturally define compositional transition systems and are already equipped with bisimulation equivalences and congruences) will be studied.

Long Term Scenarios


Our plan is twofold. We want to carry on fundamental studies in the main stream of computer science, and we want also to contribute to the solution of the practical problems outlined in the state-of-the-art section, employing innovative techniques. The work will be theoretical, but also experimental in part.
On the fundamental side, we plan to achieve a better integration of methods and results for the theories of concurrency, higher order and types. Typed $\lambda$% WIDTH=16 HEIGHT=18 -calculus, in its various versions, is a powerful unifying tool for the sequential case, being able to model in a uniform way object oriented and functional programming, normalization, type checking, abstract data types, polymorphism, modules, subtyping, logic frameworks and proof checkers. Extensions of some of these results to distributed and concurrent programming would be important results. We will start from our work about $\pi$% WIDTH=16 HEIGHT=17 -calculus and tile logic.
Moreover, we plan some long-term work about coalgebras. The link between concepts like coinduction, final coalgebras, etc. and the notions of bisimulation, synchronization tree, HM-logic, etc., studied in process algebras is clear for simple languages like CCS. However, it is still far from being well understood whether the coalgebraic framework can be extended to different forms of distribution, compositionality and higher-order concurrency. We have preliminary results in [28,40].
On the more practical side, we propose to employ the notion of coordination as a fundamental structuring concept for interactive, open, secure architectures. Even if the idea of coordination has been around for a long time, its mathematical foundations are partially missing and we plan to study them relying on the formal notions we developed, like graph rewriting, tile logic and HD-automata. The long term (and ambitious) goal is to provide a semantic-based environment to specify, validate, implement and test internet applications. The main principles of our approach are (i) processes and their properties are network aware; (ii) network coordinators and processes are different entities; (iii) proving properties is a network coordination policy. The idea is that whatever features a dynamically evolving system will have, they will depend on the context of the underlying network (i.e. on net coordinators). The KLAIM [32] language adheres to these three design principles.
In a slightly different direction, we intend to develop a methodological framework based on graph rewriting and tile logic for accommodating the semantic integration of aspect-specific visual languages. The design process of distributed systems and of software architecture styles is often based on visual modeling techniques. A variety of visual languages were developed in the past years, like entity-relationship and class diagrams, statecharts, Petri nets, etc. To cope with the heterogeneity of application domains, domain-specific modeling languages have been proposed which integrate several aspect-specific visual techniques, e.g. OO modeling languages like UML [3] and its variations, Petri-net based languages, etc. Often this integration is done informally and only at the level of syntax, leading to ambiguities which make hard to support, for example, code generation and formal verification. We think that a key issue in this area is the development of specific algebras of graphs and graph rewriting techniques, providing operators which can be applied consistently not only to the static but also to the dynamic description of system components. We will try to apply our results in e.g. [27,22]. Also, tiles naturally integrate graph descriptions at both the static and the dynamic level, e.g. actor systems and interaction diagrams. In addition, tiles can be drawn employing suggestive, wire-and-box diagrams which can be composed in a naïve fashion. A visual specification language based on tiles would take advantage of these aspects.

Participants


Short CV's



Andrea Corradini

Present position Research Associate (Ricercatore).
Education Laurea in Scienze dell'Informazione (Master in Computer Science) at the University of Pisa, April 1984. ``Diploma'' in Computer Science at the ``Scuola Normale Superiore'' (1985). Ph.D. in Computer Science (1990).
Present research interests Coalgebraic and Algebraic Specification, Structured Transition Systems, Algebraic and Categorical Models of Rewriting, Semantics of Concurrency, Graph Transformation Systems.
Publications (Co-)Author of more than 50 published papers on topics including algebraic semantics of structured transition system, graph transformation systems and their truly concurrent semantics, infinitary extensions of term rewriting systems, coalgebraic specification. Five most relevant for the proposal: [29,30,27,26,28].
Project experience Network Coordinator of the TMR Network Getgrats (General Theory of Graph Transformation Systems).
Others Organizing Committee co-chairman of MASK Workshop 1995 and Joint Compugraph-Semagraph Workshop 1995. Co-editor of the special issue of Mathematical Structures in Computer Science, vol. 6(6), 1996, dedicated to the last workshop.

Gianluigi Ferrari

Present position Research Associate (Ricercatore).
Education Laurea in Scienze dell'Informazione (Master in Computer Science), Università di Pisa, April 1994. Dottorato di Ricerca in Informatica (PhD in Computer Science), 1990.
Present Research Interests Formal specification and verification of mobile systems, programming languages for network computing, tool support for mobile systems and theoretical aspects of distributed computing.
Publications Over 50 published papers in foundations of concurrent and distributed programming, programming languages and paradigms for network computing, security and finite state verification. Five most relevant for the proposal: [36,35,32,21,33].
Professional Activities Member of the Organizing Committee of the following scientific events: Procomet'94, Confer2 Workshop 1999.
Project Experience Coordinator and site coordinator of the CNR project Modelli Astratti di Computazione (Abstract Model of Computation) (1997-1999).

Ugo Montanari

Present position Full professor (professore ordinario).
Education Laurea in Ingegneria Elettronica (Master in Electronic Engineering) Politecnico di Milano, December 1966. Libera Docenza in Computer Science, April 1971.
Present research interests Semantics of Concurrency, Process Description and Object Oriented Languages, Constraint Programming, Graph Rewriting Systems, Coordination Models, Algebraic and Categorical Models of Concurrency.
Publications Over 250 published papers. Pioneering papers in: picture recognition, graphics, graph grammars, heuristically guided search, networks of constraints, algebraic data types, logic unification and true concurrency. Five most relevant for the proposal: [29,37,34,35,25].
Professional services and activities Member of the Editorial or Advisory Boards of the following international scientific journals: Fundamenta Informaticae, Logic Programming, Mathematical Structures in Computer Science, New Generation Computing, Science of Computer Programming, Theoretical Computer Science. Program or Organizing Committee chairman or Special Issue editor of nine events/issues (last five years). Recently member of the Organizing or Program Committees of: Amast, Caap, Ccl, Concur, Coordination, Fct, Icalp, Ilps, Lics, Mfcs, Tagt, Tapsoft, Wrla.
Selected project experience Presently site coordinator for Esprit Working Groups Appligraph, Confer2 and Coordination; and TMR Network Getgrats. Coordinator of the Esprit Basic Research Action 3011 Cedisys, 1989-92. Vice-chairman of the committee for the Italian Research Program in Informatics, 1991-93.

PhD Students, Postdocs and External Collaborators


Pisa PhD students: Paolo Baldan (fourth year) on graph rewriting, Emilio Tuosto (first year) on coordination languages. Buenos Aires PhD student: Dan Hirsch on software architectures. Postdoc: Roberto Bruni on tiles.
External collaborators: Rocco De Nicola and his group, Florence, on coordination languages; Stefania Gnesi, IEI-CNR Pisa, on verification; Jose Meseguer, Menlo Park, on Petri nets and tiles; Hartmut Ehrig, Berlin, on graph rewriting; Reiko Heckel, Paderborn, on coalgebras; Paola Inverardi, l'Aquila, on software architectures; Furio Honsell and Marina Lenisa, Udine, on coalgebras. PhD's formerly supervised by Ugo Montanari (thirteen in the past ten years) involved in the proposed research: Francesca Rossi, Padova, on graph rewriting; Fabio Gadducci, Edinburgh, on tiles and graph rewriting; Daniel Yankelevich, Buenos Aires, on verification of located processes; and Vladimiro Sassone, Catania, on Petri nets.

Bibliography




1
S. Abramsky,
Interaction Categories and Communicating Sequential Processes, in A.W. Roscoe (Ed.), A Classical Mind: Essay in Honour of C.A.R. Hoare, Prentice Hall (1995), 1-15.

2
J. Andreoli, C. Hankin, D. Le Metayer (Eds), Coordination Programming: Mechanisms, Models and Semantics, Imperial College Press, 1996.

3
G. Booch, J. Rumbaugh, and I. Jacobsen.
The Unified Modeling Language User Guide.
Addison-Wesley, 1998.

4
L. Cardelli.
A language with distributed scope.
Computing Systems, 8(1):27-59, MIT, 1995.

5
N. Carriero, D. Gelenter, Coordination Languages and Their Significance. Communications of the ACM, 35(2), 97-107, 1992.

6
E. Clarke and J. Wing Eds.
Formal Methods: State of the Art and Future Directions. Strategic Directions in Comp. Res. Formal Methods WG Rep. ACM Comp. Surv., December 1996.

7
C. Fournet, G. Gonthier, J.-L. Lévy, L. Maranget, D. Rémy. A Calculus of Mobile Agents. In Proc. CONCUR'96, LNCS 1119, 1996.

8
M. Hennessy, J. Riely, Type-safe Execution of Mobile Agents in Anonymous Networks. To appear in Secure Internet Programming: Security Issues for Distributed and Mobile Objects, LNCS State-Of-The-Art-Survey (J. Vitek and C. Jensen Eds.), 1999.

9
J. Meseguer.
Conditional Rewriting Logic as a Unified Model of Concurrency.
Theoretical Computer Science 96, 1992, pp. 73-155.

10
R. Milner.
Calculi for interaction.
Acta Informatica, 33:707-737, 1996.

11
R. Milner, J. Parrow, D. Walker. A calculus of mobile processes, (Part I and II). Information and Computation, 100:1-77, 1992.

12
G. Necula, P. Lee,
Safe, Untrusted Agents Using Proof-Carrying Code,
In Mobile Agents and Security, LNCS 1419, 1998.

13

President's Information Technology Advisory Committee.
Information Technology Research: Investing in Our Future.
Report to the President, http://www.hpcc.gov/ac/report/.

14
G. Rozenberg, Ed.
Handbook of Graph Grammars and Computing by Graph Transformation, Vol.1: Foundations.
World Scientific, 1997.

15
J.J.M.M. Rutten.
Universal coalgebra: a theory of systems.
Technical Report CS-R9652, CWI, 1996.
To appear in TCS.

16
D. Turi and G. Plotkin.
Towards a mathematical operational semantics.
In Proceedings LICS'97, pages 280-305, 1997.

17
D. Volpano, G. Smith
Confinement Properties for Programming Languages, SIGACT News 29, 1998.

18
J.E. White. Mobile Agents. In Software Agents (J.M. Bradshaw, Ed.), pp. 437-471, 1996.

Bibliography of the Proposers

19
Baldan, P.,Corradini, A., Ehrig, E., Löwe, M., Montanari, U. and Rossi, F.
Concurrent Semantics of Algebraic Graph Transformations.
In: G. Rozenberg, Ed., Handbook of Graph Grammars and Computing by Graph Transformation, Vol.3: Concurrency, Parallellism, and Distribution, to appear.

20
P. Baldan, A. Corradini, and U. Montanari.
Unfolding and Event Structure Semantics for Graph Grammars.
In W. Thomas, editor, Proceedings of FoSSaCS '99, volume 1578, pages 73-89. Springer Verlag, 1999.

21
L. Bettini, R. De Nicola, G. Ferrari, R. Pugliese,
Interactive Mobile Agents in XKLAIM,
Int. Workshop on Enabling Technologies: Infrastructure for Collaborative Enterprise, IEEE, 1998.

22
Bruni, R., Gadducci, F. and Montanari, U.
Normal Forms for Partitions and Relations, Proc. 13th Workshop on Algebraic Development Techniques, Lisbon, April 2-4, 1998.
In: Jose Luiz Fiadeiro, Ed., WADT'98, Springer LNCS1589, pp.31-47.

23
Bruni, R., Meseguer, J. and Montanari, U.
Symmetric and Cartesian Double Categories as a Semantic Framework for Tile Logic.
To appear in MSCS.

24
Bruni, R., Meseguer, J. and Montanari, U.
Executable Tile Specifications for Process Calculi.
In: Jean-Pierre Finance, Ed., FASE'99, Springer LNCS 1577, pp. 60-76.

25
R. Bruni, U. Montanari,
Cartesian Closed Double Categories, their Lambda-Notation, and the $\pi$% WIDTH=16 HEIGHT=17 -Calculus.
To appear in LICS'99, 1999.

26
A. Corradini.
Concurrent Graph and Term Graph Rewriting.
In U. Montanari and V. Sassone, editors, Proceedings CONCUR'96, volume 1119 of LNCS, pages 438-464. Springer Verlag, 1996.

27
A. Corradini, and F. Gadducci,
An Algebraic Presentation of Term Graphs, via GS-Monoidal Categories.
To appear in APCS, 1999.

28
A. Corradini, R. Heckel, and U. Montanari.
From SOS specifications to structured coalgebras: How to make bismulation a congruence.
In Proc. of the Second Workshop on Coalgebraic Methods in Computer Science (CMCS'99), volume 19 of ENTCS. Elsevier Science, 1999.

29
Corradini, A. and Montanari, U.
An Algebraic Semantics for Structured Transition Systems and its Application to Logic Programs.
TCS 103 (1992) pp. 51-106.

30
A. Corradini, U. Montanari, and F. Rossi.
Graph processes.
Fundamenta Informaticae, 26:241-265, 1996.

31

Degano, P. and Montanari, U.
A Model of Distributed Systems Based on Graph Rewriting.
Journal of the ACM Vol. 34, N2, April 1987, pp. 411-449.

32
R. De Nicola, G. Ferrari, R. Pugliese.
KLAIM: A Kernel Language for Agent Interaction and Mobility.
IEEE Transactions on Software Engineering, Vol 24 (5), 1998 Special Issue on Mobility and Network Aware Computing (G. Catalin-Roman, C. Ghezzi Eds), 1998.

33
R. De Nicola, G. Ferrari, R. Pugliese, B. Venneri.
Types for Access Control,
Theoretical Computer Science, to appear, 1999.

34
G. Ferrari, S. Gnesi, U. Montanari, M. Pistore, G. Ristori,
Verifying Mobile Processes in the HAL Environment.
Computer Aided Verification (CAV'98), LNCS, 1998.

35
G. Ferrari, U. Montanari,
Tile Formats for Located and Mobile Systems,
Information and Computation, to appear, 1999.

36
Ferrari G. L., Montanari, U. and Mowbray, M.
Structured Transition Systems with Parametric Observations: Minimal Realizations and Observational Congruences.
MSCS Vol. 7, pp.241-282, 1997.

37
Ferrari, G., Montanari, U. and Quaglia, P.
A $\pi$% WIDTH=16 HEIGHT=17 -calculus with Explicit Substitutions.
TCS-c Vol. 168, 1, Nov. 1996, pp.53-103.

38
F. Gadducci, U. Montanari.
The Tile Model.
In: G. Plotkin, C. Stirling and M. Tofte, Eds., Proofs, Languages and Interaction: Essays in Honour of Robin Milner, MIT Press, to appear.

39
Hirsch, D., Inverardi, P. and Montanari, U.
Modeling Software Architectures and Styles with Graph Grammars and Constraint Solving.
Proc. Working IFIP Conference on Software Architecture, February 1999.

40
Honsell, F., Lenisa, M., Montanari, U. and Pistore, M.
Final Semantics for the Pi-Calculus.
In: D. Gries and W-P. de Roever, Eds., PROCOMET'98, Chapman & Hall 1998, pp. 226-243.

41

Meseguer, J. and Montanari, U.
Petri Nets are Monoids.
Info and Co, Vol. 88, No. 2 (October 1990), 105-155.

42
Montanari, U. and Pistore, M.
Checking Bisimilarity for Finitary pi-calculus.
In: Insup Lee, Scott A. Smolka, Eds., CONCUR'95: Concurrency Theory, Springer LNCS 962, pp. 42-56.

43
Montanari, U. and Pistore, M.
An Introduction to History Dependent Automata.
In: Andrew Gordon, Andrew Pitts and Carolyn Talcott, Eds, Second Workshop on Higher-Order Operational Techniques in Semantics (HOOTS II), ENTCS, Vol. 10, 1998.

44
Montanari, U., Pistore, M. and Rossi, F.
Modeling Concurrent, Mobile and Coordinated Systems via Graph Transformations
In: G. Rozenberg, Ed., Handbook of Graph Grammars and Computing by Graph Transformation, Vol.3: Concurrency, Parallellism, and Distribution, to appear.



Footnotes

[*]
Dipartimento di Informatica, University of Pisa. With Andrea Corradini and Gianluigi Ferrari {andrea, giangi, ugo}@di.unipi.it. Proposal for the 1999 Evaluation Exercise, May 1999.


Index Page