Temporal logic and compositional reasoning.

[Adrian Lawrence <adrian@xxxxxxxxxxxxxxx>]

As I understand it, Lamport's semantics for temporal logic is an
untyped mapping of Names --> Values describing the whole universe.
With minor technical extensions to admit "rigid variables".
And I think this is common to all flavours of temporal logic, although 
I have only been able to lay my hands on one other very old account
of temporal logic (Pnueli, 1979 - at least it was by the originator).
I gather, but may be wrong, that Lamport's TLA is distinctive in laying
emphasis on Actions (a Z person might call these Delta schemas) which
are (predicates on) state transitions, and the introduction of
stuttering which admits state transitions where nothing (relevant)
changes. 


Temporal Logic, occam, CSP and decoupling = decomposition?
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Conventional CSP does not include assignment: it can model assignment, but
it is not a primitive.

In occam, processes communicate in two ways: by participating in common
events: channels. And by safely sharing memory. When two process share
memory, it is read-only, and thus corresponds to Lamport's "rigid
variables". So in occam, we can cleanly distinguish communication
from state. As a rule, we can regard the memory changes as the private
internal matters of the processes. And the communication as the external
behaviour of processes. So it is that we can abstract from the internal
details of processes and build a very simple CSP model of just
the communication behaviour of an occam program. This is a very powerful
technique which we all use intuitively and some of us use more formally.

I suppose that it ought to be possible to do the same thing in formalisms
like temporal logic, but it is not the natural distinction that falls into
your lap. In Unity (Chandy & Misra) which perhaps has the purest form
of state transition model, channels can be identified with variables
representing the sequence of communications. There the idea of
channels is really regarded as just a particular implementation of a higher
level "pure" program. I suspect that Lamport is taking a similar view
in temporal logic.

But we have a natural decomposition into communication and state changes
which is a distinctive feature of occam. Because it includes both
CSP message passing and conventional state transformations. Allowing
us to separate concerns and keep things simple. A clear real benefit
of a compositional system.


Until HCSP (forgive the advertisement), we had no simple way to argue about
the state transitions within the processes. We were back to conventional
techniques. With HCSP, we now have a simple way to capture and model the 
state transitions as well. With abstraction so that we need not necessarily
carry all the baggage of the real program. 
   
Adrian
-- 
Adrian Lawrence.

adrian.lawrence@xxxxxxxxxxxxxxx     or adrian.lawrence@xxxxxxxxxxxxxx
Oxford University Computing Laboratory, |  Oxford University MicroProcessor
Wolfson Building,                       |  13, Banbury Road,            Unit,
Parks Road, Oxford.                     |  Oxford. OX2 6NN.
OX1 3QD. UK.                            |  UK.
Voice: (+44)-1865-273274  Fax: (+44)-1865-273275