Abstracts of presentations

Invited speakers

Prakash Panangaden, McGill University, CA
Concurrent Constraint Programming as a Linear Realizability Algebra

Abstract: Many process calculi embodying mobility are known to encode the lambda-calculus. This of course began with Robin Milner's famous paper "Functions as Processes" and was continued in the investigations of many others, notably Sangiorgi. The Concurrent Constraint Programming paradigm (ccp henceforth) emerged from the logic programming community as an interesting process calculus embodying features that look like mobility in some sense but in other senses look very different. Interestingly ccp can encode the lambda-calculus. The underlying reason why ccp can encode lambda-calculus is that ccp can encode a linear realizability algebra - an algebraic presentation of linear logic proof nets. With the latter one can express lambda-calculus. Our presentation of the ccp encoding of lambda-calculus factors through the linear realizability algebra. In fact pi-calculus also forms a linear realizability algebra and an encoding of lambda-calculus can be factored through this - as shown by Bellin and Scott. I will define linear realizability algebra, show how ccp forms an linear realizability algebra, and show the encoding of lambda-calculus that results. I will also mention some related expressiveness questions that arise from this work.

Roberto Amadio, Université de Provence, FR
Two Applications of the pi-Calculus

Abstract: Theoretical work on calculi of mobile processes has been an active area of research in the last seven years. The related literature can be classified in three main and intertwined threads of research: the study of the expressive power of the model, the introduction of typing rules constraining the behaviour of processes, and the characterization of the related observational equivalences. In this talk, we will present two concrete applications of some of the ideas and techniques developed so far.

The first application relates to the design of a programming model of distributed and mobile computation. Relying on a distributed version of the asynchonous pi-calculus, we show that a simple type system ensures `receptiveness', i.e., that any message will find an appropriate receiver. We will argue that this property can be obtained without loss of expressive power.

The second application relates to the modelling and verification of cryptographic protocols relying on a simplified pi-calculus equipped with a `cryptographic table'. The latter is a data structures representing relationships among names. Following classical approaches, we formulate the verification task as a reachability problem and prove its decidability assuming finite principals and bounds on the sorts of the messages synthesized by the attacker.

This talk is partially based on joint work with G. Boudol, C. Lhoussaine, and S. Prasad.

Accepted submissions

Rom Langerak, University of Twente, NL:
Deriving a Graph Grammar from a Complete Finite Prefix of an Unfolding: Abstract: The starting point of this paper is McMillan's complete finite prefix of an unfolding that has been obtained from a Petri net or a process algebra expression. The paper addresses the question of how to obtain the (possibly infinite) system behaviour from the finite prefix. An algorithm is presented to derive from the prefix a graph grammar that can be used to construct the unfolding. It is shown how to generate event sequences from the graph grammar which is important for constructing an interactive simulator. Finally it is indicated how the graph grammar yields a transition system that can be used for model checking and test derivation.
Anna Ingolfsdottir, BRICS, DK and Rosario Pugliese, Università di Firenze, IT:
Towards Verified Lazy Implementation of Concurrent Value-Passing Languages (abstract): Abstract: The behaviour of concurrent processes with value-passing is typically described by means of labelled transition systems. These semantic descriptions are, in general, on a very abstract level. Implementation details, such as how the values are actually transmitted from one process to another, are not considered. In this paper we will give a more concrete semantic model, based on the ``lazy''-approach, for (the late-version of) the standard CCS where the exchange of data takes place by means of synchronized use of a common store. We also prove the ``correctness'' of this ``implementation'', i.e.~we prove that this new semantics corresponds to the standard one in some formal but intuitive sense.
Heike Wehrheim, Universität Oldenburg, DE:
Partial order reductions for failures refinement: Abstract: Partial order reduction techniques have been introduced to avoid the problem of state space explosion arising in the verification of concurrent systems. The overall idea is to exploit only some of a large number of interleavings of concurrent transitions while retaining the possibility of checking certain properties. In this paper we investigate how much structure of a system has to be preserved for checking failures refinement. In contrast to previously proposed techniques we focus here on exploiting independencies between visible actions. We show that just one condition in addition to the usual linear time reduction conditions is needed to preserve the possibility of checking failures refinement. This additional condition is compared with the conditions used in partial order techniques for bisimulation checking.
Massimo Merro, INRIA, FR:
On Equators in Asynchronous Name-passing Calculi without Matching: Abstract: We give a labelled characterization of barbed congruence in asynchronous pi-calculus, which unlike previous characterizations, does not use the matching construct. In absence of matching, the observer cannot directly distinguish two names. In asynchronous pi-calculus, the fact that two names are indistinguishable can be modelled by means of Honda and Yoshida's notion of equator. So, our labelled characterization is based on such notion. As an application of our theory we provide a fully abstract encoding w.r.t. barbed congruence of external mobility (communication of free names) in terms of internal mobility (communication of private names).
Simone Tini, Università di Pisa, IT:
On The Expressiveness of Timed Concurrent Constraint Programming: Abstract: We consider the synchronous paradigms Timed Concurrent Constraint (TCC) and Default Timed Concurrent Constraint (TDCC), and we investigate their expressiveness by relating the expressive power of these paradigms with the expressive power of other synchronous languages. We define a TCC language, TCC_Argos, and we prove that it encodes Argos. The encoding is compositional w.r.to the structure of Argos programs and is linear w.r.to their size. We prove also that the ``strong abortion'' mechanism, which is not offered by Argos but is offered by other state oriented synchronous language (Esterel), can be encoded in TCC_Argos. Then we define another TCC language, TCC_Lustre, and we prove that it encodes the subset of Lustre restricted to finite value types. This encoding is compositional w.r.to the structure of Lustre programs and is linear w.r.to their size and the size of types. Finally, we conjecture that TDCC (and TCC, which is less powerful) cannot embed the full Lustre.
Lucian Wischik and Philippa Gardner, Cambridge University, UK:
Symmetric Action Calculi (abstract): Abstract: We introduce a novel form of action calculi, known as the symmetric action calculi. These have operators for names, co-names and restriction. Conventional action calculi meanwhile combine the last two into a single abstraction operator. In this respect, the move from the conventional action calculi to the symmetric mirrors that from the pi-calculus to the Fusion calculus. However, fusions 'x=y' in symmetric action calculi are part of the structural congruence rather than the transition system. We note that the reflexion operator in the reflexive action calculi is merely a special case of this sort of fusion and can be defined more conveniently as such; so too with the connection operator in Yoshida's process graphs.
Sibylle Fröschle, LFCS, UK:
Decidability of Plain and Hereditary History-Preserving Bisimilarity for BPP: Abstract: In this paper we investigate the decidability of history-preserving bisimilarity (HPB) and hereditary history-preserving bisimilarity for basic parallel processes (BPP). We find that both notions are decidable for this class of in finite systems, and present tableau-based decision procedures. The first result is not new but has already been established via the decidability of causal bisimilarity, a notion that is equivalent to history-preserving bisimilarity. However, our decision procedure provides an independent and direct proof. The decidability of hereditary HPB is a new result. This result is especially interesting, since it is now a long-standing open problem whether hereditary HPB is decidable for finite-state systems.
Gabriel Juhas, TU Berlin, DE:
Petri nets with generalised algebra: a comparison: Abstract: In the last decade we can see a substantial effort to develop an abstract and uniform constructions for Petri nets. Most of such abstractions are based on algebraic characterizations of Petri nets. They work mostly over commutative monoids and their various subclasses, namely cancellative commutative monoids or cones of Abelian groups. In the paper we study relationships between Petri nets with generalised underlying algebra. More precisely, we study Petri nets over commutative monoids, cancellative commutative monoids, cones of Abelian groups, and fully ordered cones of Abelian groups. As the main result, we show that classes of reachability graphs of Petri nets over cancellative commutative monoids and cones of Abelian groups coincide (up to isomorphism). In other words, partial order on used cancellative commutative monoid plays no role in expressive power of Petri nets. However, as shows the fact that the class of reachability graphs of nets over fully ordered cones is a proper subclass of the class of reachability graphs of nets over cancellative commutative monoids, the total order on used monoids plays an important role in expressive power of Petri nets.
Mario Bravetti and Roberto Gorrieri, Università di Bologna, IT:
Deciding and Axiomatizing ST Bisimulation for a Process Algebra with Recursion and Action Refinement: Abstract: Due to the complex nature of bisimulation equivalences which express some form of history dependence, it turned out to be very problematic to decide and, especially, axiomatize them for non trivial class of systems. Here we introduce the idea of ``compositional level-wise renaming'' which gives rise to the new possibility of axiomatizing the history dependent bisimulations with slight modifications to the machinery for standard bisimulation. We propose two techniques, which are based on this idea, for expressing the ST semantics for terms of a process algebra with recursion. The first technique, which is more intuitive, is based on dynamic names and allows to decide and axiomatize weak ST bisimulation for all processes that possess a finite state interleaving semantics. The second technique, which is based on pointers, allows to preserve the possibility of deciding and axiomatizing weak ST bisimulation when an action refinement operator $P[a \leadsto Q]$ is considered, i.e. $P[a \leadsto Q]$ is finite state whenever $P$ and $Q$ are finite state.

Last modified: Wed, 28-Jul-1999 13:07 MEST