2016

Cinzia Di Giusto, Jorge A. Pérez. Event-based run-time adaptation in communication-centric systems..
Formal Asp. Comput. 28(4): 531-566 (2016)
Authors :
Cinzia Di Giusto, Jorge A. Pérez
Title : Event-based run-time adaptation in communication-centric systems.
Reference :
Formal Asp. Comput. 28(4): 531-566 (2016)
Type : JOURNALS
Year : 2016
Abstract :
Communication-centric systems are software systems built as assemblies of distributed artifacts that interact following predefined communication protocols. Session-based concurrency is a type-based approach to ensure the conformance of communication-centric systems to such protocols. This paper presents a model of session-based concurrency with mechanisms for run-time adaptation. Our model allows us to specify communication-centric systems whose session behavior can be dynamically updated at run-time. We improve on previous work by proposing an event-based approach: adaptation requests, issued by the system itself or by its context, are assimilated to events which may trigger adaptation routines. These routines exploit type-directed checks to enable the reconfiguration of processes with active protocols. We equip our model with a type system that ensures communication safety and consistency properties: while safety guarantees absence of run-time communication errors, consistency ensures that update actions do not disrupt already established session protocols. We provide soundness results for binary and multiparty protocols.

2015

C. Di Giusto, J. A. Pérez. Disciplined structured communications with disciplined runtime adaptation.
Science of Computer Programming, 97: 235-265 (2015)
Authors :
C. Di Giusto, J. A. Pérez
Title : Disciplined structured communications with disciplined runtime adaptation
Reference :
Science of Computer Programming, 97: 235-265 (2015)
Type : JOURNALS
Year : 2015
Resources : PDF icon Pdf
Abstract :
Session types offer a powerful type-theoretic foundation for the analysis of structured communications, as commonly found in service-oriented systems. They are defined upon core programming calculi which offer only limited support for expressing requirements related to runtime adaptation. This is unfortunate, as service-oriented systems are increasingly being deployed upon highly dynamic infrastructures in which such requirements are central concerns. In previous work, we developed a process calculi framework of adaptable processes, in which concurrent processes can be replaced, suspended, or discarded at runtime. In this paper, we propose a session type discipline for a calculus with adaptable processes. Our typed framework offers a simple alternative for integrating runtime adaptation mechanisms in the modeling and analysis of structured communications. We show that well-typed processes enjoy safety and consistency properties: while the former property ensures the absence of communication errors at runtime, the latter guarantees that active session behavior is never disrupted by adaptation actions.
F. Delaplace, C. Di Giusto, J.-L. Giavitto, H. Klaudel and A. Spicher. Activity Networks with Delays application to toxicity analysis .
Research report
Authors :
F. Delaplace, C. Di Giusto, J.-L. Giavitto, H. Klaudel and A. Spicher
Title : Activity Networks with Delays application to toxicity analysis
Reference :
Research report
Type : TECHNICAL REPORTS
Year : 2015
Abstract :
ANDy, Activity Networks with Delays, is a discrete time framework aimed to the qualitative modelling of time-dependent activities such as biological networks and regulatory pathways. Activities involve entities playing the role of activators, inhibitors or products of biochemical network operation. Activities may have given duration, i.e., the time required to obtain results. An entity may represent an object (e.g., an agent, a biochemical species or a family of thereof) with a local attribute, a state denoting its level (e.g., concentration, strength). Entities levels may change as a result of an activity or may decrease gradually as time passes by. The semantics of ANDy is formally given via high-level Petri nets ensuring this way some modularity. As main results we show that ANDy systems have finite state representations even for potentially infinite processes and that ANDy's concept of time has a direct counterpart in timed automata. These results together with a modular and concise syntax make ANDy suitable for an easy and natural modelling of time-dependent (biological) systems. We conclude our paper with a general discussion on toxic behaviours, in particular we present a classification of toxicity properties and give some hints on how they can be verified with existing tools on ANDy systems.

2014

C. Di Giusto, H. Klaudel and Franck Delaplace. Systemic approach for toxicity analysis.
BioPPN, Petri Nets 2014: 30-44
Authors :
C. Di Giusto, H. Klaudel and Franck Delaplace
Title : Systemic approach for toxicity analysis
Reference :
BioPPN, Petri Nets 2014: 30-44
Type : WORKSHOPS AND POSTERS
Year : 2014
Resources : PDF icon Pdf
Abstract :
A high-level Petri net framework is introduced for the toxic risk assessment in biological and bio-synthetic systems. Unlike empirical techniques mostly used in toxicology or toxicogenomics, we propose a systemic approach consisting of a series of behavioral rules (reactions) that depend on abstract discrete \expression" levels of involved agents (species). We introduce a finite state high-level Petri net model allowing exhaustive verification (model-checking) of properties related to equilibrium alteration or appearing of hazardous behaviors. The approach is applied to the study of the impact of the aspartame assimilation into the blood glucose regulation process

2013

S. Mimram and C. Di Giusto. A Cathegorical Theory of Patches.
ENTCS, 298: pp. 283-307 (2013)
Authors :
S. Mimram and C. Di Giusto
Title : A Cathegorical Theory of Patches
Reference :
ENTCS, 298: pp. 283-307 (2013)
Type : JOURNALS
Year : 2013
Abstract :
When working with distant collaborators on the same documents, one often uses a version control system, which is a program tracking the history of files and helping importing modifications brought by others as patches. The implementation of such a system requires to handle lots of situations depending on the operations performed by users on files, and it is thus difficult to ensure that all the corner cases have been correctly addressed. Here, instead of verifying the implementation of such a system, we adopt a complementary approach: we introduce a theoretical model, which is defined abstractly by the universal property that it should satisfy, and work out a concrete description of it. We begin by defining a category of files and patches, where the operation of merging the effect of two coinitial patches is defined by pushout. Since two patches can be incompatible, such a pushout does not necessarily exist in the category, which raises the question of which is the correct category to represent and manipulate files in conflicting state. We provide an answer by investigating the free completion of the category of files under finite colimits, and give an explicit description of this category: its objects are finite sets labeled by lines equipped with a transitive relation and morphisms are partial functions respecting labeling and relations.
C. Di Giusto and J.A. Pèrez . Disciplined Structured Communications with Safe Runtime Adaptation.
In SAC 2013, ACM, pages 1913-1918, 2013.
Authors :
C. Di Giusto and J.A. Pèrez
Title : Disciplined Structured Communications with Safe Runtime Adaptation
Reference :
In SAC 2013, ACM, pages 1913-1918, 2013.
Type : PROCEEDINGS OF CONFERENCES
Year : 2013
Resources : PDF icon Pdf
Abstract :
Session types offer a powerful type-theoretic foundation for the analysis of structured communications, as commonly found in service-oriented systems. They are defined upon core programming calculi which offer only limited support for expressing adaptation and evolvability requirements. This is unfortunate, as service-oriented systems are increasingly being deployed upon highly dynamic infrastructures in which such requirements are central concerns. In previous work, we developed a process calculi frame- work of adaptable processes, in which concurrent processes can be replaced, suspended, or discarded at runtime. In this paper, we propose a session types discipline for a calculus with adaptable processes. Our framework offers an alternative for integrating runtime adaptation mechanisms in the analysis of structured communications. We show that well-typed processes enjoy consistency: communicating behavior is never interrupted by evolvability actions.
C. Di Giusto and J.A. Pèrez. Session Types with Runtime Adaptation: Overview and Examples.
PLACES 2013: 21-32
Authors :
C. Di Giusto and J.A. Pèrez
Title : Session Types with Runtime Adaptation: Overview and Examples
Reference :
PLACES 2013: 21-32
Type : WORKSHOPS AND POSTERS
Year : 2013
Resources : PDF icon Pdf
Abstract :
In recent work, we have developed a session types discipline for a calculus that features the usual constructs for session establishment and communication, but also two novel constructs that enable communicating processes to be stopped, duplicated, or discarded at runtime. The aim is to understand whether known techniques for the static analysis of structured communications scale up to the challenging context of context-aware, adaptable distributed systems, in which disciplined interaction and runtime adaptation are intertwined concerns. In this short note, we summarize the main features of our session-typed framework with runtime adaptation, and recall its basic correctness properties. We illustrate our framework by means of examples. In particular, we present a session representation of supervision trees, a mechanism for enforcing fault-tolerant applications in the Erlang language.

2012

M. Bravetti, C. Di Giusto, J.A. Pèrez and G. Zavattaro. Adaptable processes.
Logical Methods for Computer Science Vol. 8(4:13) 2012, pp. 1-71.
Authors :
M. Bravetti, C. Di Giusto, J.A. Pèrez and G. Zavattaro
Title : Adaptable processes
Reference :
Logical Methods for Computer Science Vol. 8(4:13) 2012, pp. 1-71.
Type : JOURNALS
Year : 2012
Abstract :
We propose the concept of adaptable processes as a way of overcoming the limitations that process calculi have for describing patterns of dynamic process evolution. Such patterns rely on direct ways of controlling the behavior and location of running processes, and so they are at the heart of the adaptation capabilities present in many modern concurrent systems. Adaptable processes have a location and are sensible to actions of dynamic update at runtime; this allows to express a wide range of evolvability patterns for concurrent processes. We introduce a core calculus of adaptable processes and propose two verification problems for them: bounded and eventual adaptation. While the former ensures that the number of consecutive erroneous states that can be traversed during a computation is bound by some given number k, the latter ensures that if the system enters into a state with errors then a state without errors will be eventually reached. We study the (un)decidability of these two problems in several variants of the calculus, which result from considering dynamic and static topologies of adaptable processes as well as different evolvability patterns. Rather than a specification language, our calculus intends to be a basis for investigating the fundamental properties of evolvable processes and for developing richer languages with evolvability capabilities.
M. Bravetti, C. Di Giusto, J.A. Pèrez and G. Zavattaro. Towards the Verification of Adaptable Processes.
In ISoLA 2012, volume 7609 of LNCS, pp 269-283, 2012.
Authors :
M. Bravetti, C. Di Giusto, J.A. Pèrez and G. Zavattaro
Title : Towards the Verification of Adaptable Processes
Reference :
In ISoLA 2012, volume 7609 of LNCS, pp 269-283, 2012.
Type : PROCEEDINGS OF CONFERENCES
Year : 2012
Resources : PDF icon Pdf
Abstract :
In prior work, with the aim of formally modeling and analyzing the behavior of concurrent processes with forms of dynamic evolution, we have pro- posed a process calculus of adaptable processes. Our proposal addressed the (un)decidability of two safety properties related to error occurrence. In order to allow for a more comprehensive verification framework for adaptable processes, the ability to express general properties is most desirable. In this paper we address this important issue: we explain how the proof techniques for (un)decidability results for adaptable processes generalize to a simple yet expressive temporal logic over adaptable processes. We provide examples of the expressiveness of the logic and its significance in relation with the calculus of adaptable processes.
C. Di Giusto, M. Gabbrielli, and M.C. Meo. On the Expressive Power of Multiple Heads in CHR.
ACM Transactions on Computational Logic 13(1): 6 (2012).
Authors :
C. Di Giusto, M. Gabbrielli, and M.C. Meo
Title : On the Expressive Power of Multiple Heads in CHR
Reference :
ACM Transactions on Computational Logic 13(1): 6 (2012).
Type : JOURNALS
Year : 2012
Resources : PDF icon Pdf
Abstract :
Constraint Handling Rules (CHR) is a committed-choice declarative language that has been originally designed for writing constraint solvers and is nowadays a general purpose language. CHR programs consist of multiheaded guarded rules which allow to rewrite constraints into simpler ones until a solved form is reached. Many empirical evidences suggest that multiple heads augment the expressive power of the language, however no formal result in this direction has been proved, so far.
In the first part of this article we analyze the Turing completeness of CHR with respect to the underlying constraint theory. We prove that if the constraint theory is powerful enough then restricting to single head rules does not affect the Turing completeness of the language. On the other hand, differently from the case of the multiheaded language, the single head CHR language is not Turing powerful when the underlying signature (for the constraint theory) does not contain function symbols.
In the second part we prove that, no matter which constraint theory is considered, under some reasonable assumptions it is not possible to encode the CHR language (with multi-headed rules) into a single headed language while preserving the semantics of the programs. We also show that, under some stronger assumptions, considering an increasing number of atoms in the head of a rule augments the expressive power of the language.
These results provide a formal proof for the claim that multiple heads augment the expressive power of the CHR language.

2011

C. Di Giusto, J.B. Stefani. Revisiting glues for component-based systems.
In COORDINATION 2011, volume 6721 of LNCS, pages 16-30, 2011
Authors :
C. Di Giusto, J.B. Stefani
Title : Revisiting glues for component-based systems
Reference :
In COORDINATION 2011, volume 6721 of LNCS, pages 16-30, 2011
Type : PROCEEDINGS OF CONFERENCES
Year : 2011
Resources : PDF icon Pdf
Abstract :
We take a fresh look at the expressivity of BIP, a recent influential formal component model developed by J. Sifakis et al. We introduce a process calculus, called CAB, that models composite components as the combination of a glue (using BIP terminology) and subcomponents, and that constitutes a conservative extension of BIP with more dynamic forms of glues. We study the Turing completeness of CAB variants that differ only in their language for glues. We show that limiting the glue language to BIP glues suffices to obtain Turing-completeness, whereas re- moving priorities from the control language loses Turing-completeness. We also show that adding a simple form of dynamic component creation in the control language without priorities is enough to regain Turing completeness. These results complement those obtained on BIP, highlighting in particular the key role of priorities for expressivity.
M. Bravetti, C. Di Giusto, J.A. Pèrez and G. Zavattaro. Adaptable processes (Extended Abstract).
 In FMOODS-FORTE 2011, volume 6722 of LNCS, pages 90-105, 2011.
Authors :
M. Bravetti, C. Di Giusto, J.A. Pèrez and G. Zavattaro
Title : Adaptable processes (Extended Abstract)
Reference :
 In FMOODS-FORTE 2011, volume 6722 of LNCS, pages 90-105, 2011.
Type : PROCEEDINGS OF CONFERENCES
Year : 2011
Resources : PDF icon Pdf
Abstract :
We propose the concept of adaptable processes as a way of overcoming the limitations that process calculi have for describing patterns of dynamic process evolution. Such patterns rely on direct ways of controlling the behavior and location of running processes, and so they are at the heart of the adaptation capabilities present in many modern concurrent systems. Adaptable processes have a location and are sensible to actions of dynamic update at runtime. This allows to express a wide range of evolvability patterns for processes. We introduce a core calculus of adaptable processes and propose two verification problems for them: bounded and eventual adaptation. While the former ensures that at most k consecutive errors will arise in future states, the latter ensures that if the system enters into an error state then it will eventually reach a correct state. We study the (un)decidability of these two problems in different fragments of the calculus. Rather than a specification language, our calculus intends to be a basis for investigating the fundamental properties of evolvable processes and for developing richer languages with evolvability capabilities.
M. Dalla Preda and C. Di Giusto. Hunting distributed malware with the k-calculus.
In FCT 2011, volume 6914 of Lecture Notes in Computer Science, pages 102-113, 2011
Authors :
M. Dalla Preda and C. Di Giusto
Title : Hunting distributed malware with the k-calculus
Reference :
In FCT 2011, volume 6914 of Lecture Notes in Computer Science, pages 102-113, 2011
Type : PROCEEDINGS OF CONFERENCES
Year : 2011
Resources : PDF icon Pdf
Abstract :
The defense of computer systems from malicious software attacks, such as viruses and worms, is a key aspect of computer security. The analogy between malicious software and biological infections suggested us to use the k-calculus, a formalism originally developed for the analysis of biological systems, for the formalization and analysis of malicious software. By modeling the different actors involved in a malicious code attack in the k-calculus and by simulating their behavior, it is possible to extract important information that can drive in the choice of the defense technique to apply.

2010

M. Bravetti, C. Di Giusto, J.A. Pèrez and Gianluigi Zavattaro. Steps on the Road to Component Evolvability.
Appeared as Technical Report of FACS 2010-Doctoral Track: Technical Report DI-CCTC-10-14, DI-CCTC Universidade do Minho, 2010
Authors :
M. Bravetti, C. Di Giusto, J.A. Pèrez and Gianluigi Zavattaro
Title : Steps on the Road to Component Evolvability
Reference :
Appeared as Technical Report of FACS 2010-Doctoral Track: Technical Report DI-CCTC-10-14, DI-CCTC Universidade do Minho, 2010
Type : WORKSHOPS AND POSTERS
Year : 2010
Resources : PDF icon Pdf
Abstract :
We have recently developed a calculus for dynamically evolvable ag- gregations of components. The calculus extends CCS with primitives for describ- ing components and their evolvability capabilities. Central to these novel prim- itives is a restricted form of higher-order communication of processes involved in update operations. The origins of our calculus for components can indeed be traced back to our own previous work on the expressiveness and decidability results for core higher-order process calculi. Here we overview these previous works, and discuss the motivations and design decisions that led us from higher- order process calculi to calculi for component evolvability.

2009

C. Di Giusto, M. Gabbrielli and M.C.Meo. Expressiveness of Multiple Heads in CHR.
In SOFSEM 2009, volume 5404 of LNCS pages 205-216, 2009.
Authors :
C. Di Giusto, M. Gabbrielli and M.C.Meo
Title : Expressiveness of Multiple Heads in CHR
Reference :
In SOFSEM 2009, volume 5404 of LNCS pages 205-216, 2009.
Type : PROCEEDINGS OF CONFERENCES
Year : 2009
Resources : PDF icon Pdf
Abstract :
Constraint Handling Rules (CHR) is a general purpose, committed- choice declarative language which, differently from other similar languages, uses multi-headed (guarded) rules. In this paper we prove that multiple heads augment the expressive power of the language. In fact, we first show that restricting to single head rules affects the Turing completeness of CHR, provided that the underlying signature (for the constraint theory) does not contain function symbols. Next we show that, also when considering generic constraint theories, under some rather reasonable assumptions it is not possible to encode CHR (with multi-headed rules) into a single-headed CHR language while preserving the semantics of programs. As a corollary we obtain that, under these assumptions, CHR can be encoded neither in (constraint) logic programming nor in pure Prolog.
G. Delzanno, C. Di Giusto, M. Gabbrielli, C. Laneve and G. Zavattaro. The kappa-Lattice: Decidability Boundaries for Qualitative Analysis in Biological Languages.
In CMSB 2009 volume 5684 of Lecture Notes in Bioinformatics, pages 158-172, 2009.
Authors :
G. Delzanno, C. Di Giusto, M. Gabbrielli, C. Laneve and G. Zavattaro
Title : The kappa-Lattice: Decidability Boundaries for Qualitative Analysis in Biological Languages
Reference :
In CMSB 2009 volume 5684 of Lecture Notes in Bioinformatics, pages 158-172, 2009.
Type : PROCEEDINGS OF CONFERENCES
Year : 2009
Resources : PDF icon Pdf
Abstract :
The k-calculus is a formalism for modelling molecular biology where molecules are terms with internal state and sites, bonds are represented by shared names labeling sites, and reactions are represented by rewriting rules. Depending on the shape of the rewriting rules, a lattice of dialects of k can be obtained. We analyze the expressive power of some of these dialects by focusing on the thin boundary between decidability and undecidability for problems like reachability and coverability.
C. Di Giusto, J.A. Pèrez and G. Zavattaro. On the Expressiveness of Forwarding in Higher-Order Communication.
In ICTAC 2009 volume 5688 of LNCS, pages 155-169, 2009.
Authors :
C. Di Giusto, J.A. Pèrez and G. Zavattaro
Title : On the Expressiveness of Forwarding in Higher-Order Communication
Reference :
In ICTAC 2009 volume 5688 of LNCS, pages 155-169, 2009.
Type : PROCEEDINGS OF CONFERENCES
Year : 2009
Resources : PDF icon Pdf
Abstract :
In higher-order process calculi the values exchanged in communications may contain processes. There are only two capabilities for received processes: execution and forwarding. Here we propose a limited form of forwarding: output actions can only communicate the parallel composition of statically known closed processes and processes received through previously executed input actions. We study the expressiveness of a higher-order process calculus featuring this style of communication. Our main result shows that in this calculus termination is decidable while convergence is undecidable.
Cinzia Di Giusto. Expressiveness of Concurrent Languages.
PhD Thesis, University of Bologna 2009
Authors :
Cinzia Di Giusto
Title : Expressiveness of Concurrent Languages
Reference :
PhD Thesis, University of Bologna 2009
Type : TECHNICAL REPORTS
Year : 2009
Resources : PDF icon Pdf
C. Di Giusto, C. Versari and A. Vitale. Towards a minimal calculus for complexation.
In CMSB 2009, poster session. Appeared as Technical Report of University of Pisa: TR-09-09
Authors :
C. Di Giusto, C. Versari and A. Vitale
Title : Towards a minimal calculus for complexation
Reference :
In CMSB 2009, poster session. Appeared as Technical Report of University of Pisa: TR-09-09
Type : WORKSHOPS AND POSTERS
Year : 2009
Resources : PDF icon Pdf
,
Resources : PDF icon Poster
Abstract :
We present here a termination preserving encoding of Minsky Ma- chines in a particularly restricted fragment of the κ-calculus where only one species with no fields is admitted and only binary rules are allowed.
C. Di Giusto and J.A. Pèrez. Move vs Copy: Towards a Formal Comparison of Ambients and Higher-Order Process Calculi.
Appeared as Technical Report of ICTCS 2009, pp: 107-112
Authors :
C. Di Giusto and J.A. Pèrez
Title : Move vs Copy: Towards a Formal Comparison of Ambients and Higher-Order Process Calculi
Reference :
Appeared as Technical Report of ICTCS 2009, pp: 107-112
Type : WORKSHOPS AND POSTERS
Year : 2009
Resources : PDF icon Pdf
Abstract :
We describe ongoing work on a formal comparison between Ambient-like and higher-order process calculi. Both formalisms are similar in that they communicate complex objects. Also, in both cases the associated behavioral theory can be hard to define, and employs similar techniques. However, some other characteristics suggest deep differences. Communication in Ambients resembles a “move” operation whereas in higher-order settings it is better assimilated to a “copy” operation. Most notably, there is a subtle discrepancy when it comes to scoping: most (higher-order) process calculi adopt static scoping only, whereas Ambient-like formalisms exhibit features of both static scoping and dynamic binding. As a first step towards a comparison, here we present an encoding of Ambients into a higher-order calculus with dynamic scoping.

2008

C. Di Giusto and M. Gabbrielli. Full abstraction for Linda.
In ESOP '08, volume 4960 of LNCS, pages 78-92, 2008.
Authors :
C. Di Giusto and M. Gabbrielli
Title : Full abstraction for Linda
Reference :
In ESOP '08, volume 4960 of LNCS, pages 78-92, 2008.
Type : PROCEEDINGS OF CONFERENCES
Year : 2008
Resources : PDF icon esop08.pdf
Abstract :
This paper investigates full abstraction of a trace semantics for two Linda-like languages. The first language provides primitives for adding and re- moving messages from a shared memory, local choice, parallel composition and recursion. The second one adds the possibility of checking for the absence of a message in the store. After having defined a denotational semantics based on traces, we obtain fully abstract semantics for both languages by using suitable abstractions in order to identify different traces which do not correspond to different operational behaviours.

2007

J. Aranda, C. Di Giusto, M. Nielsen and F. Valencia. CCS with Replication in the Chomsky Hierarchy: The Expressive Power of Divergence.
In APLAS '07, volume 4807 of LNCS, pages 383-398, 2007
Authors :
J. Aranda, C. Di Giusto, M. Nielsen and F. Valencia
Title : CCS with Replication in the Chomsky Hierarchy: The Expressive Power of Divergence
Reference :
In APLAS '07, volume 4807 of LNCS, pages 383-398, 2007
Type : PROCEEDINGS OF CONFERENCES
Year : 2007
Resources : PDF icon Pdf
Abstract :
A remarkable result in [4] shows that in spite of its being less expressive than CCS w.r.t. weak bisimilarity, CCS! (a CCS variant where infinite behavior is specified by using replication rather than recursion) is Turing powerful. This is done by encoding Random Access Machines (RAM) in CCS!. The encoding is said to be non-faithful because it may move from a state which can lead to termination into a divergent one which do not correspond to any configuration of the encoded RAM. I.e., the encoding is not termination preserving. In this paper we study the existence of faithful encodings into CCS! of models of computability strictly less expressive than Turing Machines. Namely, grammars of Types 1 (Context Sensitive Languages), 2 (Context Free Languages) and 3 (Regular Languages) in the Chomsky Hierarchy. We provide faithful encodings of Type 3 grammars. We show that it is impossible to provide a faithful encoding of Type 2 grammars and that termination-preserving CCS! processes can generate languages which are not Type 2. We finally show that the languages generated by termination-preserving CCS! processes are Type 1.

2006

J. Aranda, C. Di Giusto, C. Palamidessi and F. Valencia. On Recursion, Replication and Scope Mechanisms in Process Calculi.
In FMCO 2006, volume 4709 of LNCS, pages 185-206, 2006
Authors :
J. Aranda, C. Di Giusto, C. Palamidessi and F. Valencia
Title : On Recursion, Replication and Scope Mechanisms in Process Calculi
Reference :
In FMCO 2006, volume 4709 of LNCS, pages 185-206, 2006
Type : PROCEEDINGS OF CONFERENCES
Year : 2006
Resources : PDF icon fmco07.pdf
Abstract :
In this paper we shall survey and discuss in detail the work on the relative expressiveness of recursion and replication in various process calculi. Namely, CCS, the pi-calculus, the Ambient calculus, Concurrent Constraint Programming and calculi for Cryptographic Protocols. We shall give evidence that the ability of expressing recursive behaviour via replication often depends on the scoping mechanisms of the given calculus which compensate for the restriction of replication.

2004

P. Andreetto, V. Borgia, A. Dorigo, A. Gianelle, M. Mordacchini, M. Sgaravatto, L. Zangrando, S. Andreozzi, V. Ciaschini, C. Di Giusto, F. Giacomini, V. Medici, E. Ronchieri, V. Venturi, G. Avellino, S. Beco, A. Maraschini, F. Pacini, A. Guarise, G. Patania. Practical approaches to Grid workload and resource management in the EGEE project.
In CHEP'04: Proceedings of the Conference on Computing in High Energy and Nuclear Physics, pages 899-902, 2004
Authors :
P. Andreetto, V. Borgia, A. Dorigo, A. Gianelle, M. Mordacchini, M. Sgaravatto, L. Zangrando, S. Andreozzi, V. Ciaschini, C. Di Giusto, F. Giacomini, V. Medici, E. Ronchieri, V. Venturi, G. Avellino, S. Beco, A. Maraschini, F. Pacini, A. Guarise, G. Patania
Title : Practical approaches to Grid workload and resource management in the EGEE project
Reference :
In CHEP'04: Proceedings of the Conference on Computing in High Energy and Nuclear Physics, pages 899-902, 2004
Type : WORKSHOPS AND POSTERS
Year : 2004