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: