Computer Science has witnessed the emergence of a plethora of different logics, models and paradigms for the description of computation. Yet, the classic Church–Turing thesis may be seen as indicating that all general models of computation are equivalent. Alan Perlis referred to this as the ‘Turing tarpit’, and argued that some of the most crucial distinctions in computing methodology, such as sequential versus parallel, deterministic versus non-deterministic, local versus distributed disappear if all one sees in computation is pure symbol pushing. How can we express formally the difference between these models of computation?

We review the conceptual development of (true) concurrency and branching time starting from Petri nets and proceeding via Mazurkiewicz traces, pomsets, bisimulation, and event structures up to higher dimensional automata (HDAs), whose acyclic case may be identified with triadic event structures and triadic Chu spaces. Acyclic HDAs may be understood as extending the two truth values of Boolean logic with a third value $\T$ expressing transition. We prove the necessity of such a third value under mild assumptions about the nature of observable events, and show that the expansion of any complete Boolean basis $L$ to $L_{\T}$ with a third literal $\that a$ expressing $a=\T$ forms an expressively complete basis for the representation of acyclic HDAs. The main contribution is a new value $\cancel$ of cancellation, which is a sibling of $\T$, serving to distinguish $a(b+c)$ from $ab+ac$ while simplifying the extensional definitions of termination $\tick\A$ and sequence $\A\B$. We show that every HDAX (acyclic HDA with $\cancel$) is representable in the expansion of $L_{\T}$ to $L_{\T\cancel}$ with a fourth literal $\can a$ expressing $a=\cancel$.

Connections between the sequentiality/concurrency distinction and the semantics of proofs are investigated, with particular reference to games and Linear Logic.

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 were demonstrated by Stribrna. Mayr recently achieved a result, saying that weak bisimilarity for BPP is $\Pi_2^P$-hard. We improve this lower bound to PSPACE, and, moreover, prove this result for the restricted class of normed BPP. It is also not known whether weak regularity (finiteness) of BPA and BPP is decidable. 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 DP-hardness, which, in particular, implies both NP and co-NP-hardness. In each of the bisimulation/regularity problems we also consider the classes of normed processes. Finally, we show how the technique for proving co-NP lower bound for weak bisimilarity of BPA can be applied to strong bisimilarity of BPP.

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, having 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 led 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 ACP-style process algebras as subtheories of the new theory. The new approach has definite advantages over the standard approach. The paper contributes to ongoing work on relationships between algebras with different timing features.

In this paper 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, it studies the interplay between syntax and semantics of time-critical systems.