Deliverable D3
Deliverable D3
The temporal logic formalism showed considerable promise at the beginning of the project by yielding a finite state Markov model in which all past history could be encoded in the state. This allowed simple examples to be specified naturally in terms of constraints on their operation and a Markov model to be generated automatically and solved directly. A major problem was the size of the state space which grows dramatically as the complexity of the problem increases, precluding solution for non-trivial models. This work was first presented at the 2nd Qmips Workshop in Erlangen in 1993 and an early draft of a report was included with deliverable D1. It appeared in its final form as [2] in the book ``Time and Logic'' edited by L. Bolk and A. Szalas, and is included as the first report of this deliverable.
The key idea is to use the separation theorem of Gabbay [1] to decompose any formula in the logic into an implication from past and present to future. It was then shown that the past could be successively encoded finitely into the present by appropriately expanding the current state. This then leads to a discrete-time, finite state-space Markov chain. In fact our interest in the separation theorem and other logics, such as interval logics-which allow reasoning about intervals rather than points of time-led to interaction with the research group of Dra. Inma Perez de Guzman at the University of Malaga. The paper [3] written there arose from our extensive discussions and their novel approach.
Later in the project, our emphasis and effort shifted from Temporal Logic as the more direct effectiveness of the Process Algebra paradigm became apparent. The reason for this is that processes relate directly to traditional performance modelling concepts and so are easier to analyse quantitatively. In the temporal logic paradigm, processes must be described in terms of events, i.e. their initiation and completion, which is overly cumbersome. In fact it is here that an interval logic might be more appropriate since it could describe the duration of a process rather than only its end-points. It has also proved difficult to find efficient solution methods for the large Markov chains generated in the present temporal logic approach.
On the other hand, temporal logic can express assertions about the behaviour and performance of systems concisely, allowing performance to be specified under given constraints, for example. It was therefore considered more productive to advance the Process Algebra with a view to incorporating an appropriate Temporal Logic at a later date. The second report in this deliverable, written by the Erlangen group in German, but with an English abstract, describes an extension of the expressive power of a Process Algebra using Temporal Logic to specify constraints.