Corrado Priami

TCS Journal 2010 Journal Article

On the computational power of BlenX

• Alessandro Romanel
• Corrado Priami

We present some decidability and undecidability results for subsets of the BlenX Language, a process-calculi-based programming language developed for modelling biological processes. We show that for a core subset of the language (which considers only communication primitives) termination is decidable. Moreover, we prove that by adding either global priorities or events to this core language, we obtain Turing equivalent languages. The proof is through encodings of Random Access Machines (RAMs), a well-known Turing equivalent formalism, into our subsets of BlenX. All the encodings are shown to be correct.

TCS Journal 2008 Journal Article

Preface

• Corrado Priami

TCS Journal 2004 Journal Article

Preface

• Corrado Priami

TCS Journal 2002 Journal Article

A causal semantics for CCS via rewriting logic

• Pierpaolo Degano
• Fabio Gadducci
• Corrado Priami

We consider two operational semantics for CCS defined in the literature: the first exploits proved transition systems (PTS) and the second rewriting logic (RL). We show that the interleaving interpretation of both semantics agree, in that they define the same transitions and exhibit the same non-deterministic structure. In addition, we study causality in CCS computations. We recall its treatment via PTS, exhibiting the notion of causality presented in the literature, and we show how to recast it in the RL semantics via suitable axioms. Also in this case, the two semantics agree.

I&C Journal 2002 Journal Article

Language-based Performance Prediction for Distributed and Mobile Systems

• Corrado Priami

We present a framework for performance prediction of distributed and mobile systems. We rely on process calculi and their structural operational semantics. The dynamic behaviour is described through transition systems whose transitions are labelled by encodings of their proofs that we then map into stochastic processes. We enhance related works by allowing general continuous distributions resorting to a notion of enabling between transitions. We also discuss how the number of resources available affects the overall model. Finally, we introduce a notion of bisimulation that takes stochastic information into account and prove it to be a congruence. When only exponential distributions are of interest our equivalence induces a lumpable partition on the underlying Markov process.

TCS Journal 2002 Journal Article

Primitives for authentication in process algebras

• Chiara Bodei
• Pierpaolo Degano
• Riccardo Focardi
• Corrado Priami

We extend the π-calculus and the spi-calculus with two primitives that guarantee authentication. They enable us to abstract from various implementations/specifications of authentication, and to obtain idealized protocols which are “secure by construction”. The main underlying idea, originally proposed in Focardi (Proc. Sixth Italian Conf. on Theoretical Computer Science, November 1998) for entity authentication, is to use the locations of processes in order to check who is sending a message (authentication of a party) and who originated a message (message authentication). The theory of local names, developed in Bodei et al. (Theoret. Comput. Sci. 253(2) (2001) 155) for the π-calculus, gives us almost for free both the partner authentication and the message authentication primitives.

TCS Journal 2001 Journal Article

Names of the π-calculus agents handled locally

• Chiara Bodei
• Pierpaolo Degano
• Corrado Priami

We address the problem of handling names in concurrent and distributed systems made up of mobile processes. We equip processes with local environments. Our structural operational semantics handles these environments so that captures of names are never possible. Our semantics includes the specification of a distributed name manager that conservatively extends standard operational semantics. Bisimulation-based equivalences can be checked on our transition systems. They yield the same equivalence relations as those based on standard interleaving semantics. Finally, we show that our development scales up smoothly to higher-order calculi.

TCS Journal 1999 Journal Article

Non-interleaving semantics for mobile processes

• Pierpaolo Degano
• Corrado Priami

This paper studies causality in the π-calculus. Our notion of causality combines the dependencies given by the syntactic structure of processes with those originated by passing names. Our studies show that two transitions not causally related may however occur in a fixed ordering in any computation, i. e. , the π-calculus may implicitly express a precedence between actions. The same partial order of transitions is associated with all the computations that are obtained by shuffling transitions that are concurrent (i. e. related neither by causality nor by precedence). Other non-interleaving semantics are investigated and compared. The presentation takes advantage of a parametric definition of process behaviour given in SOS style that permits us to take almost for free the interleaving theory and tools. Finally, we extend our approach to higher-order π-calculus, enriched with a spawn operation.

MFCS Conference 1994 Conference Paper

Read-Write Causality

• Corrado Priami
• Daniel Yankelevich

Abstract We introduce a new kind of causality between events of a distributed system that takes the nature of the events into account. More precisely, we distinguish between read (receive) and write (send) operations, yielding a relation called read-write causality. We clarify the intuition of our causality relation through examples, and we compare it with classical models of causality. Also, we show that it is better suited than the classical relations for debugging of formal specifications.