Trend-Based Analysis of a Population Model of the AKAP Scaffold Protein

摘要: We formalise a continuous-time Markov chain with multi-dimensional discrete state space model of the AKAP scaffold protein as crosstalk mediator between two biochemical signalling pathways. The analysis by temporal properties requires reasoning about whether counts individuals same type (species) are increasing or decreasing. For this purpose we propose concept stochastic trends based on formulating probabilities transitions that increase (resp. decrease) type, and express these formulae such is not altered. define number trend (e.g. weakly increasing, strictly decreasing, etc.) use them to extend set Continuous Stochastic Logic. show how can be implemented in guarded-command style specification language for transition systems. illustrate application numerous small examples then analyse order characterise causality pulsating behaviours system.