Reasoning About Concurrent Computational Systems

Allan Cheng

August 1996

Abstract:

This thesis consists of three parts. The first presents contributions in the field of verification of finite state concurrent systems, the second presents contributions in the field of behavioural reasoning about concurrent systems based on the notions of behavioural preorders and behavioural equivalences, and, finally, the third presents contributions in the field of set constraints.

In the first part, we study the computational complexity of several standard verification problems for 1-safe Petri nets and some of its subclasses. Our results provide the first systematic study of the computational complexity of these problems.

We then investigate the computational complexity of a more general verification problem, model-checking, when an instance of the problem consists of a formula and a description of a system whose state space is at most exponentially larger than the description.

We continue by considering the problem of performing model-checking relative to a partial order semantics of concurrent systems, in which not all possible sequences of actions are considered relevant. We provide the first, to the best of our knowledge, set of sound and complete tableau rules for a CTL-like logic interpreted under progress fairness assumptions.

In the second part, we investigate Joyal, Nielsen, and Winskel's proposal of spans of open maps as an abstract category-theoretic way of adjoining a bisimulation equivalence, -bisimilarity, to a category of models of computation . We show that a representative selection of well-known bisimulations and behavioural equivalences can be captured in the setting of spans of open maps.

We then define the notion of functors being -factorisable and show how this ensures that -bisimilarity is a congruence with respect to such functors.

In the last part we investigate set constraints. Set constraints are inclusion relations between expressions denoting sets of ground terms over a ranked alphabet. They are typically derived from the syntax of a program and solutions to them can yield useful information for, e.g., type inference, implementations, and optimisations.

We provide a complete Gentzen-style axiomatisation for sequents , where and are finite sets of set constraints, based on the axioms of termset algebra. We show that the deductive system is complete for the restricted sequents over standard models, incomplete for general sequents over standard models, but complete for general sequents over set-theoretic termset algebras.

We then continue by investigating Kozen's rational spaces. We give several interesting results, among others a Myhill-Nerode like characterisation of rational points.

Available as PostScript, PDF.