PDGF Signal Path Verification Based On Probabilistic Model Detection And Counter-example Generation And Analysis

Model checking is an effective automated verification technology that has been successfully applied to the analysis and verification of systems in the areas of security and communication protocol,random distributed algorithms,biological systems and power management.As a formal verification technique,model checking can perform an exhaustive search on the state space of the system and verify the correctness of the properties.When the system does not satisfy the properties described by the logic formula,it can provide a counterexample to help the user modify the model or redesign model.Model checking is also widely used as a debugging technique to help users analyze the cause of errors when the model dissatisfies properties.Probabilistic model checking can not only qualitatively detect the system,but also quantitatively detect the correctness of a finite state system with random behavior.Therefore,it is widely used and achieves remarkable results,but for the system which dissatisfies the property,the probabilistic model checker is not available for counterexamples.Particularly,in detection of complex systems,such as signal transduction networks and gene regulatory networks,the signal transduction molecules interact and recognize each other,and transmit signals from the outside to the inside of the cell.In addition to performing its own signal transmission function,the signal pathways responsible for different biological functions in the cell also mutually restrict or mutually promote each other,thereby forming crosstalk between the signal pathways,making the system more complicated.If The probabilistic model checker can't provide useful debugging information,it will greatly limit the application of probabilistic model checking in complex networks.At present,many scholars at home and abroad have made a lot of research in the field of classical model checking and probabilistic model checking,the probabilistic model detection counterexample generation and analysis has not been comprehensively studied.In this paper,we apply the probabilistic model checking to the platelet-derived growth factor signal transduction path,and give a counterexample to the system that does not satisfy the property.The analysis of the counterexample information leads to the reason that the system does not satisfy the property.The main study for this paper are the following:1.In this paper,the probabilistic model checking technique is applied to the PDGF signal transduction path.The dynamic model of the signal pathway and the crosstalk between the signal pathways are studied by the probabilistic model checking method,and the biological phenomena are explained in the PDGF signal transduction pathway.2.The counter-example pathway of the unsatisfied property of the PDGF signal transduction pathway is generated by the XBF algorithm,which helps the user to analyze and debug errors when the model does not satisfy the described properties.3.Through further analysis of the counterexamples to find out the cause of the PDGF signal transduction path not satisfying the described properties.