EXPRESS'00 logo
7th International Workshop on
Expressiveness in Concurrency
August 21, 2000
Pennsylvania State University, USA

Abstract of invited talk

Author Title/Abstract
Neil D. Jones The Expressive Power of Higher-Order 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 higher-order programs (with functions as parameters) compute more than first-order functional programs? The answer is NO: both classes are Turing complete, i.e., both can compute all partially recursive functions. A reason is that higher-order values may be simulated in a first-order 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 ``cons-free'' programs:

  • recursion removal is possible if and only if PTIME = LOGSPACE.
  • Second-order programs are more powerful than first-order, since
    • function f: list Bool -> Bool is computable by a cons-free first-order program if and only if f is in PTIME, whereas
    • f is computable by a cons-free second-order program if and only if f is in EXPTIME.
Exact characterizations will be given for those problems of type list Bool -> Bool solvable by programs with several combinations of
  • operations on data: presence or absence of constructors;
  • order of data values: 0,1, or higher; and
  • control structures: general recursion, tail recursion, primitive recursion.

Abstracts of accepted submissions

These are the abstracts of the submissions accepted to EXPRESS'00.

Full papers

The full papers will be published in the proceedings.
Author(s) Title/Abstract
Jos C.M. Baeten Embedding Untimed into Timed Process Algebra; the Case for Explicit Termination
In ACP-style 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 re-design 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 Two-Phase Commitment Protocol in an Extended pi-Calculus
This paper examines how the pi-calculus can be extended simply and consistently to represent basic elements of distributed systems. The expressiveness of the pi-calculus for encoding various computational structures is well-known; 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 pi-calculus 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 time-critical systems.
Shoham Shamir
Orna Kupferman
Eli Shamir
Branching-Depth 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 CTLi 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 branching-depth hierarchy is strict.

We describe equivalence relations Hi that capture CTL*i: two states in a Kripke structure are Hi-equivalent iff they agree on exactly all CTL*i formulas. While H1 corresponds to trace equivalence, the limit of the sequence H1, H2,... 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 CTLi. We define the branching depth of a structure as the minimal index i for which Hi+1=Hi. 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 PSPACE-complete.

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 PI2P-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 PI2P-hardness result by Mayr, which we improve to PSPACE. No lower bound has previously been established for BPA. We demonstrate DP-hardness, which in particular implies both NP and coNP-hardness.

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 pi-calculus 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 Pi-Calculus with Explicit Substitutions and Channels, which is a syntactic extension of the pi-calculus with a specific operational semantics.

Short abstracts

The short abstracts will not be published in the proceedings.
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 pi-calculus into the asynchronous pi-calculus 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 pi-calculus. 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! pia with flat variants
uniform TyCO \approx"!" pia with nested variants
non-uniform TyCO >!? pia with nested variants

© Björn Victor
Last modified: Thu, 27-Jul-2000 23:01 MEST
[Valid HTML 4.01!]