Re: Formalizing models (CCS models)

[David Sumpter]

I just thought I'd write something about my favourite formalisation - Robin 
Milner's CCS. This has now been superceded my Pi-calculus but it goes on the 
same principles.

There is a paper by Rob Pooley on using CCS to describe process based models. 
Process based models are simply sets of queues which individuals pass through. 
Each process is an individual and the individuals interact by sitting waiting 
to 
be in these queues. These processes can be modelled using temporal CCS. See

http://www.dcs.ed.ac.uk/home/rjp/simulation/index.html

Since the queues form a simple environment (in the SWARM sense), it is easy to 
generate complete formal descriptions of both it and the agents (processes).
Such a formal description allows us to seperate qualitative behaviour (analysis 
of the formalism) and quantitive behaviour (simulation). For example, we can 
prove that an agent could become stuck in some state, affecting the simulation 
in some way. Without this knowledge we may have concluded that the global 
effects found in a simulation were due to a general behaviour of the individual.

Creating formalisms in this way is not so easy when the environment is 
spatially 
explicit (which it seems to be with most ALife models). Here, the environment 
has so many states as to make analysis intractable. However, it would be 
possible to formalise the model without reference to the environment. For 
example, here is a possible model of bears catching fish (see above reference 
for interpretation of the syntax),

\begin{eqnarray*}
Bear_0 & = & (T_{catch})\delta.kill.bear_1 + (T_{nocatch}){\bf 0} \\
Bear_1 & = & (T_{catch})\delta.kill.bear_2 + (T_{nocatch}){\bf 0} \\
Bear_2 & = & (T_{catch})\delta.kill.(bear_0 | bear_0) + (T_{nocatch}){\bf 0} \\
\end{eqnarray*}
\normalsize
\small
\begin{eqnarray*}
Fish_1 & = & \delta.kill.{\bf 0} + (T_{birth})fish_2 \\
Fish_2 & = & \delta.kill.fish_1 + (T_{birth})fish_3 \\
..... & & \\
Fish_n & = & \delta.kill.fish_{n-1} + (T_{birth})fish_{n+1} \\
..... & & \\
\end{eqnarray*}
\normalsize
The value {\bf 0} implies the agent cannot act. The CCS model for 5 bears and 
20 
fish is therefore,
\small
\begin{eqnarray*}
Model & = & (Bear_0 | Bear_0 | Bear_0 | Bear_0 | Bear_0 | Fish_20)
\end{eqnarray*}
\normalsize
The times for $(T_{catch})$, $(T_{nocatch})$ and $(T_{birth})$ are determined 
by 
the positions of the bears in the environment and their random movements (i.e. 
simulation). The formal model can be used here to prove that when there are no 
fish, all the bears will die (starvation). Obvious, but possibly more useful in 
complicated examples.

This is formalisation to a weak degree and does not fulfill the description  
which Roger wants for repeatable experiments (i.e. $(T_{catch})$, 
$(T_{nocatch})$ and $(T_{birth})$ are not well defined). However, it does give 
us a formalism to find answers about our own simulations and could be combined 
with a description of environment to give a complete, repeatable experiment 
type 
formalism.

David.

---------------------------------------------------------------
David J.T. Sumpter
Mathematics Department, UMIST, P.O. Box 88, Manchester, M60 1QD

http:\\www.ma.umist.ac.uk\dsumpter\index.html
---------------------------------------------------------------  



                  ==================================
   Swarm-Modelling is for discussion of Simulation and Modelling techniques
   esp. using Swarm.  For list administration needs (esp. [un]subscribing),
   please send a message to <address@hidden> with "help" in the
   body of the message.
                  ==================================