Author name cluster

Roberto M. Amadio

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

8 papers

2 author rows

I&C Journal 2007 Journal Article

A synchronous π-calculus

Roberto M. Amadio

The SL synchronous programming model is a relaxation of the Esterel synchronous model where the reaction to the absence of a signal within an instant can only happen at the next instant. In previous work, we have revisited the SL synchronous programming model. In particular, we have discussed an alternative design of the model, introduced a CPS translation to a tail recursive form, and proposed a notion of bisimulation equivalence. In the present work, we extend the tail recursive model with first-order data types obtaining a non-deterministic synchronous model whose complexity is comparable to the one of the π-calculus. We show that our approach to bisimulation equivalence can cope with this extension and in particular that labelled bisimulation can be characterised as a contextual bisimulation.

Details DOI

TCS Journal 2006 Journal Article

Resource control for synchronous cooperative threads

Roberto M. Amadio
Silvano Dal Zilio

We develop new methods to statically bound the resources needed for the execution of systems of concurrent, interactive threads. Our study is concerned with a synchronous model of interaction based on cooperative threads whose execution proceeds in synchronous rounds called instants. Our contribution is a system of compositional static analyses to guarantee that each instant terminates and to bound the size of the values computed by the system as a function of the size of its parameters at the beginning of the instant. Our method generalises an approach designed for first-order functional languages that relies on a combination of standard termination techniques for term rewriting systems and an analysis of the size of the computed values based on the notion of quasi-interpretation. We show that these two methods can be combined to obtain an explicit polynomial bound on the resources needed for the execution of the system during an instant. As a second contribution, we introduce a virtual machine and a related bytecode thus producing a precise description of the resources needed for the execution of a system. In this context, we present a suitable control flow analysis that allows to formulate the static analyses for resource control at bytecode level.

Details DOI

CSL Conference 2004 Conference Paper

A Functional Scenario for Bytecode Verification of Resource Bounds

Roberto M. Amadio
Solange Coupet-Grimal
Silvano Dal-Zilio
Line Jakubiec

Abstract We consider a scenario where (functional) programs in pre-compiled form are exchanged among untrusted parties. Our contribution is a system of annotations for the code that can be verified at load time so as to ensure bounds on the time and space resources required for its execution, as well as to guarantee the usual integrity properties. Specifically, we define a simple stack machine for a first-order functional language and show how to perform type, size, and termination verifications at the level of the bytecode of the machine. In particular, we show that a combination of size verification based on quasi-interpretations and of termination verification based on lexicographic path orders leads to an explicit bound on the space required for the execution.

Details

TCS Journal 2003 Journal Article

On the symbolic reduction of processes with cryptographic functions

Roberto M. Amadio
Denis Lugiez
Vincent Vanackère

We study the reachability problem for cryptographic protocols represented as processes relying on perfect cryptographic functions. We introduce a symbolic reduction system that can handle hashing functions, symmetric keys, and public keys. Desirable properties such as secrecy or authenticity are specified by inserting logical assertions in the processes. We show that the symbolic reduction system provides a flexible decision procedure for finite processes and a reference for sound implementations. The symbolic reduction system can be regarded as a variant of syntactic unification which is compatible with certain set-membership constraints. For a significant fragment of our formalism, we argue that a dag implementation of the symbolic reduction system leads to an algorithm running in NPTIME thus matching the lower bound of the problem. In the case of iterated or finite control processes, we show that the problem is undecidable in general and in PTIME for a subclass of iterated processes that do not rely on pairing. Our technique is based on rational transductions of regular languages and it applies to a class of processes containing the ping-pong protocols presented in Dolev et al. (Inform. Comput. (55) (1982) 57).

Details DOI

TCS Journal 2000 Journal Article

On modelling mobility

Roberto M. Amadio

We present a model of distributed computation which is based on a fragment of the π-calculus relying on asynchronous point-to-point communication. We enrich the model with the following features: the explicit distribution of processes to locations, the routing of messages, the mobility of processes, and the failure of locations and their detection. Our contributions are two folds. At the specification level, we give a synthetic and flexible formalization of the features mentioned above. At the verification level, we provide original methods to reason about the bisimilarity of processes.

Details DOI

TCS Journal 1998 Journal Article

On bisimulations for the asynchronous π-calculus

Roberto M. Amadio
Ilaria Castellani
Davide Sangiorgi

The asynchronous π-calculus is a variant of the π-calculus where message emission is non-blocking. Honda and Tokoro have studied a semantics for this calculus based on bisimulation. Their bisimulation relies on a modified transition system where, at any moment, a process can perform any input action. In this paper we propose a new notion of bisimulation for the asynchronous π-calculus, defined on top of the standard labelled transition system. We give several characterizations of this equivalence including one in terms of Honda and Tokoro's bisimulation, and one in terms of barbed equivalence. We show that this bisimulation is preserved by name substitutions, hence by input prefix. Finally, we give a complete axiomatization of the (strong) bisimulation for finite terms.

Details DOI

MFCS Conference 1993 Conference Paper

On the Adequacy of Per Models

Roberto M. Amadio

Abstract We consider a fixed point extension of the second order lambda calculus equipped with a call by value evaluation mechanism. We interpret the language in a partial cartesian closed category of “directed complete” partial equivalence relations (pers) over a domain theoretic model of a type-free, call-by-value, lambda calculus. Our main result is that the notions of “syntactic” and “semantic” convergence coincide.

Details

I&C Journal 1991 Journal Article

Recursion over realizability structures

Roberto M. Amadio

Realizability structures play a major role in the metamathematics of intuitionistic systems and they are a basic tool in the extraction of the computational content of constructive proofs. Besides their rich categorical structure and effectiveness properties provide a privileged mathematical setting for the semantics of data types of programming languages. In this paper we emphasize the modelling of recursive definitions of programs and types. A realizability model for a language including Girard's system F and an operator of recursion on types is given and some of its local properties are studied.

Details DOI