Specifying message passing and time-critical systems with temporal logic (Q684564)

This monograph, based on the 1989 Ph.d. thesis of the author presents a temporal logic based framework for specification of Message passing systems and time-critical systems. The idea to use some logical formalism for specification of systems is quite standard, and also the use of temporal logic for this purpose is not original. The next issue to be decided on is the precise nature of the logic used, and it it on this point that the various treatments in the literature diverge substantially. The author aims with his choices at a rather uniform framework where the temporal logic is extended with powerful tools all remaining within the scope of multi-modal logic. This is motivated by the observation that by introducing ad-hoc mechanisms involving abstract data structures the specification uses precisely the sort of implementation specific details one wants to escape from when setting up the specification. Also the specification for similar systems should resemble each other (something which seems to be not the case in part of the literature referred to). The required sort of enrichments are of various nature. It was in the work of the author that the usefulness of adding a modal operator Dp stating that \(p\) holds in some different world was brought to my attention for the first time. The monograph includes a section on the logical properties of this extension of modal logic; this theory in the mean time has been brought to maturity in the Ph.D. research of Maarten de Rijke. A second extension is the introduction of uniqueness assumptions about messages etc. to be inserted into the system. A rather elementary expressiveness result shows that without such assumptions on the environment no unbounded buffer transmission system can be specified. In the final section an extension of temporal logic called metric temporal logic is introduced for specifying time-critical systems. This language allows to talk about events occurring within a given amount of time without introducing a time variable in the state description. The logic requires however first order quantification over an arithmetic domain used for measuring time intervals. Note however that both the time space and its measure domain are subjected to rather mild axioms which support both the standard domains like the integers, reals or rationals and non-Archimedean domains. The monograph presents an unusual mixture of logic and applied computer science. The logics introduced are investigated with respect to axiomatizability, expressiveness and correspondence theory (but no complexity issues are mentioned other than in the discussion about related approaches in the literature). Subsequently the use of the logics is illustrated by simple examples some of which are drawn from the authors previous experience (he has worked for some years in industry before starting on this thesis project). In the concluding section the work is compared to work by others. Clearly in order to appreciate the merits of the proposed formalisms one needs a more complete insight in the various alternatives than can be provided for in such a concluding survey. What is clear however is that the author has successfully remained within the constraints stated in the introduction. With respect to the sections on the logics one can note that the inclusion of correspondence theory is unusual for computer science logic. The treatment of Sahlqvist theorems stating which modal properties correspond to first order frame properties give proof of the influence of van Benthem on this research project.