A declarative approach for first-order built-in's of Prolog

We provide here a framework for studying Prolog programs with various built-in's that include arithmetic operations, and such metalogical relations likevar andground. To this end we propose a new, declarative semantics and prove completeness of the Prolog computation mechanism w.r.t. this semantics. We also show that this semantics is fully abstract in an appropriate sense. Finally, we provide a method for proving termination of Prolog programs with built-in's which uses this semantics. The method is shown to be modular and is illustrated by proving termination of a number of programs including the unify program of Sterling and Shapiro [17].     

Separation of synchronous and asynchronous communication via testing

One of the early results concerning the asynchronous π$\pi$-calculus which significantly contributed to its popularity is the capability of encoding the output prefix of the (choiceless) π$\pi$-calculus in a natural and elegant way. Encodings of this kind were proposed by Honda and Tokoro, by Nestmann and (independently) by Boudol. We investigate whether the above encodings preserve De Nicola and Hennessy’s testing semantics. In this sense, it turns out that, under some general conditions, no encoding of the output prefix is able to preserve the must testing. This negative result is due to (a) the non-atomicity of the sequences of steps which are necessary in the asynchronous π$\pi$-calculus to mimic synchronous communication, and (b) testing semantics’ sensitivity to divergence.     

Expressiveness of Probabilistic π-calculus

In this work we propose a probabilistic extension of the π-calculus. The main novelty is a probabilistic mixed choice operator, that is, a choice construct with a probability distribution on the branches, and where input and output actions can both occur as guards. We develop the operational semantics of this calculus, and then we investigate its expressiveness. In particular, we compare it with the sublanguage with the two separate choices, where input and output guards are not allowed together in the same choice construct. Our main result is that the separate choices can encode the mixed one. Further, we show that input-guarded choice can encode output-guarded choice and viceversa. In contrast, we conjecture that neither of them can encode the pair of the two separate choices.     

A framework for analyzing probabilistic protocols and its application to the Partial Secrets Exchange

We propose a probabilistic variant of the pi-calculus as a framework to specify randomized security protocols and their intended properties. In order to express and verify the correctness of the protocols, we develop a probabilistic version of the testing semantics. We then illustrate these concepts on an extended example: the Partial Secret Exchange, a protocol which uses a randomized primitive, the Oblivious Transfer, to achieve fairness of information exchange between two parties.     

Preface: Volume 16, Issue 2

This volume contains the Proceedings of the fifth EXPRESS workshop. The workshop was held in Nice, France, on 7 September 1998, as a satellite event to CONCUR '98.The EXPRESS workshops aim at bringing together researchers interested in the relations between various formal systems, particularly in the field of Concurrency. More specifically, they focus on the comparison between programming concepts (such as concurrent, functional, imperative, logic and object-oriented programming) and between mathematical models of computation (such as process algebras, Petri nets, event structures, modal logics, rewrite systems etc.) on the basis of their relative expressive power.These workshops were originally held as meetings of the HCM project EXPRESS, which has been active with the same focus from January 1994 till December 1997. The first three workshops were held respectively in Amsterdam (1994, chaired by Frits Vaandrager), Tarquinia (1995, chaired by Rocco de Nicola), and Dagstuhl (1996, chaired by Ursula Goltz, Frits Vaandrager and Rocco de Nicola). The fourth workshop, which took place in Santa Margherita Ligure in 1997 and was co-chaired by Catuscia Palamidessi and Joachim Parrow, was organized as a conference with a call for papers and a significant attendance from outside the project. The fifth workshop, EXPRESS '98, was again organised as a (one day) conference, and was also meant as an occasion to discuss on the inheritance of the Express project and possible directions of future research. We had 17 submissions, out of which we selected 7 for inclusion in these proceedings (41%). Additionally, this collection contains the contribution of the two invited speakers, Matthew Hennessy (University of Sussex, UK) and P.S. Thiagarajan (SPIC Mathematical Institute, IN).We would like to thank the authors of the submitted papers, the invited speakers, and the members of the program committee for their contribution to both the meeting and this volume. We also would like to thank INRIA for their help with the local organization, and Michael Mislove for his help with the editing of the proceedings.

EXPRESS '98 Programme Committee
Ilaria Castellani (co-chair, INRIA)	Catuscia Palamidessi (co-chair, PSU)
Luca Aceto (Aalborg Univ.)	Roberto Amadio (Univ. Marseille)
Eike Best (Oldenburg Univ.)	Steve Brookes (CMU)
Philippe Darondeau (INRIA)	Rocco De Nicola (Univ. Firenze)
Jan Willem Klop (CWI)	Patrick Lincoln (SRI)
Frits Vaandrager (Nijmegen Univ.)	Glynn Winskel (Aarhus Univ.)

Full-size table

17 October 1998, Ilaria Castellani and Catuscia Palamidessi     

On the Expressive Power of Temporal Concurrent Constraint Programming Languages: (invited talk)

The tcc paradigm is a formalism for timed concurrent constraint programming. Several tcc languages differing in their way of expressing infinite behavior have been proposed in the literature. In this work we study the expressive power of some of these languages. In particular, we show that: (1) recursive procedures with parameters can be encoded into parameterless recursive procedures with dynamic scoping, and viceversa. (2) replication can be encoded into parameterless recursive procedures with static scoping, and viceversa. (3) the languages from (1) are strictly more expressive than the languages from (2). Furthermore, we show that behavioral equivalence is undecidable for the languages from (1), but decidable for the languages from (2). The undecidability result holds even if the process variables take values from a fixed finite domain.(Joint work with Mogens Nielsen and Frank D. Valencia)     

A Congruence Format for Name-passing Calculi

We define and use a SOS-based framework to specify the transition systems of calculi with name-passing properties. This setting uses proof-theoretic tools to take care of some of the difficulties specific to name-binding and make them easier to handle in proofs. The contribution of this paper is the presentation of a format that ensures that open bisimilarity is a congruence for calculi specified within this framework, extending the well-known tyft/tyxt format to the case of name-binding and name-passing. We apply this result to the π-calculus in both its late and early semantics.     

Making random choices invisible to the scheduler

When dealing with process calculi and automata which express both nondeterministic and probabilistic behavior, it is customary to introduce the notion of scheduler to resolve the nondeterminism. It has been observed that for certain applications, notably those in security, the scheduler needs to be restricted so not to reveal the outcome of the protocol’s random choices, or otherwise the model of adversary would be too strong even for “obviously correct” protocols. We propose a process-algebraic framework in which the control on the scheduler can be specified in syntactic terms, and we show how to apply it to solve the problem mentioned above. We also consider the definition of (probabilistic) may and must preorders, and we show that they are precongruences with respect to the restricted schedulers. Furthermore, we show that all the operators of the language, except replication, distribute over probabilistic summation, which is a useful property for verification.     

Separation of Synchronous and Asynchronous Communication Via Testing

One of the early results about the asynchronous π-calculus which significantly contributed to its popularity is the capability of encoding the output prefix of the (choiceless) π-calculus in a natural and elegant way. Encodings of this kind were proposed by Honda and Tokoro, by Nestmann and (independently) by Boudol. We investigate whether the above encodings preserve De Nicola and Hennessy's testing semantics. In this sense, it turns out that, under some general conditions, no encoding of output prefix is able to preserve the must testing. This negative result is due to (a) the non atomicity of the sequences of steps which are necessary in the asynchronous π-calculus to mimic synchronous communication, and (b) testing semantics's sensitivity to divergence.