|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:
|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
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 |
|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|
|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.|
| Oltea Mihaela Herescu |
|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 |
|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|