Process Algebra as Modelling: Process Algebra as Modelling Chris Tofts
HPLB, August 2005
Some wider thoughts: Some wider thoughts
And after 7.5 Million years: And after 7.5 Million years
Key Problems: Key Problems How do you verify simulations – especially Markov based ones?
Can you get negative results from a simulation?
Can you treat mathematics like different processor architectures?
How do you get decision makers to believe the results of models?
All the problems I’ve had process algebra with…: All the problems I’ve had process algebra with… Or all the problems I’ve had with process algebra
Just as a list: Just as a list Ant activity synchronisation
Task allocation in ants, bees and naked mole rats
Brood sorting in Ants
Path finding in ants
Effects of vertical parasites on population extinction
Vertical parasite within host transmission
Parasite mediated meta population dynamics
Foster’s bottling plant in Birmingham
Semantics of Demos – generic discrete event simulator
Correctness of NUMA memory control
Spawning Systems
Concurrent queue control
Correctness of asynchronous hardware
Timing behaviour of asynchronous hardware
Probabilistic performance of asynchronous hardware
Evolution of sex
Channel allocation in mobile phones
Modelling bursty/autosynchronised traffic
Desynchronisation in parallel pipelines
Efficient modelling of resource
Reductionism vs functional
For some selected models: For some selected models How the model works
How big the systems were
What the models predicted/demonstrated
What I learnt from doing it
Any future work
Task Allocation: Task Allocation
The model: The model Tasks are arranged in order – consequence of the physical nature of the colony situation
If you do not find sufficient work for some number of ‘turns’ then consider moving
If moving move up or down a task with a certain probabilities – may not necessarily be symmetric ‘please don’t make me forage’
Results: Results If there is an optimum arrangement of the animals with respect to the tasks then this will eventually be reached.
Observations: Observations Can include animals with specialised ‘morphs’ – they are either only willing to perform one task, and grab the work their with higher priority than task mates, or move towards favoured task with high probability when given excuse.
Can model dynamics of task, consider placing all animals as correct solution to different task allocation problem, see how long stability takes to arise.
Can build really small simulation on top of proved results and use it to do further arithmetic such as tracking age.
What I learnt: What I learnt Power of Markov chain decomposition theorem
Cannot get the data to support further modelling
Get really small simulation which can be compared with theorem – only used for arithmetic not for fundamental property checking
Don’t mess with genetic determinists
Upsets Aristotle
What happened afterwards: What happened afterwards The ‘foraging for work’ task allocation method often described as controversial – used as experimental design example in biology
Many experiments trying to compare it with ‘old’ hypotheses
Path Finding in Vertical Parasites: Path Finding in Vertical Parasites
The model: The model Parasite moves into daughter cells when cells split
Parasite ‘tracks’ gonadal tissue with probability p
Parasite breeds by duplication at a rate relative to the host cell division rate
Once in a cell the parasite cannot move between cells
Results: Results Particular distribution for parasite load in cells of embryo
Demonstrated that parasites about 70% ‘good’ at tracking pre-gonadal tissue
Possible explanation for less than 100% transmission effectiveness of vertical parasites
Early within host cell level model of disease process
What I learnt: What I learnt Close relationship of particular class of probabilistic processes to branching processes
Clarity of presentation of process algebra
Just how much pain can be inflicted on a biology PhD student
Further work: Further work Closely related to work on ‘male exhaustion
Leading to meta population analysis of local extinction caused by parasitism
Possible explanation of co-evolutionary stability
Evolution of Sex: Evolution of Sex
The model: The model Multiple factors on a chromosone
Outcome determined by probabilistic function on count
Count Outcome Definitely male Definitely female 50/50
Results: Results 3 Solutions C,C X,Y X,X Z,Z Z,W L,L L,H H,H Type 1 Type 2 Type 2 Type 3
Results(2): Results(2) Some species of turtle show limit of about 87% ESD – just where the total lies in Type 3
What I learnt: What I learnt Need to be careful about closed states – the actual closed state here is no animals
Need to be careful applying Hardy-Weinberg
Can take a very long time to run the sims to cross check the maths
Simulo state space 2000 animals 2*20 factors each, so raw state space of k*(20)^2000
Further work: Further work When distributed over multiple chromosones get 1 new really weird type – but looks(;-)) very delicate hard to reach
Interaction with cross over rate
Way too weird for biologists not height
When done against probabilistic function get types 1 and 3 only but lets look at evidence for XY and ZW, often based on 2 animals…
Problems + My Gain: Problems + My Gain
Problems + My Gain: Problems + My Gain
Correctness of asynchronous hardware
Timing behaviour of asynchronous hardware
Probabilistic performance of asynchronous hardware
Evolution of sex
Desynchronisation in parallel pipelines
Efficient modelling of resource
Process Algebras Achievements: Process Algebras Achievements Composition
Composition
Composition (or is this just algebra?)
Very small notation for very large problems – even though I didn’t show it, none of these problems run to much more than a page
Actually copes with non-computational concurrent systems
More different calculi than string theory
Fixed ratio of calculi to calculations during researchers lifetime
Acknowledgements: Acknowledgements Mel Hatcher, Graham Birtwistle, Faron Moller, Alison Dunn, Nigel Franks, Tim Stickland, Anna Sendova-Franks, Matthew Morely, Athena Christodoulou, Steve Furber, Doug Edwards, James Dyer, Richard Taylor, Rebecca Terry, Don Goodeve, Dale Tanneyhill, David Pym, Jamie Dick, numerous 3rd year Biology project students
Slide29: