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.

• 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.

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.

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₁ corresponds to trace equivalence, the limit of the sequence H₁, H₂,... 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 PSPACE-complete.

Weak regularity (finiteness) of BPA and BPP is not known to be decidable either. In the case of BPP there is a PI₂^P-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.