

Author  Title/Abstract 

Neil D. Jones  The Expressive Power of HigherOrder Types or, Life without CONS 
This talk uses complexity theory to prove expressivity results
about several aspects of functional programming languages.
An expressivity question: can higherorder programs (with functions as parameters) compute more than firstorder functional programs? The answer is NO: both classes are Turing complete, i.e., both can compute all partially recursive functions. A reason is that higherorder values may be simulated in a firstorder language by using the list constructor ``cons'' to build function closures. Rather than give up, we study smaller programming languages that are less than Turing complete. Examples for ``consfree'' programs:

Author(s)  Title/Abstract 

Jos C.M. Baeten  Embedding Untimed into Timed Process Algebra; the Case for Explicit Termination 
In ACPstyle process algebra, the interpretation of a constant
atomic action combines action execution with termination. In a
setting with timing, different forms of termination can be
distinguished: some time termination, termination before the
next clock tick, urgent termination, being terminated. In a
setting with the silent action tau, we also have silent
termination.
This leads to problems with the interpretation of atomic actions in timed theories that involve some form of the empty process or some form of the silent action. Reflection on these problems lead to a redesign of basic process algebra, where action execution and termination are separated. Instead of actions as constants, we have action prefix operators. Sequential composition remains a basic operator, and thus we have two basic constants for termination, delta for unsuccessful termination (deadlock) and epsilon for successful termination (skip). We can recover standard process algebras as subtheories of the new theory. The new approach has definite advantages over the standard approach.  
Martin Berger Kohei Honda  The TwoPhase Commitment Protocol in an Extended piCalculus 
This paper examines how the picalculus can be extended simply and consistently to represent basic elements of distributed systems. The expressiveness of the picalculus for encoding various computational structures is wellknown; for describing computation in distributed systems, however, the calculus often needs be extended to be able to cleanly model phenomena inherent in distributed systems. We demonstrate three such extensions (message loss, timers and process failure/recovery) and examine their descriptive power, taking the Two Phase Commit Protocol (2PCP), a basic instance of an atomic commitment protocol, as a testbed. Systematic extensions of the picalculus are used for representing the 2PCP under various failure assumptions, as well as for reasoning about its essential properties. Observations on relative expressiveness in comparison with the original calculus are also discussed.  
Flavio Corradini Dino Di Cola  A Study on the Interplay between Syntax and Semantics of Timed Processes 
We show how the expressive power of a language for the description of timed processes strongly affects the discriminating power of urgent and patient actions. In a sense this paper studies the interplay between syntax and semantics of timecritical systems.  
Shoham Shamir Orna Kupferman Eli Shamir  BranchingDepth Hierarchies in Temporal Logic 
We study the distinguishing and expressive power of branching temporal
logics with bounded nesting depth of path quantifiers. We define the
fragments CTL*_{i} and CTL_{i} of CTL* and CTL, where at most i nestings
of path quantifiers are allowed. We show that for all i >= 1, the
logic CTL*_{i+1} has more distinguishing and expressive power than
CTL*_{i}; thus the branchingdepth hierarchy is strict.
We describe equivalence relations H_{i} that capture CTL*_{i}: two states in a Kripke structure are H_{i}equivalent iff they agree on exactly all CTL*_{i} formulas. While H_{1} corresponds to trace equivalence, the limit of the sequence H_{1}, H_{2},... is Milner's bisimulation. These results are not surprising, but they give rise to several interesting observations and problems. In particular, while CTL* and CTL have the same distinguishing power, this is not the case for CTL*_{i} and CTL_{i}. We define the branching depth of a structure as the minimal index i for which H_{i+1}=H_{i}. The branching depth indicates on the possibility of using bisimulation instead of trace equivalence (and similarly for simulation and trace containment). We show that the problem of finding the branching depth is PSPACEcomplete.  
Jiri Srba  Complexity of Weak Bisimilarity and Regularity for BPA and BPP 
It is an open problem whether weak bisimilarity is decidable for
Basic Process Algebra (BPA) and Basic Parallel Processes (BPP).
A PSPACE lower bound for BPA and NP lower bound for BPP have been
demonstrated by Stribrna. Mayr achieved recently a result, saying
that weak bisimilarity for BPP is PI_{2}^{P}hard. We improve this
lower bound to PSPACE, moreover for the restricted class of normed BPP.
Weak regularity (finiteness) of BPA and BPP is not known to be decidable either. In the case of BPP there is a PI_{2}^{P}hardness result by Mayr, which we improve to PSPACE. No lower bound has previously been established for BPA. We demonstrate DPhardness, which in particular implies both NP and coNPhardness. In each of the bisimulation/regularity problems we consider also the classes of normed processes.  
Pascal Zimmer  On the Expressiveness of Pure Mobile Ambients 
We consider the Pure Ambient Calculus, which is Cardelli and Gordon's Ambient Calculus restricted to its mobility primitives, and we focus on its expressive power. Since it has no form of communication or substitution, we show how these notions can be simulated by mobility and modifications in the hierarchical structure of ambients. As an example, we give an encoding of the synchronous picalculus into pure ambients and we state an operational correspondence result. In order to simplify the proof and give an intuitive understanding of the encoding, we design an intermediate language: the PiCalculus with Explicit Substitutions and Channels, which is a syntactic extension of the picalculus with a specific operational semantics. 
Author(s)  Title/Abstract 

Oltea Mihaela Herescu Catuscia Palamidessi  Encoding pi in asynchronous pi via randomization (short abstract) 
We consider the problem of encoding the picalculus into the asynchronous picalculus via a uniform translation while preserving a reasonable semantics. Although it has been shown that this is not possible with an exact encoding, we suggest a randomized approach using a probabilistic extension of the asynchronous picalculus. We can show that our solution is correct with probability $1$ wrt a notion of testing semantics extended to probabilistic processes, under any weakly fair scheduler.  
Uwe Nestmann António Ravara  What's TyCO, After All? (short abstract) 
uniform TyCO \equiv! pi_{a} with flat variants uniform TyCO \approx"!" pi_{a} with nested variants nonuniform TyCO >!? pi_{a} with nested variants 
© Björn Victor Last modified: Thu, 27Jul2000 23:01 MEST 