Pisa  Dipartimento di Informatica  Research Evaluation Exercise 1999
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 clientserver 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 ``peertopeer'', codeondemand, 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: welltyped 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 calculus [11] is
definitely the most studied model. It can be considered as the concurrent
counterpart of 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 calculus (or similar kernel languages) into
sufficiently rich type systems for higher order.
Distributed process calculi build the calculus to express some
key issues of distributed computing, like security. We mention in
particular the JoinCalculus [7], but several others have
also been proposed (e.g. the Secure Calculus, the
Distributed 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
proofcarrying 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, 198992),
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
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 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
calculus turned out to be flexible and general enough to handle
various historydependent 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 calculus. Correspondingly,
to make the approach independent from the actual syntax, certain classes of
automata, called History Dependent Automata (HDautomata) 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 HDautomata has been defined
within the verification environment JACK developed in Pisa at IEICNR, and
a tool able to translate from the calculus to HDautomata 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 HDautomata 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 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 2categories. 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 builtin 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 HDautomata
techniques to the analysis of security protocols specified in the
secure 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
notation associated to their cartesian closed version
[25]. Preliminary results about the early version of the
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 stateoftheart 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
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 calculus and tile logic.
Moreover, we plan some longterm work about coalgebras. The link between
concepts like coinduction, final coalgebras, etc. and the notions of
bisimulation, synchronization tree, HMlogic, 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
higherorder 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 HDautomata. The long term (and ambitious) goal
is to provide a semanticbased 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 aspectspecific 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 entityrelationship and class diagrams,
statecharts, Petri nets, etc. To cope with the heterogeneity of application
domains, domainspecific modeling languages have been proposed which
integrate several aspectspecific visual techniques, e.g. OO modeling
languages like UML [3] and its variations, Petrinet 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, wireandbox 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 cochairman of MASK
Workshop 1995 and Joint CompugraphSemagraph Workshop 1995. Coeditor
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)
(19971999).
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, 198992.
Vicechairman of the committee for the Italian Research Program in
Informatics, 199193.
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,
IEICNR 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), 115.
 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.
AddisonWesley, 1998.
 4
 L. Cardelli.
A language with distributed scope.
Computing Systems, 8(1):2759, MIT, 1995.
 5
 N. Carriero, D. Gelenter,
Coordination Languages and Their Significance.
Communications of the ACM, 35(2), 97107, 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,
Typesafe Execution of Mobile Agents in Anonymous Networks.
To appear in Secure Internet Programming: Security Issues for
Distributed and Mobile Objects,
LNCS StateOfTheArtSurvey (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. 73155.
 10

R. Milner.
Calculi for interaction.
Acta Informatica, 33:707737, 1996.
 11
 R. Milner, J. Parrow, D. Walker.
A calculus of mobile processes, (Part I and II).
Information and Computation, 100:177, 1992.
 12
 G. Necula, P. Lee,
Safe, Untrusted Agents Using ProofCarrying 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 CSR9652, CWI, 1996.
To appear in TCS.
 16

D. Turi and G. Plotkin.
Towards a mathematical operational semantics.
In Proceedings LICS'97, pages 280305, 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. 437471, 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 7389. 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 24, 1998.
In: Jose Luiz Fiadeiro, Ed., WADT'98, Springer LNCS1589,
pp.3147.
 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: JeanPierre Finance, Ed., FASE'99, Springer LNCS
1577, pp. 6076.
 25
 R. Bruni, U. Montanari,
Cartesian Closed Double Categories, their LambdaNotation,
and the 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 438464. Springer Verlag, 1996.
 27
 A. Corradini, and F. Gadducci,
An Algebraic Presentation of Term Graphs, via GSMonoidal
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. 51106.
 30

A. Corradini, U. Montanari, and F. Rossi.
Graph processes.
Fundamenta Informaticae, 26:241265, 1996.
 31

Degano, P. and Montanari, U.
A Model of Distributed Systems Based on Graph
Rewriting.
Journal of the ACM Vol. 34, N†2, April 1987, pp. 411449.
 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. CatalinRoman, 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.241282, 1997.
 37
 Ferrari, G., Montanari, U. and Quaglia, P.
A calculus with Explicit
Substitutions.
TCSc Vol. 168, 1, Nov. 1996, pp.53103.
 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 PiCalculus.
In: D. Gries and WP. de Roever, Eds., PROCOMET'98,
Chapman & Hall 1998, pp. 226243.
 41

Meseguer, J. and Montanari, U.
Petri Nets are Monoids.
Info and Co, Vol. 88, No. 2 (October 1990), 105155.
 42
 Montanari, U. and Pistore, M.
Checking Bisimilarity for Finitary
picalculus.
In: Insup Lee, Scott A. Smolka, Eds., CONCUR'95: Concurrency
Theory, Springer LNCS 962, pp. 4256.
 43
 Montanari, U. and Pistore, M.
An Introduction to History Dependent
Automata.
In: Andrew Gordon, Andrew Pitts and Carolyn Talcott, Eds, Second
Workshop on HigherOrder 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