PH.D. Thesis Abstract

Abstract

   The subject matter of this thesis is a mathematical approach to the analysis of concurrent finite-state systems. Finite-state systems with concurrent features (such as the behaviour of digital circuits) is inherently very complex. A great deal of interest has been attracted to research new and novel techniques for ensuring the correctness of their functions. In this thesis, we explore the technique of formal verification with a process algebra. A central task which is regarded as essential in establishing a good verification technique is to be carried out.
   The task is to settle a criterion for deciding identity/distinction between system behaviours. Three considerations need to be taken into account. First, such a criterion is expected to be a reasonable one; any statement about identity/distinction claimed by the criterion needs to sustain a natural interpretation which is consistent to the way systems behave. Secondly, the criterion should be a correct mathematical model to the real world; it ought to be able to underpin an algebraic system for reasoning about the behaviour of systems. Thirdly, the criterion is required to be computed within acceptable time; thus systems with large scale complexity cam be dealt with.
   Motivated by these three considerations, a new notion of system behavioural interpretation (an operational semantics of an algebraic system) is proposed. Compared with several well-known counterpart notions in accordance with the three desirable considerations stated above, the new interpretation is found to be an improved work.